Alias support for ocaml mode

4 files changed, 61 insertions, 24 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 6b7239b4..147e177b 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -287,15 +287,15 @@ and pp_format_o o =
 
 let pp_format_tag = function
   | Emp_local -> "Tag_empty"
-  | Emp_intro -> "Tag_empty" (*TODO carry this out for use in future analysis that doesn't use the interpreter?*)
-  | Emp_set -> "Tag_empty" (* Same as above *)
+  | Emp_intro -> "Tag_intro"
+  | Emp_set -> "Tag_set" 
   | Emp_global -> "Tag_global"
   | External (Some s) -> "(Tag_extern (Just \""^s^"\"))"
   | External None -> "(Tag_extern Nothing)"
   | Default -> "Tag_default"
   | Constructor -> "Tag_ctor"
   | Enum i -> "(Tag_enum " ^ (lemnum string_of_int i) ^ ")"
-  | Alias -> "Tag_alias"
+  | Alias alias_inf -> "Tag_alias"
   | Spec -> "Tag_spec"
 
 let rec pp_format_nes nes = 
@@ -634,6 +634,7 @@ let squarebarbars = enclose lsquarebarbar rsquarebarbar
 let lsquarecolon = string "[:"
 let rsquarecolon = string ":]"
 let squarecolons = enclose lsquarecolon rsquarecolon
+let string_lit = enclose dquote dquote
 let spaces op = enclose space space op
 let semi_sp = semi ^^ space
 let comma_sp = comma ^^ space
@@ -1327,7 +1328,7 @@ let doc_exp_ocaml, doc_let_ocaml =
             group ((string "set_vector_range") ^^ space ^^ (doc_lexp_ocaml le) ^^ space ^^ (exp e)))
        | _ ->
          (match le_act with
-          | LEXP_vector _ | LEXP_vector_range _ | LEXP_cast _ | LEXP_field _ ->
+          | LEXP_vector _ | LEXP_vector_range _ | LEXP_cast _ | LEXP_field _ | LEXP_id _ ->
             (doc_lexp_rwrite le e)
           | LEXP_memory _ -> (doc_lexp_fcall le e)))
     | E_vector_append(l,r) ->
@@ -1395,8 +1396,7 @@ let doc_exp_ocaml, doc_let_ocaml =
       (match fannot with
        | Base((_,{t= Tapp("register",_)}),_,_,_,_) |
          Base((_,{t= Tabbrev(_,{t=Tapp("register",_)})}),_,_,_,_)->
-        parens ((string "get_register_field") ^^ space ^^ (exp fexp) ^^ space ^^
-                (string "\"") ^^ (doc_id id) ^^ string "\"")
+        parens ((string "get_register_field") ^^ space ^^ (exp fexp) ^^ space ^^ string_lit (doc_id id))
       | _ -> exp fexp ^^ dot ^^ doc_id id)
     | E_block [] -> string "()"
     | E_block exps | E_nondet exps ->
@@ -1406,6 +1406,15 @@ let doc_exp_ocaml, doc_let_ocaml =
       (match annot with
       | Base((_, ({t = Tapp("reg",_)} | {t=Tabbrev(_,{t=Tapp("reg",_)})})),_,_,_,_) ->
         string "!" ^^ doc_id_ocaml id
+      | Base(_,Alias alias_info,_,_,_) ->
+        (match alias_info with
+         | Alias_field(reg,field) -> parens (string "get_register_field" ^^ space ^^ string reg ^^ string_lit (string field))
+         | Alias_extract(reg,start,stop) ->
+           if start = stop
+           then parens (string "bit_vector_access" ^^ space ^^ string reg ^^ space ^^ doc_int start)
+           else parens (string "vector_subrange" ^^ space ^^ string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop)
+         | Alias_pair(reg1,reg2) ->
+           parens (string "vector_append" ^^ space ^^ string reg1 ^^ space ^^ string reg2))        
       | _ -> doc_id_ocaml id)
     | E_lit lit -> doc_lit lit
     | E_cast(typ,e) -> (parens (doc_op colon (group (exp e)) (doc_typ typ)))
@@ -1516,10 +1525,28 @@ let doc_exp_ocaml, doc_let_ocaml =
       parens ((string "set_vector_subrange") ^^ space ^^
               doc_lexp_ocaml v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v)
     | LEXP_field(v,id) ->
-      parens ((string "set_register_field") ^^ space ^^ doc_lexp_ocaml v ^^ space ^^string "\"" ^^ doc_id id ^^
-              string "\"" ^^ space ^^ exp e_new_v)
-    | LEXP_id id -> doc_id_ocaml id
-    | LEXP_cast(typ,id) -> (doc_id_ocaml id)
+      parens ((string "set_register_field") ^^ space ^^
+              doc_lexp_ocaml v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v)
+    | LEXP_id id | LEXP_cast (_,id) ->
+      (match annot with
+       | Base(_,Alias alias_info,_,_,_) ->
+         (match alias_info with
+          | Alias_field(reg,field) ->
+            parens ((string "set_register_field") ^^ space ^^
+                    string reg ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v)
+          | Alias_extract(reg,start,stop) ->
+            if start = stop
+            then
+              doc_op (string "<-")
+                (group (parens ((string "get_varray") ^^ space ^^ string reg)) ^^ dot ^^ parens (doc_int start))
+                (exp e_new_v)
+            else 
+              parens ((string "set_vector_subrange") ^^ space ^^
+                      string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v)
+          | Alias_pair(reg1,reg2) ->
+            parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v))              
+       | _ -> 
+         doc_id_ocaml id) 
 
   and doc_lexp_fcall ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = match lexp with
     | LEXP_memory(id,args) -> doc_id_ocaml id ^^ parens (separate_map comma exp (args@[e_new_v]))
@@ -1556,7 +1583,7 @@ let doc_typdef_ocaml (TD_aux(td,_)) = match td with
         (concat [string "type"; space; doc_id_ocaml_type id;])
         (enums_doc)
   | TD_register(id,n1,n2,rs) ->
-    let doc_rid (r,id) = separate comma_sp [string "\"" ^^ doc_id id ^^ string "\""; doc_range_ocaml r;] in
+    let doc_rid (r,id) = separate comma_sp [string_lit (doc_id id); doc_range_ocaml r;] in
     let doc_rids = group (separate_map (break 1) doc_rid rs) in
     match n1,n2 with
     | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 9f97c482..1155473b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -497,7 +497,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       | Some(Base((params,t),tag,cs,ef,bounds)) ->
         let ((t,cs,ef,_),is_alias) = 
           match tag with | Emp_global | External _ -> (subst params false t cs ef),false 
-            | Alias -> (t,cs, add_effect (BE_aux(BE_rreg, Parse_ast.Unknown)) ef, Envmap.empty),true 
+            | Alias alias_inf -> (t,cs, add_effect (BE_aux(BE_rreg, Parse_ast.Unknown)) ef, Envmap.empty),true 
             | _ -> (t,cs,ef,Envmap.empty),false 
         in
         let t,cs' = get_abbrev d_env t in
@@ -517,12 +517,12 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
           (rebuild tannot,t,t_env,cs@cs',bounds,ef)
         | Tapp("register",[TA_typ(t')]),Tuvar _ ->
           let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
-          let tannot = Base(([],t),(if is_alias then Alias else External (Some i)),cs,ef',bounds) in
+          let tannot = Base(([],t),(if is_alias then tag else External (Some i)),cs,ef',bounds) in
           let t',cs',_,e' = type_coerce (Expr l) d_env Require false false b_env t' (rebuild tannot) expect_actual in
           (e',t,t_env,cs@cs',bounds,ef')
         | Tapp("register",[TA_typ(t')]),_ ->
           let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
-          let tannot = Base(([],t),(if is_alias then Alias else External (Some i)),cs,ef',bounds) in
+          let tannot = Base(([],t),(if is_alias then tag else External (Some i)),cs,ef',bounds) in
           let t',cs',_,e' = type_coerce (Expr l) d_env Require false false b_env t' (rebuild tannot) expect_actual in
           (e',t',t_env,cs@cs',bounds,ef')
         | Tapp("reg",[TA_typ(t')]),_ ->
@@ -1333,16 +1333,16 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
          let bounds = extract_bounds d_env i t in
          let tannot = (Base(([],t),Emp_intro,[],pure_e,bounds)) in
          (LEXP_aux(lexp,(l,tannot)),t,false,Envmap.from_list [i,tannot],Emp_intro,[],bounds,pure_e)
-       | Some(Base(([],t),Alias,_,_,_)) ->
+       | Some(Base(([],t),Alias alias_inf,_,_,_)) ->
          let ef = {effect = Eset[BE_aux(BE_wreg,l)]} in
          (match Envmap.apply d_env.alias_env i with
           | Some(OneReg(reg, (Base(([],t'),_,_,_,_)))) ->
-            (LEXP_aux(lexp,(l,(Base(([],t'),Alias,[],ef,nob)))), t, false, Envmap.empty, External (Some reg),[],nob,ef)
+            (LEXP_aux(lexp,(l,(Base(([],t'),Alias alias_inf,[],ef,nob)))), t, false, Envmap.empty, External (Some reg),[],nob,ef)
           | Some(TwoReg(reg1,reg2, (Base(([],t'),_,_,_,_)))) ->
             let u = match t.t with
               | Tapp("register", [TA_typ u]) -> u 
               | _ -> raise (Reporting_basic.err_unreachable l "TwoReg didn't contain a register type") in
-            (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef,nob))), u, false, Envmap.empty, External None,[],nob,ef)
+            (LEXP_aux(lexp,(l,Base(([],t'),Alias alias_inf,[],ef,nob))), u, false, Envmap.empty, External None,[],nob,ef)
           | _ -> assert false)
        | Some(Base((parms,t),tag,cs,_,b)) ->
           let t,cs,_,_ = 
@@ -1907,7 +1907,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
               (match lookup_field_type fi r with
                 | None -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
                 | Some et ->
-                  let tannot = Base(([],et),Alias,[],pure_e,nob) in
+                  let tannot = Base(([],et),Alias (Alias_field(reg,fi)),[],pure_e,nob) in
                   let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in
                   (AL_aux(AL_subreg(reg_a,subreg),(l,tannot)),tannot,d_env)))
         | _ -> typ_error l ("Expected a register with fields, given " ^ (t_to_string reg_t)))
@@ -1919,7 +1919,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
           (match (base.nexp,len.nexp,order.order, bit) with
             | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll))) ->
               if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k 
-              then let tannot = Base(([],item_t),Alias,[],pure_e,nob) in
+              then let tannot = Base(([],item_t),Alias (Alias_extract(reg, k,k)),[],pure_e,nob) in
                    let d_env = 
                      {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in
                    (AL_aux(AL_bit(reg_a,(E_aux(bit,(le,eannot)))), (l,tannot)), tannot,d_env)
@@ -1937,7 +1937,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
               if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k2 && k < k2 
               then let t = {t = Tapp("vector",[TA_nexp (int_to_nexp k);TA_nexp (int_to_nexp ((k2-k) +1));
                                               TA_ord order; TA_typ item_t])} in 
-                   let tannot = Base(([],t),Alias,[],pure_e,nob) in
+                   let tannot = Base(([],t),Alias (Alias_extract(reg, k, k2)),[],pure_e,nob) in
                    let d_env = 
                      {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in
                    (AL_aux(AL_slice(reg_a,(E_aux(sl1,(le1,eannot1))),(E_aux(sl2,(le2,eannot2)))),
@@ -1955,7 +1955,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
           let t = {t= Tapp("register",
                            [TA_typ {t= Tapp("vector",[TA_nexp b1; TA_nexp (mk_add r r2);
                                                       TA_ord {order = Oinc}; TA_typ item_t])}])} in
-          let tannot = Base(([],t),Alias,[],pure_e,nob) in
+          let tannot = Base(([],t),Alias (Alias_pair(reg1,reg2)),[],pure_e,nob) in
           let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, TwoReg(reg1,reg2,tannot))} in
           (AL_aux (AL_concat(reg1_a,reg2_a), (l,tannot)), tannot, d_env)
         | _ -> typ_error l 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index f91e7178..9ae5a319 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -73,6 +73,11 @@ and t_arg =
   | TA_eft of effect
   | TA_ord of order 
 
+type alias_inf =
+  | Alias_field of string * string
+  | Alias_extract of string * int * int
+  | Alias_pair of string * string
+
 type tag =
   | Emp_local
   | Emp_global
@@ -82,7 +87,7 @@ type tag =
   | Default
   | Constructor
   | Enum of int
-  | Alias
+  | Alias of alias_inf
   | Spec
 
 let rec compare_nexps n1 n2 =
@@ -323,7 +328,7 @@ let tag_to_string = function
   | Default -> "Default"
   | Constructor -> "Constructor"
   | Enum _ -> "Enum"
-  | Alias -> "Alias"
+  | Alias _ -> "Alias"
   | Spec -> "Spec"
     
 let enforce_to_string = function
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 93bb1f7c..d1396367 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -75,6 +75,11 @@ and t_arg =
 module Nexpmap : Finite_map.Fmap with type k = nexp
 type nexp_map = nexp Nexpmap.t
 
+type alias_inf =
+  | Alias_field of string * string
+  | Alias_extract of string * int * int
+  | Alias_pair of string * string
+
 type tag =
   | Emp_local (* Standard value, variable, expression *)
   | Emp_global (* Variable from global instead of local scope *)
@@ -84,7 +89,7 @@ type tag =
   | Default (* Variable has default type, has not been bound *)
   | Constructor (* Variable is a data constructor *)
   | Enum of int (* Variable came from an enumeration, int tells me the highest possible numeric value *)
-  | Alias (* Variable came from a register alias *)
+  | Alias of alias_inf (* Variable came from a register alias *)
   | Spec (* Variable came from a val specification *)
 
 type constraint_origin =