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, 60 insertions, 7 deletions

diff --git a/src/interpreter.ml b/src/interpreter.ml
index 4fd75094..7e84f5c7 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -53,20 +53,30 @@ open Ast_util
 open Value
 
 type gstate =
-  { registers : value Bindings.t }
+  { registers : value Bindings.t;
+    letbinds : (Type_check.tannot letbind) list
+  }
 
 type lstate =
   { locals : value Bindings.t }
 
 type state = lstate * gstate
 
-let initial_gstate =
-  { registers = Bindings.empty }
+let rec ast_letbinds (Defs defs) =
+  match defs with
+  | [] -> []
+  | DEF_val lb :: defs -> lb :: ast_letbinds (Defs defs)
+  | _ :: defs -> ast_letbinds (Defs defs)
+
+let initial_gstate ast =
+  { registers = Bindings.empty;
+    letbinds = ast_letbinds ast
+  }
 
 let initial_lstate =
   { locals = Bindings.empty }
 
-let initial_state = initial_lstate, initial_gstate
+let initial_state ast = initial_lstate, initial_gstate ast
 
 let value_of_lit (L_aux (l_aux, _)) =
   match l_aux with
@@ -77,6 +87,11 @@ let value_of_lit (L_aux (l_aux, _)) =
   | L_false -> V_bool false
   | L_string str -> V_string str
   | L_num n -> V_int n
+  | L_hex str ->
+     Util.string_to_list str
+     |> List.map (fun c -> List.map (fun b -> V_bit b) (Sail_lib.hex_char c))
+     |> List.concat
+     |> (fun v -> V_vector v)
   | _ -> failwith "Unimplemented value_of_lit" (* TODO *)
 
 let is_value = function
@@ -175,7 +190,7 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
     | E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps)
     | E_app_infix (exp1, op, exp2) -> E_app_infix (subst id value exp1, op, subst id value exp2)
     | E_tuple exps -> E_tuple (List.map (subst id value) exps)
-    | E_assign (lexp, exp) -> E_assign (lexp, subst id value exp) (* Shadowing... *)
+    | E_assign (lexp, exp) -> E_assign (subst_lexp id value lexp, subst id value exp) (* Shadowing... *)
     | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) ->
        (* TODO: Fix shadowing *)
        E_let (LB_aux (LB_val (pat, subst id value bind), lb_annot), subst id value body)
@@ -189,6 +204,16 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
   in
   wrap e_aux
 
+and subst_lexp id value (LEXP_aux (lexp_aux, annot) as lexp) =
+  let wrap lexp_aux = LEXP_aux (lexp_aux, annot) in
+  let lexp_aux = match lexp_aux with
+    | LEXP_deref exp -> LEXP_deref (subst id value exp)
+    | LEXP_id id' -> LEXP_id id'
+    | LEXP_memory (f, exps) -> LEXP_memory (f, List.map (subst id value) exps)
+    | _ -> failwith ("subst lexp")
+  in
+  wrap lexp_aux
+
 
 (**************************************************************************)
 (* 2. Expression Evaluation                                               *)
@@ -199,6 +224,14 @@ let unit_exp = E_lit (L_aux (L_unit, Parse_ast.Unknown))
 let is_value_fexp (FE_aux (FE_Fexp (id, exp), _)) = is_value exp
 let value_of_fexp (FE_aux (FE_Fexp (id, exp), _)) = (string_of_id id, value_of_exp exp)
 
+let rec build_letchain lbs (E_aux (_, annot) as exp) =
+  print_endline ("LETCHAIN " ^ string_of_exp exp);
+  match lbs with
+  | [] -> exp
+  | lb :: lbs ->
+     let exp = E_aux (E_let (lb, exp), annot) in
+     build_letchain lbs exp
+
 let rec step (E_aux (e_aux, annot) as orig_exp) =
   let wrap e_aux' = return (E_aux (e_aux', annot)) in
   match e_aux with
@@ -246,6 +279,9 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
      else
        failwith "Match failure"
 
+  | E_vector_update (vec, n, x) ->
+     wrap (E_app (mk_id "vector_update", [vec; n; x]))
+
   (* otherwise left-to-right evaluation order for function applications *)
   | E_app (id, exps) ->
      let evaluated, unevaluated = Util.take_drop is_value exps in
@@ -298,6 +334,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
   | E_throw exp when is_value exp -> throw (value_of_exp exp)
   | E_throw exp -> step exp >>= fun exp' -> wrap (E_throw exp')
 
+  | E_ref id -> return (exp_of_value (V_ref (string_of_id id)))
   | E_id id ->
      begin
        let open Type_check in
@@ -312,6 +349,10 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
           in
           return exp
        | Local (Mutable, _) -> return (exp_of_value (Bindings.find id lstate.locals))
+       | Local (Immutable, _) ->
+          let chain = build_letchain gstate.letbinds orig_exp in
+          print_endline "CHAINED";
+          return chain
        | _ -> failwith "id"
      end
 
@@ -355,6 +396,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
      let ul = (Parse_ast.Unknown, None) in
      let exp' = E_aux (E_record_update (lexp_exp, FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), ul)], false), ul)), ul) in
      wrap (E_assign (lexp, exp'))
+  | E_assign (LEXP_aux (LEXP_vector (vec, n), _), exp) ->
+     let open Type_check in
+     let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in
+     let ul = (Parse_ast.Unknown, None) in
+     let exp' = E_aux (E_vector_update (vec_exp, n, exp), ul) in
+     wrap (E_assign (vec, exp'))
   | E_assign (LEXP_aux (LEXP_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) ->
      begin
        let open Type_check in
@@ -366,6 +413,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
           puts ({ lstate with locals = Bindings.add id (value_of_exp exp) lstate.locals }, gstate) >> wrap unit_exp
        | _ -> failwith "Assign"
      end
+  | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) when not (is_value reference) ->
+     step reference >>= fun reference' -> wrap (E_assign (LEXP_aux (LEXP_deref reference', annot), exp))
+  | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) ->
+     let id = Id_aux (Id (coerce_ref (value_of_exp reference)), Parse_ast.Unknown) in
+     gets >>= fun (lstate, gstate) ->
+     puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp
   | E_assign _ -> assert false
 
   | E_try (exp, pexps) when is_value exp -> return exp
@@ -443,7 +496,7 @@ let rec get_fundef id (Defs defs) =
 let stack_cont (_, _, cont) = cont
 let stack_string (str, _, _) = str
 let stack_state (_, lstate, _) = lstate
-                            
+
 type frame =
   | Done of state * value
   | Step of string * state * (Type_check.tannot exp) monad * (string * lstate * (value -> (Type_check.tannot exp) monad)) list
@@ -473,5 +526,5 @@ let rec eval_frame ast = function
         print_endline ("Returning value: " ^ string_of_value v |> Util.cyan |> Util.clear);
         Step (stack_string head, (stack_state head, snd state), stack_cont head v, stack')
      | Yield (Assertion_failed msg), _ ->
-        failwith msg 
+        failwith msg
      | _ -> assert false