summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/state.lem59
-rw-r--r--src/gen_lib/state_lifting.lem27
-rw-r--r--src/gen_lib/state_monad.lem14
-rw-r--r--src/pretty_print_lem.ml70
-rw-r--r--src/process_file.ml9
-rw-r--r--src/process_file.mli2
6 files changed, 110 insertions, 71 deletions
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 61477258..6bc304a8 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,33 +1,8 @@
open import Pervasives_extra
-(*open import Sail_impl_base*)
open import Sail_values
-open import Prompt_monad
-open import Prompt
open import State_monad
open import {isabelle} `State_monad_lemmas`
-(* State monad wrapper around prompt monad *)
-
-val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState ra s = match s with
- | (Done a) -> returnS a
- | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
- | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v))
- | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v))
- | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v))
- | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v))
- | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v))
- | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v))
- | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k)
- | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k)
- | (Footprint k) -> liftState ra k
- | (Barrier _ k) -> liftState ra k
- | (Print _ k) -> liftState ra k (* TODO *)
- | (Fail descr) -> failS descr
- | (Exception e) -> throwS e
-end
-
-
val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
let rec iterS_aux i f xs = match xs with
| x :: xs -> f i x >>$ iterS_aux (i + 1) f xs
@@ -53,6 +28,40 @@ end
declare {isabelle} termination_argument foreachS = automatic
+val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e
+let bool_of_bitU_fail = function
+ | B0 -> returnS false
+ | B1 -> returnS true
+ | BU -> failS "bool_of_bitU"
+end
+
+val bool_of_bitU_oracleS : forall 'rv 'e. bitU -> monadS 'rv bool 'e
+let bool_of_bitU_oracleS = function
+ | B0 -> returnS false
+ | B1 -> returnS true
+ | BU -> undefined_boolS ()
+end
+
+val bools_of_bits_oracleS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e
+let bools_of_bits_oracleS bits =
+ foreachS bits []
+ (fun b bools ->
+ bool_of_bitU_oracleS b >>$= (fun b ->
+ returnS (bools ++ [b])))
+
+val of_bits_oracleS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
+let of_bits_oracleS bits =
+ bools_of_bits_oracleS bits >>$= (fun bs ->
+ returnS (of_bools bs))
+
+val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
+let of_bits_failS bits = maybe_failS "of_bits" (of_bits bits)
+
+val mword_oracleS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
+let mword_oracleS () =
+ bools_of_bits_oracleS (repeat [BU] (integerFromNat size)) >>$= (fun bs ->
+ returnS (wordFromBitlist bs))
+
val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
diff --git a/src/gen_lib/state_lifting.lem b/src/gen_lib/state_lifting.lem
new file mode 100644
index 00000000..7e569a7e
--- /dev/null
+++ b/src/gen_lib/state_lifting.lem
@@ -0,0 +1,27 @@
+open import Pervasives_extra
+open import Sail_values
+open import Prompt_monad
+open import Prompt
+open import State_monad
+open import {isabelle} `State_monad_lemmas`
+
+(* State monad wrapper around prompt monad *)
+
+val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
+let rec liftState ra s = match s with
+ | (Done a) -> returnS a
+ | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
+ | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v))
+ | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v))
+ | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v))
+ | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v))
+ | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v))
+ | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v))
+ | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k)
+ | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k)
+ | (Footprint k) -> liftState ra k
+ | (Barrier _ k) -> liftState ra k
+ | (Print _ k) -> liftState ra k (* TODO *)
+ | (Fail descr) -> failS descr
+ | (Exception e) -> throwS e
+end
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index 8253b800..781bc129 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -94,12 +94,12 @@ let assert_expS exp msg = if exp then returnS () else failS msg
(* For early return, we abuse exceptions by throwing and catching
the return value. The exception type is "either 'r 'e", where "Right e"
represents a proper exception and "Left r" an early return of value "r". *)
-type monadSR 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
+type monadRS 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
-val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadSR 'regs 'a 'r 'e
+val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e
let early_returnS r = throwS (Left r)
-val catch_early_returnS : forall 'regs 'a 'e. monadSR 'regs 'a 'a 'e -> monadS 'regs 'a 'e
+val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e
let catch_early_returnS m =
try_catchS m
(function
@@ -108,12 +108,12 @@ let catch_early_returnS m =
end)
(* Lift to monad with early return by wrapping exceptions *)
-val liftSR : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadSR 'regs 'a 'r 'e
-let liftSR m = try_catchS m (fun e -> throwS (Right e))
+val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e
+let liftRS m = try_catchS m (fun e -> throwS (Right e))
(* Catch exceptions in the presence of early returns *)
-val try_catchSR : forall 'regs 'a 'r 'e1 'e2. monadSR 'regs 'a 'r 'e1 -> ('e1 -> monadSR 'regs 'a 'r 'e2) -> monadSR 'regs 'a 'r 'e2
-let try_catchSR m h =
+val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) -> monadRS 'regs 'a 'r 'e2
+let try_catchRS m h =
try_catchS m
(function
| Left r -> throwS (Left r)
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f58c3fa6..a7da28bc 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -62,6 +62,8 @@ open Pretty_print_common
let opt_sequential = ref false
let opt_mwords = ref false
+let appendS str = if !opt_sequential then str ^ "S" else str
+
type context = {
early_ret : bool;
bound_nexps : NexpSet.t;
@@ -551,10 +553,11 @@ let doc_exp_lem, doc_let_lem =
let expY = top_exp ctxt true in
let expN = top_exp ctxt false in
let expV = top_exp ctxt in
+ let wrap_parens doc = if aexp_needed then parens (doc) else doc in
let liftR doc =
if ctxt.early_ret && effectful (effect_of full_exp)
- then separate space [string "liftR"; parens (doc)]
- else doc in
+ then wrap_parens (separate space [string (appendS "liftR"); parens (doc)])
+ else wrap_parens doc in
match e with
| E_assign((LEXP_aux(le_act,tannot) as le), e) ->
(* can only be register writes *)
@@ -571,13 +574,13 @@ let doc_exp_lem, doc_let_lem =
underscore ^^
doc_id_lem id in
liftR ((prefix 2 1)
- (string "write_reg_field_range")
+ (string (appendS "write_reg_field_range"))
(align (doc_lexp_deref_lem ctxt le ^/^
field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
| _ ->
let deref = doc_lexp_deref_lem ctxt le in
liftR ((prefix 2 1)
- (string "write_reg_range")
+ (string (appendS "write_reg_range"))
(align (deref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
| LEXP_vector (le,e2) ->
(match le with
@@ -608,13 +611,13 @@ let doc_exp_lem, doc_let_lem =
dot ^^
string "set_field"*) in
liftR ((prefix 2 1)
- (string "write_reg_field")
+ (string (appendS "write_reg_field"))
(doc_lexp_deref_lem ctxt le ^^ space ^^
field_ref ^/^ expY e))
| LEXP_deref re ->
- liftR ((prefix 2 1) (string "write_reg") (expY re ^/^ expY e))
+ liftR ((prefix 2 1) (string (appendS "write_reg")) (expY re ^/^ expY e))
| _ ->
- liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem ctxt le ^/^ expY e)))
+ liftR ((prefix 2 1) (string (appendS "write_reg")) (doc_lexp_deref_lem ctxt le ^/^ expY e)))
| E_vector_append(le,re) ->
raise (Reporting_basic.err_unreachable l
"E_vector_append should have been rewritten before pretty-printing")
@@ -650,7 +653,11 @@ let doc_exp_lem, doc_let_lem =
parens (separate space [string "integerNegate"; expY exp3])
| _ -> expY exp3
in
- let combinator = if effectful (effect_of body) then "foreachM" else "foreach" in
+ let combinator =
+ if effectful (effect_of body)
+ then if !opt_sequential then "foreachS" else "foreachM"
+ else "foreach"
+ in
let indices_pp = parens (separate space [string "index_list"; expY exp1; expY exp2; step]) in
let used_vars_body = find_e_ids body in
let body_lambda =
@@ -683,12 +690,13 @@ let doc_exp_lem, doc_let_lem =
match args with
| [cond; varstuple; body] ->
let return (E_aux (e, a)) = E_aux (E_internal_return (E_aux (e, a)), a) in
+ let monad_suffix = if !opt_sequential then "S" else "M" in
let csuffix, cond, body =
match effectful (effect_of cond), effectful (effect_of body) with
| false, false -> "", cond, body
- | false, true -> "M", return cond, body
- | true, false -> "M", cond, return body
- | true, true -> "M", cond, body
+ | false, true -> monad_suffix, return cond, body
+ | true, false -> monad_suffix, cond, return body
+ | true, true -> monad_suffix, cond, body
in
let used_vars_body = find_e_ids body in
let lambda =
@@ -719,7 +727,7 @@ let doc_exp_lem, doc_let_lem =
begin
match args with
| [exp] ->
- let epp = separate space [string "early_return"; expY exp] in
+ let epp = separate space [string (appendS "early_return"); expY exp] in
let aexp_needed, tepp =
if contains_t_pp_var ctxt (typ_of exp) ||
contains_t_pp_var ctxt (typ_of full_exp) then
@@ -788,7 +796,7 @@ let doc_exp_lem, doc_let_lem =
let eff = effect_of full_exp in
let base_typ = Env.base_typ_of env typ in
if has_effect eff BE_rreg then
- let epp = separate space [string "read_reg";doc_id_lem (append_id id "_ref")] in
+ let epp = separate space [string (appendS "read_reg");doc_id_lem (append_id id "_ref")] in
if is_bitvector_typ base_typ
then liftR (parens (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env true base_typ)))))
else liftR epp
@@ -874,12 +882,10 @@ let doc_exp_lem, doc_let_lem =
else
raise (Reporting_basic.err_todo l "Warning: try-block around pure expression")
| E_throw e ->
- let epp = liftR (separate space [string "throw"; expY e]) in
- if aexp_needed then parens (align epp) else align epp
- | E_exit e -> liftR (separate space [string "exit"; expY e])
+ align (liftR (separate space [string (appendS "throw"); expY e]))
+ | E_exit e -> liftR (separate space [string (appendS "exit"); expY e])
| E_assert (e1,e2) ->
- let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in
- if aexp_needed then parens (align epp) else align epp
+ align (liftR (separate space [string (appendS "assert_exp"); expY e1; expY e2]))
| E_app_infix (e1,id,e2) ->
raise (Reporting_basic.err_unreachable l
"E_app_infix should have been rewritten before pretty-printing")
@@ -888,26 +894,28 @@ let doc_exp_lem, doc_let_lem =
| E_internal_plet (pat,e1,e2) ->
let epp =
let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
+ let bind_pp = string (if !opt_sequential then ">>$=" else ">>=") in
+ let seq_pp = string (if !opt_sequential then ">>$" else ">>") in
let middle =
match fst (untyp_pat pat) with
- | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) ->
- string ">>"
+ | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> seq_pp
| P_aux (P_tup _, _)
when not (IdSet.mem (mk_id "varstup") (find_e_ids e2)) ->
(* Work around indentation issues in Lem when translating
tuple patterns to Isabelle *)
separate space
- [string ">>= fun varstup -> let";
+ [bind_pp; string "fun varstup -> let";
doc_pat_lem ctxt true pat;
string "= varstup in"]
| _ ->
- separate space [string ">>= fun"; doc_pat_lem ctxt true pat; arrow]
+ separate space [bind_pp; string "fun";
+ doc_pat_lem ctxt true pat; arrow]
in
infix 0 1 middle (expV b e1) (expN e2)
in
if aexp_needed then parens (align epp) else epp
| E_internal_return (e1) ->
- separate space [string "return"; expY e1]
+ wrap_parens (align (separate space [string (appendS "return"); expY e1]))
| E_sizeof nexp ->
(match nexp_simp nexp with
| Nexp_aux (Nexp_constant i, _) -> doc_lit_lem (L_aux (L_num i, l))
@@ -915,15 +923,15 @@ let doc_exp_lem, doc_let_lem =
raise (Reporting_basic.err_unreachable l
"pretty-printing non-constant sizeof expressions to Lem not supported"))
| E_return r ->
- let ret_monad = if !opt_sequential then " : MR regstate" else " : MR" in
+ (* let ret_monad = if !opt_sequential then " : MR regstate" else " : MR" in *)
let ta =
if contains_t_pp_var ctxt (typ_of full_exp) || contains_t_pp_var ctxt (typ_of r)
then empty
else separate space
- [string ret_monad;
+ [string ": MR";
parens (doc_typ_lem (typ_of full_exp));
parens (doc_typ_lem (typ_of r))] in
- align (parens (string "early_return" ^//^ expV true r ^//^ ta))
+ align (parens (string (appendS "early_return") ^//^ expV true r ^//^ ta))
| E_constraint _ -> string "true"
| E_comment _ | E_comment_struc _ -> empty
| E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _
@@ -1250,7 +1258,7 @@ let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with
let doc_fun_body_lem ctxt exp =
let doc_exp = doc_exp_lem ctxt false exp in
if ctxt.early_ret
- then align (string "catch_early_return" ^//^ parens (doc_exp))
+ then align (string (appendS "catch_early_return") ^//^ parens (doc_exp))
else doc_exp
let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) =
@@ -1445,12 +1453,12 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs)
separate empty (List.map doc_def_lem statedefs); hardline;
hardline;
register_refs; hardline;
- (* if !opt_sequential then
+ if !opt_sequential then
concat [
- string ("type MR 'a 'r = State_monad.MR regstate 'a 'r " ^ exc_typ); hardline;
- string ("type M 'a = State_monad.M regstate 'a " ^ exc_typ); hardline;
+ string ("type MR 'a 'r = monadRS regstate 'a 'r " ^ exc_typ); hardline;
+ string ("type M 'a = monadS regstate 'a " ^ exc_typ); hardline;
]
- else *)
+ else
concat [
string ("type MR 'a 'r = monadR register_value 'a 'r " ^ exc_typ); hardline;
string ("type M 'a = monad register_value 'a " ^ exc_typ); hardline
diff --git a/src/process_file.ml b/src/process_file.ml
index 4856c20a..1d4c5f03 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -51,9 +51,6 @@
open PPrint
open Pretty_print_common
-let opt_lem_sequential = ref false
-let opt_lem_mwords = ref false
-
type out_type =
| Lem_ast_out
| Lem_out of string list
@@ -246,10 +243,10 @@ let output_lem filename libs defs =
let generated_line = generated_line filename in
(* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *)
let types_module = (filename ^ "_types") in
- let monad_modules = ["Prompt_monad"; "Prompt"; "State"] in
- (* if !Pretty_print_lem.opt_sequential
+ let monad_modules = (*["Prompt_monad"; "Prompt"; "State"] in*)
+ if !Pretty_print_lem.opt_sequential
then ["State_monad"; "State"]
- else ["Prompt_monad"; "Prompt"] in *)
+ else ["Prompt_monad"; "Prompt"] in
let operators_module =
if !Pretty_print_lem.opt_mwords
then "Sail_operators_mwords"
diff --git a/src/process_file.mli b/src/process_file.mli
index b38b4259..cc94888e 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -65,8 +65,6 @@ val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val load_file_no_check : Ast.order -> string -> unit Ast.defs
val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t
-val opt_lem_sequential : bool ref
-val opt_lem_mwords : bool ref
val opt_just_check : bool ref
val opt_ddump_tc_ast : bool ref
val opt_ddump_rewrite_ast : ((string * int) option) ref
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 19:27:16 +0000