summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/.merlin2
-rw-r--r--src/c_backend.ml59
-rw-r--r--src/gen_lib/prompt_monad.lem2
-rw-r--r--src/gen_lib/sail_values.lem12
-rw-r--r--src/gen_lib/state.lem24
-rw-r--r--src/monomorphise.ml18
-rw-r--r--src/state.ml2
7 files changed, 91 insertions, 28 deletions
diff --git a/src/.merlin b/src/.merlin
index 14aeec34..b9fefd29 100644
--- a/src/.merlin
+++ b/src/.merlin
@@ -2,7 +2,7 @@ S .
S lem_interp/
B _build/
B _build/lem_interp/
-B pprint/src/_build
+B _build/pprint/src/
PKG zarith
PKG linksem
PKG lem \ No newline at end of file
diff --git a/src/c_backend.ml b/src/c_backend.ml
index fa1f2b5e..adc44820 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -138,6 +138,9 @@ type aexp =
| AE_record_update of aval * aval Bindings.t * typ
| AE_for of id * aexp * aexp * aexp * order * aexp
| AE_loop of loop * aexp * aexp
+ | AE_short_circuit of sc_op * aval * aexp
+
+and sc_op = SC_and | SC_or
and apat =
| AP_tup of apat list
@@ -212,6 +215,7 @@ let rec aexp_rename from_id to_id aexp =
| AE_for (id, aexp1, aexp2, aexp3, order, aexp4) when Id.compare from_id to_id = 0 -> AE_for (id, aexp1, aexp2, aexp3, order, aexp4)
| AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> AE_for (id, recur aexp1, recur aexp2, recur aexp3, order, recur aexp4)
| AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, recur aexp1, recur aexp2)
+ | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval_rename from_id to_id aval, recur aexp)
and apexp_rename from_id to_id (apat, aexp1, aexp2) =
if IdSet.mem from_id (apat_bindings apat) then
@@ -251,6 +255,7 @@ let rec no_shadow ids aexp =
let ids = IdSet.add id ids in
AE_for (id, no_shadow ids aexp1, no_shadow ids aexp2, no_shadow ids aexp3, order, no_shadow ids aexp4)
| AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, no_shadow ids aexp1, no_shadow ids aexp2)
+ | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, no_shadow ids aexp)
and no_shadow_apexp ids (apat, aexp1, aexp2) =
let shadows = IdSet.inter (apat_bindings apat) ids in
@@ -283,12 +288,14 @@ let rec map_aval f = function
AE_case (f aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ)
| AE_try (aexp, cases, typ) ->
AE_try (map_aval f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ)
+ | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, f aval, map_aval f aexp)
(* Map over all the functions in an aexp. *)
let rec map_functions f = function
| AE_app (id, vs, typ) -> f id vs typ
| AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ)
| AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_functions f aexp)
+ | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, map_functions f aexp)
| AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_functions f aexp1, map_functions f aexp2, typ2)
| AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ)
| AE_if (aval, aexp1, aexp2, typ) ->
@@ -337,6 +344,10 @@ let rec pp_aexp = function
pp_annot typ (pp_id id) ^^ string " := " ^^ pp_aexp aexp
| AE_app (id, args, typ) ->
pp_annot typ (pp_id id ^^ parens (separate_map (comma ^^ space) pp_aval args))
+ | AE_short_circuit (SC_or, aval, aexp) ->
+ pp_aval aval ^^ string " || " ^^ pp_aexp aexp
+ | AE_short_circuit (SC_and, aval, aexp) ->
+ pp_aval aval ^^ string " && " ^^ pp_aexp aexp
| AE_let (id, id_typ, binding, body, typ) -> group
begin
match binding with
@@ -455,6 +466,9 @@ let rec apat_globals = function
let rec anf (E_aux (e_aux, exp_annot) as exp) =
let to_aval = function
| AE_val v -> (v, fun x -> x)
+ | AE_short_circuit (_, _, _) as aexp ->
+ let id = gensym () in
+ (AV_id (id, Local (Immutable, bool_typ)), fun x -> AE_let (id, bool_typ, aexp, x, typ_of exp))
| AE_app (_, _, typ)
| AE_let (_, _, _, _, typ)
| AE_return (_, typ)
@@ -536,6 +550,18 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) =
let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in
exp_wrap (wrap (AE_record_update (aval, record, typ_of exp)))
+ | E_app (id, [exp1; exp2]) when string_of_id id = "and_bool" ->
+ let aexp1 = anf exp1 in
+ let aexp2 = anf exp2 in
+ let aval1, wrap = to_aval aexp1 in
+ wrap (AE_short_circuit (SC_and, aval1, aexp2))
+
+ | E_app (id, [exp1; exp2]) when string_of_id id = "or_bool" ->
+ let aexp1 = anf exp1 in
+ let aexp2 = anf exp2 in
+ let aval1, wrap = to_aval aexp1 in
+ wrap (AE_short_circuit (SC_or, aval1, aexp2))
+
| E_app (id, exps) ->
let aexps = List.map anf exps in
let avals = List.map to_aval aexps in
@@ -1606,6 +1632,29 @@ let rec compile_aexp ctx = function
(fun clexp -> icopy clexp (F_id gs, ctyp)),
gs_cleanup
+ | AE_short_circuit (SC_and, aval, aexp) ->
+ let left_setup, cval, left_cleanup = compile_aval ctx aval in
+ let right_setup, _, call, right_cleanup = compile_aexp ctx aexp in
+ let gs = gensym () in
+ left_setup
+ @ [ idecl CT_bool gs;
+ iif cval (right_setup @ [call (CL_id gs)] @ right_cleanup) [icopy (CL_id gs) (F_lit "false", CT_bool)] CT_bool ]
+ @ left_cleanup,
+ CT_bool,
+ (fun clexp -> icopy clexp (F_id gs, CT_bool)),
+ []
+ | AE_short_circuit (SC_or, aval, aexp) ->
+ let left_setup, cval, left_cleanup = compile_aval ctx aval in
+ let right_setup, _, call, right_cleanup = compile_aexp ctx aexp in
+ let gs = gensym () in
+ left_setup
+ @ [ idecl CT_bool gs;
+ iif cval [icopy (CL_id gs) (F_lit "true", CT_bool)] (right_setup @ [call (CL_id gs)] @ right_cleanup) CT_bool ]
+ @ left_cleanup,
+ CT_bool,
+ (fun clexp -> icopy clexp (F_id gs, CT_bool)),
+ []
+
| AE_assign (id, assign_typ, aexp) ->
(* assign_ctyp is the type of the C variable we are assigning to,
ctyp is the type of the C expression being assigned. These may
@@ -2786,9 +2835,6 @@ let codegen_def' ctx = function
| _ -> assert false
in
let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in
- prerr_endline (string_of_id id);
- prerr_endline (Util.string_of_list ", " (fun arg -> sgen_id arg) args);
- prerr_endline (Util.string_of_list ", " (fun ctyp -> sgen_ctyp ctyp) arg_ctyps);
let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in
let function_header =
match ret_arg with
@@ -2888,7 +2934,7 @@ let compile_ast ctx (Defs defs) =
let postamble = separate hardline (List.map string
( [ "int main(void)";
"{";
- " setup_real();" ]
+ " setup_library();" ]
@ fst exn_boilerplate
@ List.concat (List.map (fun r -> fst (register_init_clear r)) regs)
@ (if regs = [] then [] else [ " zinitializze_registers(UNIT);" ])
@@ -2897,8 +2943,9 @@ let compile_ast ctx (Defs defs) =
@ letbind_finalizers
@ List.concat (List.map (fun r -> snd (register_init_clear r)) regs)
@ snd exn_boilerplate
- @ [ " return 0;" ]
- @ [ "}" ] ))
+ @ [ " cleanup_library();";
+ " return 0;";
+ "}" ] ))
in
let hlhl = hardline ^^ hardline in
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
index ff5e3726..38f79868 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/prompt_monad.lem
@@ -125,7 +125,7 @@ let write_mem_val v = match bytes_of_bits v with
| Just v ->
let k successful = (return successful) in
Write_memv (List.reverse v) k
- | Nothing -> fail "write_mem_val"
+ | Nothing -> Fail "write_mem_val"
end
val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 33caac37..b981bb91 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -379,11 +379,13 @@ end
(* just_list takes a list of maybes and returns Just xs if all elements have
a value, and Nothing if one of the elements is Nothing. *)
val just_list : forall 'a. list (maybe 'a) -> maybe (list 'a)
-let rec just_list [] = Just []
-and just_list (x :: xs) =
- match (x, just_list xs) with
- | (Just x, Just xs) -> Just (x :: xs)
- | (_, _) -> Nothing
+let rec just_list l = match l with
+ | [] -> Just []
+ | (x :: xs) ->
+ match (x, just_list xs) with
+ | (Just x, Just xs) -> Just (x :: xs)
+ | (_, _) -> Nothing
+ end
end
declare {isabelle} termination_argument just_list = automatic
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 4675428e..fba8d9b7 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -9,17 +9,19 @@ open import {isabelle} `State_monad_extras`
(* 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 _ (Done a) = returnS a
-and liftState ra (Read_mem rk a sz k) = bindS (read_memS rk a sz) (fun v -> liftState ra (k v))
-and liftState ra (Write_memv descr k) = bindS (write_mem_valS descr) (fun v -> liftState ra (k v))
-and liftState ra (Read_reg descr k) = bindS (read_regvalS ra descr) (fun v -> liftState ra (k v))
-and liftState ra (Excl_res k) = bindS (excl_resultS ()) (fun v -> liftState ra (k v))
-and liftState ra (Write_ea wk a sz k) = seqS (write_mem_eaS wk a sz) (liftState ra k)
-and liftState ra (Write_reg r v k) = seqS (write_regvalS ra r v) (liftState ra k)
-and liftState ra (Barrier _ k) = liftState ra k
-and liftState _ (Fail descr) = failS descr
-and liftState _ (Error descr) = failS descr
-and liftState _ (Exception e) = throwS e
+let rec liftState ra s = match s with
+ | (Done a) -> returnS a
+ | (Read_mem rk a sz k) -> bindS (read_memS rk a sz) (fun v -> liftState ra (k v))
+ | (Write_memv descr k) -> bindS (write_mem_valS descr) (fun v -> liftState ra (k v))
+ | (Read_reg descr k) -> bindS (read_regvalS ra descr) (fun v -> liftState ra (k v))
+ | (Excl_res k) -> bindS (excl_resultS ()) (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)
+ | (Barrier _ k) -> liftState ra k
+ | (Fail descr) -> failS descr
+ | (Error descr) -> failS descr
+ | (Exception e) -> throwS e
+end
(* TODO
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index d14097af..2fe7cc33 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -993,6 +993,20 @@ let stop_at_false_assertions e =
let l = Generated Unknown in
E_aux (E_exit (E_aux (E_lit (L_aux (L_unit,l)),(l,None))),(l,None))
in
+ let rec nc_false (NC_aux (nc,_)) =
+ match nc with
+ | NC_false -> true
+ | NC_and (nc1,nc2) -> nc_false nc1 || nc_false nc2
+ | _ -> false
+ in
+ let rec exp_false (E_aux (e,_)) =
+ match e with
+ | E_constraint nc -> nc_false nc
+ | E_lit (L_aux (L_false,_)) -> true
+ | E_app (Id_aux (Id "and_bool",_),[e1;e2]) ->
+ exp_false e1 || exp_false e2
+ | _ -> false
+ in
let rec exp (E_aux (e,ann) as ea) =
match e with
| E_block es ->
@@ -1029,9 +1043,7 @@ let stop_at_false_assertions e =
let e2,stop = exp e2 in
E_aux (E_let (LB_aux (LB_val (p,e1),lbann),e2),ann), stop
end
- | E_assert (E_aux (E_constraint (NC_aux (NC_false,_)),_),_) ->
- ea, Some (typ_of_annot ann)
- | E_assert (E_aux (E_lit (L_aux (L_false,_)),_),_) ->
+ | E_assert (e1,_) when exp_false e1 ->
ea, Some (typ_of_annot ann)
| _ -> ea, None
in fst (exp e)
diff --git a/src/state.ml b/src/state.ml
index 67eda5b8..5873c472 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -238,7 +238,7 @@ let register_refs_lem prefix_recordtype mwords registers =
separate hardline setters ^^ hardline ^^
string " Nothing" ^^ hardline ^^ hardline ^^
string "let register_accessors = (get_regval, set_regval)" ^^ hardline ^^ hardline ^^
- string "let liftS = liftState register_accessors" ^^ hardline
+ string "let liftS s = liftState register_accessors s" ^^ hardline
in
separate hardline [generic_convs; refs; getters_setters]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 13:46:37 +0000