summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile2
-rw-r--r--src/ast_util.ml20
-rw-r--r--src/ast_util.mli3
-rw-r--r--src/pretty_print_lem.ml19
-rw-r--r--src/pretty_print_lem_ast.ml2
-rw-r--r--src/rewriter.ml62
6 files changed, 66 insertions, 42 deletions
diff --git a/src/Makefile b/src/Makefile
index 6cfcf874..1bac0b71 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -177,7 +177,7 @@ _build/cheri_embed_types_sequential.lem: $(CHERI_SAILS) ./sail.native
_build/Cheri_embed_sequential.thy: _build/cheri_embed_types_sequential.lem
cd _build ;\
- lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem
+ lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem
_build/mips_all.sail: $(MIPS_SAILS)
cat $(MIPS_SAILS) > $@
diff --git a/src/ast_util.ml b/src/ast_util.ml
index aef1a05d..2f630021 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -618,6 +618,22 @@ let rec simplify_nexp (Nexp_aux (nexp, l)) =
| Nexp_exp of nexp (* exponential *)
| Nexp_neg of nexp (* For internal use *) *)
+let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) =
+ let rewrap e_aux = E_aux (e_aux, annot) in
+ match lexp_aux with
+ | LEXP_id id | LEXP_cast (_, id) -> rewrap (E_id id)
+ | LEXP_tup les ->
+ let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with
+ | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot)
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in
+ rewrap (E_tuple (List.map get_id les))
+ | LEXP_vector (lexp, e) -> rewrap (E_vector_access (lexp_to_exp lexp, e))
+ | LEXP_vector_range (lexp, e1, e2) -> rewrap (E_vector_subrange (lexp_to_exp lexp, e1, e2))
+ | LEXP_field (lexp, id) -> rewrap (E_field (lexp_to_exp lexp, id))
+ | LEXP_memory (id, exps) -> rewrap (E_app (id, exps))
+
let rec is_number (Typ_aux (t,_)) =
match t with
| Typ_app (Id_aux (Id "range", _),_)
@@ -625,6 +641,10 @@ let rec is_number (Typ_aux (t,_)) =
| Typ_app (Id_aux (Id "atom", _),_) -> true
| _ -> false
+let is_reftyp (Typ_aux (typ_aux, _)) = match typ_aux with
+ | Typ_app (id, _) -> string_of_id id = "register" || string_of_id id = "reg"
+ | _ -> false
+
let rec is_vector_typ = function
| Typ_aux (Typ_app (Id_aux (Id "vector",_), [_;_;_;_]), _) -> true
| Typ_aux (Typ_app (Id_aux (Id "register",_), [Typ_arg_aux (Typ_arg_typ rtyp,_)]), _) ->
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 6164fc17..246e0ebd 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -203,7 +203,10 @@ val nexp_identical : nexp -> nexp -> bool
val is_nexp_constant : nexp -> bool
val simplify_nexp : nexp -> nexp
+val lexp_to_exp : 'a lexp -> 'a exp
+
val is_number : typ -> bool
+val is_reftyp : typ -> bool
val is_vector_typ : typ -> bool
val is_bit_typ : typ -> bool
val is_bitvector_typ : typ -> bool
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 5e0d39a0..e2c8c0ac 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -418,10 +418,21 @@ let doc_exp_lem, doc_let_lem =
(align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
parens (string "update_reg_field_bit" ^/^ field_ref ^/^ expY e2) ^/^ expY e)))
| _ ->
- liftR ((prefix 2 1)
- (string "update_reg")
- (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
- parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e))
+ (match le with
+ | LEXP_aux (_, (_, Some (_, Typ_aux (Typ_app (vector, [_; _; _; Typ_arg_aux (Typ_arg_typ etyp, _)]), _), _)))
+ when is_reftyp etyp && string_of_id vector = "vector" ->
+ (* Special case vectors of register references *)
+ let deref =
+ parens (separate space [
+ string "access";
+ expY (lexp_to_exp le);
+ expY e2
+ ]) in
+ liftR ((prefix 2 1) (string "write_reg") (deref ^/^ expY e))
+ | _ ->
+ liftR ((prefix 2 1) (string "update_reg")
+ (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+ parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e)))
)
(* | LEXP_field (le,id) when is_bit_typ t ->
liftR ((prefix 2 1)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 68745bf9..73f06d1a 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -210,7 +210,7 @@ and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) =
(match t with
| Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
| Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
- | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")") ^
+ | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")") ^ " " ^
(pp_format_l_lem l) ^ ")"
and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
"(NC_aux " ^
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 78b29200..d6a6aa2f 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2209,29 +2209,19 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
| Some (_, _, eff) -> effectful_effs eff
| _ -> false
-let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = match lexp with
- | LEXP_id id | LEXP_cast (_, id) ->
- (le, E_aux (E_id id, annot), (fun exp -> exp))
- | LEXP_tup les ->
- let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with
- | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot)
- | _ ->
- raise (Reporting_basic.err_unreachable l
- ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in
- (le, E_aux (E_tuple (List.map get_id les), annot), (fun exp -> exp))
+let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) =
+ match lexp with
+ | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ -> (le, (fun exp -> exp))
| LEXP_vector (lexp, e) ->
- let (lexp, access, rexp) = rewrite_local_lexp lexp in
- (lexp, E_aux (E_vector_access (access, e), annot),
- (fun exp -> rexp (E_aux (E_vector_update (access, e, exp), annot))))
+ let (lhs, rhs) = rewrite_local_lexp lexp in
+ (lhs, (fun exp -> rhs (E_aux (E_vector_update (lexp_to_exp lexp, e, exp), annot))))
| LEXP_vector_range (lexp, e1, e2) ->
- let (lexp, access, rexp) = rewrite_local_lexp lexp in
- (lexp, E_aux (E_vector_subrange (access, e1, e2), annot),
- (fun exp -> rexp (E_aux (E_vector_update_subrange (access, e1, e2, exp), annot))))
+ let (lhs, rhs) = rewrite_local_lexp lexp in
+ (lhs, (fun exp -> rhs (E_aux (E_vector_update_subrange (lexp_to_exp lexp, e1, e2, exp), annot))))
| LEXP_field (lexp, id) ->
- let (lexp, access, rexp) = rewrite_local_lexp lexp in
+ let (lhs, rhs) = rewrite_local_lexp lexp in
let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
- (lexp, E_aux (E_field (access, id), annot),
- (fun exp -> rexp (E_aux (E_record_update (access, field_update exp), annot))))
+ (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), annot))))
| _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
(*Expects to be called after rewrite_defs; thus the following should not appear:
@@ -2250,7 +2240,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
| [] -> []
| (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps
when lexp_is_local_intro le env && not (lexp_is_effectful le) ->
- let (le', _, re') = rewrite_local_lexp le in
+ let (le', re') = rewrite_local_lexp le in
let e' = re' (rewrite_base e) in
let exps' = walker exps in
let effects = union_eff_exps exps' in
@@ -2303,7 +2293,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
rewrap (E_block (walker exps))
| E_assign(le,e)
when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) ->
- let (le', _, re') = rewrite_local_lexp le in
+ let (le', re') = rewrite_local_lexp le in
let e' = re' (rewrite_base e) in
let block = E_aux (E_block [], simple_annot l unit_typ) in
fix_eff_exp (E_aux (E_internal_let(le', e', block), annot))
@@ -2635,7 +2625,7 @@ let rewrite_simple_assignments defs =
let env = env_of_annot annot in
match e_aux with
| E_assign (lexp, exp) ->
- let (lexp, _, rhs) = rewrite_local_lexp lexp in
+ let (lexp, rhs) = rewrite_local_lexp lexp in
let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in
check_exp env assign unit_typ
| _ -> E_aux (e_aux, annot)
@@ -2977,9 +2967,9 @@ let rewrite_defs_effectful_let_expressions =
let e_let (lb,body) =
match lb with
| LB_aux (LB_val_implicit (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _)
- when lexp_is_local le (env_of_annot annot) ->
+ when lexp_is_local le (env_of_annot annot) && not (lexp_is_effectful le) ->
(* Rewrite assignments to local variables into let bindings *)
- let (lhs, _, rhs) = rewrite_local_lexp le in
+ let (lhs, rhs) = rewrite_local_lexp le in
E_let (LB_aux (LB_val_implicit (pat_of_local_lexp lhs, rhs exp), annot), body)
| LB_aux (LB_val_explicit (_,pat,exp'),annot')
| LB_aux (LB_val_implicit (pat,exp'),annot') ->
@@ -3023,28 +3013,28 @@ let eqidtyp (id1,_) (id2,_) =
name1 = name2
let find_introduced_vars exp =
- let lEXP_aux ((ids,lexp),annot) =
- let ids = match lexp, annot with
- | LEXP_id id, (_, Some (env, _, _))
- | LEXP_cast (_, id), (_, Some (env, _, _))
+ let e_aux ((ids,e_aux),annot) =
+ let ids = match e_aux, annot with
+ | E_internal_let (LEXP_aux (LEXP_id id, _), _, _), (_, Some (env, _, _))
+ | E_internal_let (LEXP_aux (LEXP_cast (_, id), _), _, _), (_, Some (env, _, _))
when id_is_unbound id env -> IdSet.add id ids
| _ -> ids in
- (ids, LEXP_aux (lexp, annot)) in
+ (ids, E_aux (e_aux, annot)) in
fst (fold_exp
- { (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp)
+ { (compute_exp_alg IdSet.empty IdSet.union) with e_aux = e_aux } exp)
let find_updated_vars exp =
let intros = find_introduced_vars exp in
- let lEXP_aux ((ids,lexp),annot) =
- let ids = match lexp, annot with
- | LEXP_id id, (_, Some (env, _, _))
- | LEXP_cast (_, id), (_, Some (env, _, _))
+ let e_aux ((ids,e_aux),annot) =
+ let ids = match e_aux, annot with
+ | E_assign (LEXP_aux (LEXP_id id, _), _), (_, Some (env, _, _))
+ | E_assign (LEXP_aux (LEXP_cast (_, id), _), _), (_, Some (env, _, _))
when id_is_local_var id env && not (IdSet.mem id intros) ->
(id, annot) :: ids
| _ -> ids in
- (ids, LEXP_aux (lexp, annot)) in
+ (ids, E_aux (e_aux, annot)) in
dedup eqidtyp (fst (fold_exp
- { (compute_exp_alg [] (@)) with lEXP_aux = lEXP_aux } exp))
+ { (compute_exp_alg [] (@)) with e_aux = e_aux } exp))
let swaptyp typ (l,tannot) = match tannot with
| Some (env, typ', eff) -> (l, Some (env, typ, eff))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 16:27:28 +0000