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, 10 insertions, 1 deletions

diff --git a/src/rewriter.ml b/src/rewriter.ml
index fb82b80f..53a43e5b 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -107,7 +107,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
   let effsum = match e with
     | E_block es -> union_eff_exps es
     | E_nondet es -> union_eff_exps es
-    | E_id _
+    | E_id _ | E_ref _
     | E_lit _ -> eff
     | E_cast (_,e) -> effect_of e
     | E_app (f,es) ->
@@ -339,6 +339,7 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) =
   let rewrap le = LEXP_aux(le,(l,annot)) in
   match lexp with
   | LEXP_id _ | LEXP_cast _ -> rewrap lexp
+  | LEXP_deref exp -> rewrap (LEXP_deref (rewriters.rewrite_exp rewriters exp))
   | LEXP_tup tupls -> rewrap (LEXP_tup (List.map (rewriters.rewrite_lexp rewriters) tupls))
   | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewriters.rewrite_exp rewriters) exps))
   | LEXP_vector (lexp,exp) ->
@@ -472,6 +473,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   { e_block                  : 'exp list -> 'exp_aux
   ; e_nondet                 : 'exp list -> 'exp_aux
   ; e_id                     : id -> 'exp_aux
+  ; e_ref                    : id -> 'exp_aux
   ; e_lit                    : lit -> 'exp_aux
   ; e_cast                   : Ast.typ * 'exp -> 'exp_aux
   ; e_app                    : id * 'exp list -> 'exp_aux
@@ -512,6 +514,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; e_internal_value         : Value.value -> 'exp_aux
   ; e_aux                    : 'exp_aux * 'a annot -> 'exp
   ; lEXP_id                  : id -> 'lexp_aux
+  ; lEXP_deref               : 'exp -> 'lexp_aux
   ; lEXP_memory              : id * 'exp list -> 'lexp_aux
   ; lEXP_cast                : Ast.typ * id -> 'lexp_aux
   ; lEXP_tup                 : 'lexp list -> 'lexp_aux
@@ -538,6 +541,7 @@ let rec fold_exp_aux alg = function
   | E_block es -> alg.e_block (List.map (fold_exp alg) es)
   | E_nondet es -> alg.e_nondet (List.map (fold_exp alg) es)
   | E_id id -> alg.e_id id
+  | E_ref id -> alg.e_ref id
   | E_lit lit -> alg.e_lit lit
   | E_cast (typ,e) -> alg.e_cast (typ, fold_exp alg e)
   | E_app (id,es) -> alg.e_app (id, List.map (fold_exp alg) es)
@@ -588,6 +592,7 @@ let rec fold_exp_aux alg = function
 and fold_exp alg (E_aux (exp_aux,annot)) = alg.e_aux (fold_exp_aux alg exp_aux, annot)
 and fold_lexp_aux alg = function
   | LEXP_id id -> alg.lEXP_id id
+  | LEXP_deref exp -> alg.lEXP_deref (fold_exp alg exp)
   | LEXP_memory (id,es) -> alg.lEXP_memory (id, List.map (fold_exp alg) es)
   | LEXP_tup les -> alg.lEXP_tup (List.map (fold_lexp alg) les)
   | LEXP_cast (typ,id) -> alg.lEXP_cast (typ,id)
@@ -618,6 +623,7 @@ let id_exp_alg =
   { e_block = (fun es -> E_block es)
   ; e_nondet = (fun es -> E_nondet es)
   ; e_id = (fun id -> E_id id)
+  ; e_ref = (fun id -> E_ref id)
   ; e_lit = (fun lit -> (E_lit lit))
   ; e_cast = (fun (typ,e) -> E_cast (typ,e))
   ; e_app = (fun (id,es) -> E_app (id,es))
@@ -658,6 +664,7 @@ let id_exp_alg =
   ; e_internal_value = (fun v -> E_internal_value v)
   ; e_aux = (fun (e,annot) -> E_aux (e,annot))
   ; lEXP_id = (fun id -> LEXP_id id)
+  ; lEXP_deref = (fun e -> LEXP_deref e)
   ; lEXP_memory = (fun (id,es) -> LEXP_memory (id,es))
   ; lEXP_cast = (fun (typ,id) -> LEXP_cast (typ,id))
   ; lEXP_tup = (fun tups -> LEXP_tup tups)
@@ -712,6 +719,7 @@ let compute_exp_alg bot join =
   { e_block = split_join (fun es -> E_block es)
   ; e_nondet = split_join (fun es -> E_nondet es)
   ; e_id = (fun id -> (bot, E_id id))
+  ; e_ref = (fun id -> (bot, E_ref id))
   ; e_lit = (fun lit -> (bot, E_lit lit))
   ; e_cast = (fun (typ,(v,e)) -> (v, E_cast (typ,e)))
   ; e_app = (fun (id,es) -> split_join (fun es -> E_app (id,es)) es)
@@ -760,6 +768,7 @@ let compute_exp_alg bot join =
   ; e_internal_value = (fun v -> (bot, E_internal_value v))
   ; e_aux = (fun ((v,e),annot) -> (v, E_aux (e,annot)))
   ; lEXP_id = (fun id -> (bot, LEXP_id id))
+  ; lEXP_deref = (fun (v, e) -> (v, LEXP_deref e))
   ; lEXP_memory = (fun (id,es) -> split_join (fun es -> LEXP_memory (id,es)) es)
   ; lEXP_cast = (fun (typ,id) -> (bot, LEXP_cast (typ,id)))
   ; lEXP_tup = (fun ls ->