Changes between Version 94 and Version 95 of IR2

Timestamp:

05/13/21 14:01:34 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -257 +257 @@
 * Explanation of `$defined`:
   * A bit is associated to each object.  We say an object is "defined" if the bit is true, else it is undefined.
-  * An object is initially undefined.  It becomes defined by assignment.
+  * An object is initially undefined.  It becomes defined by assignment.   If the right hand side of the assignment involves undefined objects, it is unspecified whether the left hand side will be defined.
   * Objects of pointer type are special in that they can change from defined to undefined.  This happens when the object into which they point is deallocated or goes out of scope.
   * An object of array type becomes defined when assigned a `$new_array`.  However, its elements are undefined.
   * An object of array type also becomes defined when assigned a `$new` value.  In that case, the elements are also defined.
   * A pointer becomes defined when assigned the result of an `$alloc`.   Each element in the newly allocated object is undefined.
-  * Example: to determine whether it is safe to read `*(p+i)`, assert `$summable(p, i) && $valid(p+i) && $defined(*(p+i))`.  You must check (1) you can sum `p` and `i`, (2) `p+i` points to an object of the base type, so dereference is safe, and (3) the object is defined (has been assigned a value).  If you aren't sure `p` and `i` have been defined, you can add `$defined(p) && $defined(i)` to the assertion.
+  * Example: to determine whether it is safe to read `*(p+i)`, assert `$summable(p, i) && $valid(p+i) && $defined(*(p+i))`.  You must check (1) you can sum `p` and `i`, (2) `p+i` points to an object of the base type, so dereference is safe, and (3) the object is defined (has been assigned a value).  If you aren't sure `p` and `i` have been defined, you can add `$defined(p) && $defined(i)` to the assertion.   It may be more efficient to use temporary variables and break this up into multiple assertions.
+
+=== How to implement `$defined` using symbolic execution ===
+
+Create a symbolic constant named `UNDEF` for each type T.   These can be created on-the-fly, as they are needed.
+
+Every variable is initialized to the `UNDEF` of its type.   The exception is a struct, which may be initialized to a concrete struct in which each field is `UNDEF`.   (Either way will work, but the latter will probably be more effective.)
+
+For a complete type T, the "undef-initializer" for T is defined as follows: if T is not an array type, the undef-initializer is defined exactly as above: either the symbolic constant `UNDEF` or a concrete struct of `UNDEF`s.   If T is the complete array type S[n], the undef-initializer is the array-lambda expression with length n and defining expression the undef-initializer for S.  
+
+`$new_array(n,T)` returns the undef-initializer for T[n].
+
+`$alloc(h,n,T)` creates a new object in the heap h with value the undef-initializer for T[n], and returns a pointer to element 0 of that object.
+
+Evaluation of `$defined(expr)` returns `!FORALL UNDEF:T . expr == UNDEF`, where `T` is the type of `expr`.