@@ -66,6 +66,33 @@ object Objects:
66
66
67
67
// ----------------------------- abstract domain -----------------------------
68
68
69
+ /** Syntax for the data structure abstraction used in abstract domain:
70
+ *
71
+ * ve ::= ObjectRef(class)
72
+ * | OfClass(class, vs[outer], ctor, args, env)
73
+ * | OfArray(object[owner], regions)
74
+ * | Fun(..., env)
75
+ * | Cold // abstract values in domain
76
+ * vs ::= Set(ve) // set of abstract values
77
+ *
78
+ * refMap = ( ObjectRef | OfClass ) -> ( valsMap, varsMap, outersMap ) // refMap stores field informations of an object or instance
79
+ * valsMap = valsym -> vs // maps immutable fields to their values
80
+ * varsMap = valsym -> addr // each mutable field has an abstract address
81
+ * outersMap = class -> vs // maps outer objects to their values
82
+ *
83
+ * arrayMap = OfArray -> addr // an array has one address that stores the join value of every element
84
+ *
85
+ * heap = addr -> vs // only this map's entries can be modified
86
+ *
87
+ * env = (valsMap, Option[env]) // stores local variables in the residing method, and possibly outer environments
88
+ *
89
+ * addr ::= localVarAddr(regions, valsym, owner)
90
+ * | fieldVarAddr(regions, valsym, owner) // independent of OfClass/ObjectRef
91
+ * | arrayAddr(regions, owner) // independent of array element type
92
+ *
93
+ * regions ::= List(sourcePosition)
94
+ */
95
+
69
96
sealed abstract class Value :
70
97
def show (using Context ): String
71
98
0 commit comments