Lots of experimental changes on this branch

* Changed comment syntax to C-style /* */ and //

* References to registers and mutable variables are never created
implicitly - a reference to a register or variable R is now created
via the expression "ref R". References are assigned like "(*Y) = X",
with "(*ref R) = X" being equivalent to "R = X". Everything is always
explicit now, which simplifies the logic in the typechecker. There's
also now an invariant that every id directly in a LEXP is mutable,
which is actually required for our rewriter steps to be sound.

* More flexible syntax for L-expressions to better support wierd
power-idioms, some syntax sugar means that:

X.GET(a, b, c)  ==>  _mod_GET(X, a, b, c)
X->GET(a, b, c)  ==>  _mod_GET(ref X, a, b, c)

for setters, this can be combined with the (still somewhat poorly
named) LEXP_memory construct, such that:

X->SET(a, b, c) = Y  ==>  _mod_SET(ref X, a, b, c, Y)

Currently I use the _mod_ prefix for these 'modifier' functions, but
we could omit that a la rust.

* The register bits typedef construct no longer exists in the
typechecker. This construct never worked consistently between backends
and inc/dec vectors, and it can be easily replaced by structs with
fancy setters/getters if need be. One can also use custom type operators to mimic the syntax, i.e.

type operator ... ('n : Int) ('m : Int) = slice('n, 'm)

struct cr = {
  CR0 : 32 ... 35,
  /* 32 : LT; 33 : GT; 34 : EQ; 35 : SO; */
  CR1 : 36 ... 39,
  /* 36 : FX; 37 : FEX; 38 : VX; 39 : OX; */
  CR2 : 40 ... 43,
  CR3 : 44 ... 47,
  CR4 : 48 ... 51,
  CR5 : 52 ... 55,
  CR6 : 56 ... 59,
  CR7 : 60 ... 63,
}

This greatly simplifies a lot of the logic in the typechecker, as it
means that E_field is no longer ambiguously overloaded between records
and register bit typedefs. This also makes writing semantics for these
constructs much simpler.

1 files changed, 8 insertions, 0 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index a28352f5..87baa746 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -328,6 +328,7 @@ let rewrite_sizeof (Defs defs) =
     { e_block = (fun es -> let (es, es') = List.split es in (E_block es, E_block es'))
     ; e_nondet = (fun es -> let (es, es') = List.split es in (E_nondet es, E_nondet es'))
     ; e_id = (fun id -> (E_id id, E_id id))
+    ; e_ref = (fun id -> (E_ref id, E_ref id))
     ; e_lit = (fun lit -> (E_lit lit, E_lit lit))
     ; e_cast = (fun (typ,(e,e')) -> (E_cast (typ,e), E_cast (typ,e')))
     ; e_app = (fun (id,es) -> let (es, es') = List.split es in (E_app (id,es), E_app (id,es')))
@@ -368,6 +369,7 @@ let rewrite_sizeof (Defs defs) =
     ; e_internal_value = (fun v -> (E_internal_value v, E_internal_value v))
     ; e_aux = (fun ((e,e'),annot) -> (E_aux (e,annot), E_aux (e',annot)))
     ; lEXP_id = (fun id -> (LEXP_id id, LEXP_id id))
+    ; lEXP_deref = (fun (e, e') -> (LEXP_deref e, LEXP_deref e'))
     ; lEXP_memory = (fun (id,es) -> let (es, es') = List.split es in (LEXP_memory (id,es), LEXP_memory (id,es')))
     ; lEXP_cast = (fun (typ,id) -> (LEXP_cast (typ,id), LEXP_cast (typ,id)))
     ; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups'))
@@ -2955,6 +2957,12 @@ let rewrite_defs_ocaml = [
   (* ("separate_numbs", rewrite_defs_separate_numbs) *)
   ]
 
+let rewrite_defs_interpreter = [
+    ("constraint", rewrite_constraint);
+    ("trivial_sizeof", rewrite_trivial_sizeof);
+    ("sizeof", rewrite_sizeof);
+  ]
+
 let rewrite_defs_sil = [
     ("top_sort_defs", top_sort_defs);
     ("tuple_vector_assignments", rewrite_tuple_vector_assignments);