summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/sail_values.lem19
-rw-r--r--src/gen_lib/vector.lem5
-rw-r--r--src/pretty_print.ml49
-rw-r--r--src/rewriter.ml80
4 files changed, 89 insertions, 64 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index bd295616..c47e763f 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -13,11 +13,14 @@ let get_elements (Vector elements _) = elements
let get_start (Vector _ s) = s
let length (Vector bs _) = length bs
+let rec nth n xs = match (n,l) with
+ | (0,x :: xs) -> x
+ | (n + 1,x :: xs) -> nth n xs
+end
let vector_access (Vector bs start) n =
- let (Just b) = if is_inc then List.index bs (n - start)
- else List.index bs (start - n) in
- b
+ if is_inc then nth bs (n - start) else nth bs (start - n)
+
let write_two_registers r1 r2 vec =
let size = length_register r1 in
@@ -130,11 +133,11 @@ let rec divide_by_2 bs i (n : integer) =
let rec add_one_bit bs co i =
if i < 0 then bs
- else match (List.index bs i,co) with
- | (Just B0,false) -> replace bs (i,B1)
- | (Just B0,true) -> add_one_bit (replace bs (i,B1)) true (i-1)
- | (Just B1, false) -> add_one_bit (replace bs (i,B0)) true (i-1)
- | (Just B1, true) -> add_one_bit bs true (i-1)
+ else match (nth bs i,co) with
+ | (B0,false) -> replace bs (i,B1)
+ | (B0,true) -> add_one_bit (replace bs (i,B1)) true (i-1)
+ | (B1,false) -> add_one_bit (replace bs (i,B0)) true (i-1)
+ | (B1,true) -> add_one_bit bs true (i-1)
(* | Vundef,_ -> assert false*)
end
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index fe70c9c0..75628f45 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -4,11 +4,6 @@ type bit = B0 | B1 | BU
type vector = Vector of list bit * nat
-let vector_access (Vector bs start) n =
- let (Just b) = if is_inc then List.index bs (n - start)
- else List.index bs (start - n) in
- b
-
let read_vector_subrange is_inc (Vector bs start) n m =
let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
let (_,suffix) = List.splitAt offset bs in
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 9b1bf6f7..07f931de 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1940,12 +1940,12 @@ let doc_exp_lem, doc_let_lem =
| E_assign((LEXP_aux(le_act,tannot) as le),e) ->
(match annot with
| Base(_,(Emp_local | Emp_set),_,_,_,_) ->
- (match le_act with
+ (match le_act with
| LEXP_id _ | LEXP_cast _ ->
(*Setting local variable fully *)
- doc_op coloneq (doc_lexp_lem true le) (exp e)
+ doc_op coloneq (doc_lexp_lem true le) (exp e)
| LEXP_vector _ ->
- doc_op (string "<-") (doc_lexp_array_lem le) (exp e)
+ separate space [string "write_register";parens (doc_lexp_array_lem le);exp e]
| LEXP_vector_range _ ->
doc_lexp_rwrite le e)
| _ ->
@@ -2158,14 +2158,9 @@ let doc_exp_lem, doc_let_lem =
match lexp with
| LEXP_vector(v,e) -> doc_lexp_array_lem le
| LEXP_vector_range(v,e1,e2) ->
- parens ((string "vector_subrange") ^^ space ^^ (doc_lexp_lem false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2))
+ parens (string "vector_subrange" ^^ space ^^ (doc_lexp_lem false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2))
| LEXP_field(v,id) -> (doc_lexp_lem false v) ^^ dot ^^ doc_id_lem id
- | LEXP_id id | LEXP_cast(_,id) ->
- let name = doc_id_lem id in
- match annot,top_call with
- | Base((_,{t=Tapp("reg",_)}),Emp_set,_,_,_,_),false | Base((_,{t=Tabbrev(_,{t=Tapp("reg",_)})}),Emp_set,_,_,_,_),false ->
- string "!" ^^ name
- | _ -> name
+ | LEXP_id id | LEXP_cast(_,id) -> doc_id_lem id
and doc_lexp_array_lem ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
| LEXP_vector(v,e) ->
@@ -2175,12 +2170,15 @@ let doc_exp_lem, doc_let_lem =
(match t_act.t with
| Tid "bit"
| Tabbrev(_,{t=Tid "bit"}) ->
- parens (string "get_elements" ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^
- parens (top_exp e)
- | _ -> parens (string "get_elements" ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^
- parens (top_exp e))
+ separate space [string "nth";
+ parens (string "get_elements" ^^ space ^^ doc_lexp_lem false v);
+ parens (top_exp e)]
+ | _ ->
+ separate space [string "nth";
+ parens (string "get_elements" ^^ space ^^ doc_lexp_lem false v);
+ parens (top_exp e)]
| _ ->
- parens ((string "get_varray") ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^ parens (top_exp e))
+ parens ((string "get_elements") ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^ parens (top_exp e)))
| _ -> empty
and doc_lexp_rwrite ((LEXP_aux(lexp,(l,annot))) as le) e_new_v =
@@ -2199,12 +2197,12 @@ let doc_exp_lem, doc_let_lem =
| _ -> (false,false) in
match lexp with
| LEXP_vector(v,e) ->
- doc_op (string "<-")
+ doc_op (string "write_register")
(group (parens (string "get_elements" ^^ space ^^ doc_lexp_lem false v)) ^^
dot ^^ parens (exp e))
(exp e_new_v)
| LEXP_vector_range(v,e1,e2) ->
- parens (string "write_vector_subrange" ^^ space ^^
+ parens (string "write_register_subrange" ^^ space ^^
doc_lexp_lem false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v)
| LEXP_field(v,id) ->
parens (string "write_register" ^^ space ^^
@@ -2219,7 +2217,7 @@ let doc_exp_lem, doc_let_lem =
| Alias_extract(reg,start,stop) ->
if start = stop
then
- doc_op (string "<-")
+ doc_op (string "write_register")
(group (parens (string "get_elements" ^^ space ^^ string reg)) ^^
dot ^^ parens (doc_int start))
(exp e_new_v)
@@ -2322,7 +2320,14 @@ let doc_def_lem def = match def with
-let reg_decls defs =
+let reg_decls (Defs defs) =
+
+ let dirpp =
+ let b = match Spec_analysis.default_order (Defs defs) with
+ | {order = Oinc} -> "true"
+ | {order = Odec} -> "false"
+ | {order = _} -> failwith "Can't deal with variable order" in
+ separate space [string "let";string "is_inc";equals;string "true"] in
let (regtyps,typedregs,simpleregs,defs) =
List.fold_left
@@ -2342,8 +2347,6 @@ let reg_decls defs =
Nexp_aux (Nexp_constant 63,Unknown),
name) in
- let dirpp = separate space [string "let";string "is_inc";equals;string "true"] in
-
let reg_decls =
(List.map default simpleregs) @
List.fold_left
@@ -2489,8 +2492,8 @@ let reg_decls defs =
(separate (hardline ^^ hardline) [dirpp;regspp;statepp;lengthpp;read_register_pp;write_register_pp],defs)
-let doc_defs_lem (Defs(defs)) =
- let (decls,defs) = reg_decls defs in
+let doc_defs_lem (Defs defs) =
+ let (decls,defs) = reg_decls (Defs defs) in
(decls,separate_map empty doc_def_lem defs)
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 68bb2c2a..2a9782ba 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1000,12 +1000,9 @@ let remove_blocks_exp_alg =
let rec f = function
| [e] -> e (* check with Kathy if that annotation is fine *)
- | e :: es -> letbind_wild e (f es)
- | e -> E_aux (E_lit (L_aux (L_unit,Unknown)), (Unknown,simple_annot ({t = Tid "unit"}))) in
-(*
- | [] -> E_aux (E_lit (L_aux (L_unit,Unknown)), (Unknown,simple_annot ({t = Tid "unit"})))
+ | e -> E_aux (E_lit (L_aux (L_unit,Unknown)), (Unknown,simple_annot ({t = Tid "unit"})))
| e :: es -> letbind_wild e (f es) in
- *)
+
let e_aux = function
| (E_block es,annot) -> f es
| (e,annot) -> E_aux (e,annot) in
@@ -1043,7 +1040,7 @@ let rec value ((E_aux (exp_aux,_)) as exp) =
| E_tuple es
| E_vector es
| E_list es -> List.fold_left (&&) true (List.map value es)
- | _ -> false
+ | _ -> false
let only_local_eff (l,(Base ((t_params,t),tag,nexps,eff,effsum,bounds))) =
(l,Base ((t_params,t),tag,nexps,eff,eff,bounds))
@@ -1059,6 +1056,9 @@ let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list
let rec n_exp_name (exp : 'a exp) (k : 'a exp -> 'a exp) : 'a exp =
n_exp exp (fun exp -> if value exp then k exp else letbind exp k)
+
+and n_exp_pure (exp : 'a exp) (k : 'a exp -> 'a exp) : 'a exp =
+ n_exp exp (fun exp -> if not (effectful exp) then k exp else letbind exp k)
and n_exp_nameL (exps : 'a exp list) (k : 'a exp list -> 'a exp) : 'a exp =
mapCont n_exp_name exps k
@@ -1128,7 +1128,7 @@ and n_exp_term (new_return : bool) (exp : 'a exp) : 'a exp =
(* changed this from n_exp to n_exp_name so that when we return updated variables
* from a for-loop, for example, we can just add those into the returned tuple and
* don't need to a-normalise again *)
- n_exp exp (fun exp -> exp)
+ n_exp_pure exp (fun exp -> exp)
and n_exp (exp : 'a exp) (k : 'a exp -> 'a exp) : 'a exp =
@@ -1226,6 +1226,7 @@ and n_exp (exp : 'a exp) (k : 'a exp -> 'a exp) : 'a exp =
n_exp_name exp1 (fun exp1 ->
k (rewrap_localeff (E_field (exp1,id))))
| E_case (exp1,pexps) ->
+ (* PROBABLY NEED to insert E_returns here *)
n_exp_name exp1 (fun exp1 ->
n_pexpL pexps (fun pexps ->
let geteffs (Pat_aux (_,(_,Base (_,_,_,_,eff,_)))) = eff in
@@ -1308,7 +1309,11 @@ let find_updated_vars exp =
; e_field = (fun (e1,id) -> e1)
; e_case = (fun (e1,pexps) -> e1 @ List.flatten pexps)
; e_let = (fun (lb,e2) -> lb @ e2)
- ; e_assign = (fun ((None,[(id,b)]),e2) -> if b then id :: e2 else e2)
+ ; e_assign =
+ (function
+ | ((None,[(id,b)]),e2) -> if b then id :: e2 else e2
+ | ((None,[]),e2) -> e2
+ )
; e_exit = (fun e1 -> e1)
; e_internal_cast = (fun (_,e1) -> e1)
; e_internal_exp = (fun _ -> [])
@@ -1511,9 +1516,11 @@ let rec rewrite_for_if_case ((E_aux (expaux,annot)) as exp) =
| _ -> exp
-let replace_e_assign =
+let replace_var_update_e_assign =
let e_aux (expaux,annot) =
+
+ let f v body lexp =
let letbind (E_aux (E_id id,_) as e_id) (v : 'a exp) (body : 'a exp) : 'a exp =
(* body is a function : E_id variable -> actual body *)
@@ -1523,40 +1530,57 @@ let replace_e_assign =
let annot_let = (Parse_ast.Unknown,simple_annot_efr (gettype body) (geteffs body)) in
let pat = P_aux (P_id id,annot_pat) in
E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let) in
-
- let f v body = function
- | LEXP_aux (LEXP_id id,annot) ->
- let eid = E_aux (E_id id,(Unknown,simple_annot (gettype v))) in
- letbind eid v body
- | LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,annot2),i),annot) ->
- let eid = E_aux (E_id id,(Unknown,simple_annot (gettype_annot annot2))) in
- let v = E_aux (E_vector_update (eid,i,v),(Unknown,simple_annot (gettype_annot annot))) in
- letbind eid v body
- | LEXP_aux (LEXP_vector_range (LEXP_aux (LEXP_id id,annot2),i,j),annot) ->
- let eid = E_aux (E_id id,(Unknown,simple_annot (gettype_annot annot2))) in
- let v = E_aux (E_vector_update_subrange (eid,i,j,v),
- (Unknown,simple_annot (gettype_annot annot))) in
- letbind eid v body in
+
+ match lexp with
+ | LEXP_aux (LEXP_id id,annot) ->
+ let eid = E_aux (E_id id,(Unknown,simple_annot (gettype v))) in
+ letbind eid v body
+ | LEXP_aux (LEXP_cast (_,id),annot) ->
+ let eid = E_aux (E_id id,(Unknown,simple_annot (gettype v))) in
+ letbind eid v body
+ | LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,annot2),i),annot) ->
+ let eid = E_aux (E_id id,(Unknown,simple_annot (gettype_annot annot2))) in
+ let v = E_aux (E_vector_update (eid,i,v),(Unknown,simple_annot (gettype_annot annot))) in
+ letbind eid v body
+ | LEXP_aux (LEXP_vector_range (LEXP_aux (LEXP_id id,annot2),i,j),annot) ->
+ let eid = E_aux (E_id id,(Unknown,simple_annot (gettype_annot annot2))) in
+ let v = E_aux (E_vector_update_subrange (eid,i,j,v),
+ (Unknown,simple_annot (gettype_annot annot))) in
+ letbind eid v body in
match expaux with
| E_let (LB_aux (LB_val_explicit (_,_,E_aux (E_assign (lexp,v),annot2)),_),body)
| E_let (LB_aux (LB_val_implicit (_,E_aux (E_assign (lexp,v),annot2)),_),body)
- when
- let {effect = Eset effs} = geteffs_annot annot2 in
- List.exists (function BE_aux (BE_lset,_) -> true | _ -> false) effs ->
+ when let {effect = Eset effs} = geteffs_annot annot2 in
+ List.exists (function BE_aux (BE_lset,_) -> true | _ -> false) effs ->
f v body lexp
| E_let (lb,body) -> E_aux (E_let (lb,body),annot)
(* E_internal_plet is only used for effectful terms, shouldn't be needed to deal with here *)
| E_internal_let (LEXP_aux ((LEXP_id id | LEXP_cast (_,id)),_),v,body) ->
let (E_aux (_,pannot)) = v in
let lbannot = (Parse_ast.Unknown,simple_annot_efr (gettype body) (geteffs body)) in
- E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id,pannot),v),lbannot),body),annot)
+ E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id,pannot),v),lbannot),body),annot)
+ | E_assign (lexp,v)
+ when let {effect = Eset effs} = geteffs_annot annot in
+ List.exists (function BE_aux (BE_lset,_) -> true | _ -> false) effs ->
+ f v (E_aux (E_lit (L_aux (L_unit,Unknown)), (Unknown,simple_annot ({t = Tid "unit"})))) lexp
+
+
| _ -> E_aux (expaux,annot) in
{ id_exp_alg with e_aux = e_aux }
+let replace_memwrite_e_assign =
+ let e_aux = fun (expaux,annot) ->
+ match expaux with
+ | E_assign (LEXP_aux (LEXP_memory (id,args),_),v) -> E_aux (E_app (id,args @ [v]),annot)
+ | _ -> E_aux (expaux,annot) in
+ { id_exp_alg with e_aux = e_aux }
+
let rewrite_defs_remove_e_assign =
- let rewrite_exp _ _ e = (fold_exp replace_e_assign) (rewrite_for_if_case e) in
+ let rewrite_exp _ _ e =
+ (fold_exp replace_memwrite_e_assign)
+ ((fold_exp replace_var_update_e_assign) (rewrite_for_if_case e)) in
rewrite_defs_base
{rewrite_exp = rewrite_exp
; rewrite_pat = rewrite_pat
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:44:39 +0000