summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile2
-rw-r--r--src/ast_util.ml15
-rw-r--r--src/ast_util.mli1
-rw-r--r--src/gen_lib/sail_operators.lem18
-rw-r--r--src/gen_lib/sail_operators_mwords.lem14
-rw-r--r--src/gen_lib/state.lem41
-rw-r--r--src/initial_check.ml13
-rw-r--r--src/initial_check.mli2
-rw-r--r--src/pretty_print_common.ml2
-rw-r--r--src/pretty_print_lem.ml88
-rw-r--r--src/pretty_print_lem_ast.ml1
-rw-r--r--src/process_file.ml41
-rw-r--r--src/process_file.mli3
-rw-r--r--src/rewriter.ml54
-rw-r--r--src/sail.ml13
-rw-r--r--src/util.ml9
-rw-r--r--src/util.mli5
17 files changed, 209 insertions, 113 deletions
diff --git a/src/Makefile b/src/Makefile
index 4147b10c..6cfcf874 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -173,7 +173,7 @@ _build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native
_build/cheri_embed_types_sequential.lem: $(CHERI_SAILS) ./sail.native
mkdir -p _build
cd _build ;\
- ../sail.native -lem_lib "Mips_extras_embed" -lem -o cheri $(CHERI_SAILS)
+ ../sail.native -lem_lib "Mips_extras_embed" -lem -lem_sequential -lem_mwords -o cheri $(CHERI_SAILS)
_build/Cheri_embed_sequential.thy: _build/cheri_embed_types_sequential.lem
cd _build ;\
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 5740a3c7..aef1a05d 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -392,6 +392,11 @@ and string_of_n_constraint = function
| NC_aux (NC_true, _) -> "true"
| NC_aux (NC_false, _) -> "false"
+let string_of_annot = function
+ | Some (_, typ, eff) ->
+ "Some (_, " ^ string_of_typ typ ^ ", " ^ string_of_effect eff ^ ")"
+ | None -> "None"
+
let string_of_quant_item_aux = function
| QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid
| QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> string_of_kind k ^ " " ^ string_of_kid kid
@@ -629,13 +634,17 @@ let rec is_vector_typ = function
let typ_app_args_of = function
| Typ_aux (Typ_app (Id_aux (Id c,_), targs), l) ->
(c, List.map (fun (Typ_arg_aux (a,_)) -> a) targs, l)
- | Typ_aux (_, l) -> raise (Reporting_basic.err_typ l "typ_app_args_of called on non-app type")
+ | Typ_aux (_, l) as typ ->
+ raise (Reporting_basic.err_typ l
+ ("typ_app_args_of called on non-app type " ^ string_of_typ typ))
let rec vector_typ_args_of typ = match typ_app_args_of typ with
| ("vector", [Typ_arg_nexp start; Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], _) ->
- (start, len, ord, etyp)
+ (simplify_nexp start, simplify_nexp len, ord, etyp)
| ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp
- | (_, _, l) -> raise (Reporting_basic.err_typ l "vector_typ_args_of called on non-vector type")
+ | (_, _, l) ->
+ raise (Reporting_basic.err_typ l
+ ("vector_typ_args_of called on non-vector type " ^ string_of_typ typ))
let is_order_inc = function
| Ord_aux (Ord_inc, _) -> true
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 6a150872..e6823ee9 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -146,6 +146,7 @@ val string_of_order : order -> string
val string_of_nexp : nexp -> string
val string_of_typ : typ -> string
val string_of_typ_arg : typ_arg -> string
+val string_of_annot : ('a * typ * effect) option -> string
val string_of_n_constraint : n_constraint -> string
val string_of_quant_item : quant_item -> string
val string_of_typquant : typquant -> string
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index fbe096c9..a760fb42 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -205,6 +205,7 @@ let modulo (l,r) = hardware_mod l r
let quot = hardware_quot
let power (l,r) = integerPow l r
+let add_int = add
let sub_int = sub
let mult_int = mult
@@ -452,6 +453,9 @@ let rec repeat xs n =
let duplicate (bit, length) =
Vector (repeat [bit] length) (length - 1) false
+let replicate_bits (v, count) =
+ Vector (repeat (get_elems v) count) ((length v * count) - 1) false
+
let compare_op op (l,r) = (op l r)
let lt = compare_op (<)
@@ -531,3 +535,17 @@ let make_bitvector_undef length =
let mask' (start, n, Vector bits _ dir) =
let current_size = List.length bits in
Vector (drop (current_size - (natFromInteger n)) bits) start dir
+
+
+(* Register operations *)
+
+let update_reg_range i j reg_val new_val = update reg_val i j new_val
+let update_reg_bit i reg_val bit = update_pos reg_val i bit
+let update_reg_field_range regfield i j reg_val new_val =
+ let current_field_value = regfield.get_field reg_val in
+ let new_field_value = update current_field_value i j new_val in
+ regfield.set_field reg_val new_field_value
+let write_reg_field_bit regfield i reg_val bit =
+ let current_field_value = regfield.get_field reg_val in
+ let new_field_value = update_pos current_field_value i bit in
+ regfield.set_field reg_val new_field_value
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 9bc81b3e..44ae9d7c 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -245,6 +245,7 @@ let modulo (l,r) = hardware_mod l r
let quot = hardware_quot
let power (l,r) = integerPow l r
+let add_int = add
let sub_int = sub
let mult_int = mult
@@ -574,3 +575,16 @@ let make_bitvector_undef length =
(* TODO *)
val mask : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
let mask (start, _, Bitvector w _ dir) = (Bitvector (zeroExtend w) start dir)
+
+(* Register operations *)
+
+let update_reg_range i j reg_val new_val = bvupdate reg_val i j new_val
+let update_reg_bit i reg_val bit = bvupdate_pos reg_val i bit
+let update_reg_field_range regfield i j reg_val new_val =
+ let current_field_value = regfield.get_field reg_val in
+ let new_field_value = bvupdate current_field_value i j new_val in
+ regfield.set_field reg_val new_field_value
+let write_reg_field_bit regfield i reg_val bit =
+ let current_field_value = regfield.get_field reg_val in
+ let new_field_value = bvupdate_pos current_field_value i bit in
+ regfield.set_field reg_val new_field_value
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index d5866cde..914955e0 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,7 +1,6 @@
open import Pervasives_extra
open import Sail_impl_base
open import Sail_values
-open import Sail_operators_mwords
(* 'a is result type *)
@@ -51,7 +50,7 @@ let inline (>>) m n = m >>= fun _ -> n
val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a
let exit _ s = [(Right (), s)]
-val early_return : forall 'regs 'r. 'r -> MR 'regs unit 'r
+val early_return : forall 'regs 'a 'r. 'r -> MR 'regs 'a 'r
let early_return r s = [(Right (Just r), s)]
val catch_early_return : forall 'regs 'a. MR 'regs 'a 'a -> M 'regs 'a
@@ -76,12 +75,11 @@ let set_reg state reg v =
<| state with regstate = reg.write_to state.regstate v |>
-val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M 'regs (bitvector 'b)
+val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> integer -> integer -> M 'regs (vector bitU)
let read_mem dir read_kind addr sz state =
- let addr = unsigned addr in
let addrs = range addr (addr+sz-1) in
let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
- let value = vec_to_bvec (Sail_values.internal_mem_value dir memory_value) in
+ let value = Sail_values.internal_mem_value dir memory_value in
let is_exclusive = match read_kind with
| Sail_impl_base.Read_plain -> false
| Sail_impl_base.Read_reserve -> true
@@ -98,9 +96,9 @@ let read_mem dir read_kind addr sz state =
(* caps are aligned at 32 bytes *)
let cap_alignment = (32 : integer)
-val read_tag : forall 'regs 'a. bool -> read_kind -> bitvector 'a -> M 'regs bitU
+val read_tag : forall 'regs 'a. bool -> read_kind -> integer -> M 'regs bitU
let read_tag dir read_kind addr state =
- let addr = (unsigned addr) / cap_alignment in
+ let addr = addr / cap_alignment in
let tag = match (Map.lookup addr state.tagstate) with
| Just t -> t
| Nothing -> B0
@@ -125,18 +123,17 @@ let excl_result () state =
(Left true, <| state with last_exclusive_operation_was_load = false |>) in
(Left false, state) :: if state.last_exclusive_operation_was_load then [success] else []
-val write_mem_ea : forall 'regs 'a. write_kind -> bitvector 'a -> integer -> M 'regs unit
+val write_mem_ea : forall 'regs 'a. write_kind -> integer -> integer -> M 'regs unit
let write_mem_ea write_kind addr sz state =
- let addr = unsigned addr in
[(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)]
-val write_mem_val : forall 'regs 'b. bitvector 'b -> M 'regs bool
+val write_mem_val : forall 'regs 'b. vector bitU -> M 'regs bool
let write_mem_val v state =
let (write_kind,addr,sz) = match state.write_ea with
| Nothing -> failwith "write ea has not been announced yet"
| Just write_ea -> write_ea end in
let addrs = range addr (addr+sz-1) in
- let v = external_mem_value (bvec_to_vec v) in
+ let v = external_mem_value v in
let addresses_with_value = List.zip addrs v in
let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
state.memstate addresses_with_value in
@@ -178,28 +175,6 @@ let update_reg reg f v state =
let current_value = get_reg state reg in
let new_value = f current_value v in
[(Left (), set_reg state reg new_value)]
-let write_reg_range reg i j v state =
- let current_value = get_reg state reg in
- let new_value = bvupdate current_value i j v in
- [(Left (), set_reg state reg new_value)]
-let write_reg_bit reg i bit state =
- let current_value = get_reg state reg in
- let new_value = bvupdate_pos current_value i bit in
- [(Left (), set_reg state reg new_value)]
-let write_reg_field reg regfield =
- update_reg reg regfield.set_field
-let write_reg_field_range reg regfield i j =
- let upd regval v =
- let current_field_value = regfield.get_field regval in
- let new_field_value = bvupdate current_field_value i j v in
- regfield.set_field regval new_field_value in
- update_reg reg upd
-let write_reg_field_bit reg regfield i =
- let upd regval v =
- let current_field_value = regfield.get_field regval in
- let new_field_value = bvupdate_pos current_field_value i v in
- regfield.set_field regval new_field_value in
- update_reg reg upd
val barrier : forall 'regs. barrier_kind -> M 'regs unit
diff --git a/src/initial_check.ml b/src/initial_check.ml
index e9695dd4..4c0a0db4 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -44,6 +44,8 @@ open Ast
open Util
open Ast_util
+let opt_undefined_gen = ref false
+
module Envmap = Finite_map.Fmap_map(String)
module Nameset' = Set.Make(String)
module Nameset = struct
@@ -1116,6 +1118,11 @@ let generate_initialize_registers vs_ids (Defs defs) =
let process_ast order defs =
let (ast, _, _) = to_ast Nameset.empty initial_kind_env order defs in
- let vs_ids = val_spec_ids ast in
- let ast = generate_undefineds vs_ids ast in
- generate_initialize_registers vs_ids ast
+ if not !opt_undefined_gen
+ then ast
+ else
+ begin
+ let vs_ids = val_spec_ids ast in
+ let ast = generate_undefineds vs_ids ast in
+ generate_initialize_registers vs_ids ast
+ end
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 86b5ca3b..feb9cb83 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -43,6 +43,8 @@
open Ast
open Ast_util
+val opt_undefined_gen : bool ref
+
val process_ast : order -> Parse_ast.defs -> unit defs
val val_spec_ids : 'a defs -> IdSet.t
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 70f5b749..02cc3574 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -212,7 +212,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with
| Nexp_var v -> doc_var v
| Nexp_id i -> braces (doc_id i)
- | Nexp_constant i -> doc_int i
+ | Nexp_constant i -> if i < 0 then parens(doc_int i) else doc_int i
| Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _->
group (parens (nexp ne))
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 3d4f3083..5e0d39a0 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -58,7 +58,11 @@ let langlebar = string "<|"
let ranglebar = string "|>"
let anglebars = enclose langlebar ranglebar
-let fix_id name = match name with
+let is_number_char c =
+ c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' ||
+ c = '6' || c = '7' || c = '8' || c = '9'
+
+let fix_id remove_tick name = match name with
| "assert"
| "lsl"
| "lsr"
@@ -76,22 +80,17 @@ let fix_id name = match name with
| "EQ"
| "integer"
-> name ^ "'"
- | _ -> name
-
-let is_number char =
- char = '0' || char = '1' || char = '2' || char = '3' || char = '4' || char = '5' ||
- char = '6' || char = '7' || char = '8' || char = '9'
+ | _ ->
+ if name.[0] = '\'' then
+ let var = String.sub name 1 (String.length name - 1) in
+ if remove_tick then var else (var ^ "'")
+ else if is_number_char(name.[0]) then
+ ("v" ^ name ^ "'")
+ else name
let doc_id_lem (Id_aux(i,_)) =
match i with
- | Id i ->
- (* this not the right place to do this, just a workaround *)
- if i.[0] = '\'' then
- string ((String.sub i 1 (String.length i - 1)) ^ "'")
- else if is_number(i.[0]) then
- string ("v" ^ i ^ "'")
- else
- string (fix_id i)
+ | Id i -> string (fix_id false i)
| DeIid x ->
(* add an extra space through empty to avoid a closing-comment
* token in case of x ending with star. *)
@@ -102,7 +101,7 @@ let doc_id_lem_type (Id_aux(i,_)) =
| Id("int") -> string "ii"
| Id("nat") -> string "ii"
| Id("option") -> string "maybe"
- | Id i -> string (fix_id i)
+ | Id i -> string (fix_id false i)
| DeIid x ->
(* add an extra space through empty to avoid a closing-comment
* token in case of x ending with star. *)
@@ -115,12 +114,14 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
| Id("nat") -> string "integer"
| Id("Some") -> string "Just"
| Id("None") -> string "Nothing"
- | Id i -> string (fix_id (String.capitalize i))
+ | Id i -> string (fix_id false (String.capitalize i))
| DeIid x ->
(* add an extra space through empty to avoid a closing-comment
* token in case of x ending with star. *)
separate space [colon; string (String.capitalize x); empty]
+let doc_var_lem kid = string (fix_id true (string_of_kid kid))
+
let effectful_set =
List.exists
(fun (BE_aux (eff,_)) ->
@@ -230,6 +231,7 @@ let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with
| Typ_wild -> true
| Typ_id _ -> false
| Typ_var _ -> true
+ | Typ_exist _ -> true
| Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2
| Typ_tup ts -> List.exists contains_t_pp_var ts
| Typ_app (c,targs) ->
@@ -321,6 +323,7 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) =
begin match id with
| Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
| _ -> doc_id_lem id end
+ | P_var kid -> doc_var_lem kid
| P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id])
| P_typ(typ,p) ->
let doc_p = doc_pat_lem sequential mwords true p in
@@ -391,15 +394,16 @@ let doc_exp_lem, doc_let_lem =
underscore ^^
doc_id_lem id in
liftR ((prefix 2 1)
- (string "write_reg_field_range")
+ (string "update_reg")
(align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space^^
- field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
+ parens (string "update_reg_field_range" ^/^ field_ref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
| _ ->
liftR ((prefix 2 1)
- (string "write_reg_range")
- (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)))
+ (string "update_reg")
+ (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+ parens (string "update_reg_range" ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
)
- | LEXP_vector (le,e2) when is_bit_typ t ->
+ | LEXP_vector (le,e2) ->
(match le with
| LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
if is_bit_typ (typ_of_annot fannot) then
@@ -410,12 +414,14 @@ let doc_exp_lem, doc_let_lem =
underscore ^^
doc_id_lem id in
liftR ((prefix 2 1)
- (string "write_reg_field_bit")
- (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e)))
+ (string "update_reg")
+ (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 "write_reg_bit")
- (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e))
+ (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)
@@ -425,9 +431,11 @@ let doc_exp_lem, doc_let_lem =
let field_ref =
doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
underscore ^^
- doc_id_lem id in
+ doc_id_lem id ^^
+ dot ^^
+ string "set_field" in
liftR ((prefix 2 1)
- (string "write_reg_field")
+ (string "update_reg")
(doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
field_ref ^/^ expY e))
(* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
@@ -692,7 +700,7 @@ let doc_exp_lem, doc_let_lem =
let recordtyp = match annot with
| Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
tid
- | _ -> raise (report l "cannot get record type") in
+ | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
let epp = anglebars (space ^^ (align (separate_map
(semi_sp ^^ break 1)
(doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
@@ -702,7 +710,7 @@ let doc_exp_lem, doc_let_lem =
let recordtyp = match eannot with
| Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
tid
- | _ -> raise (report l "cannot get record type") in
+ | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))
| E_vector exps ->
let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
@@ -801,21 +809,26 @@ let doc_exp_lem, doc_let_lem =
if aexp_needed then parens (align bepp) else bepp
| E_vector_update(v,e1,e2) ->
let t = typ_of full_exp in
+ let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+ let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
let call =
if is_bitvector_typ t (*&& mwords*)
- then "bitvector_update_pos"
- else "update_pos" in
- let epp = separate space [string call;expY v;expY e1;expY e2] in
+ then "bitvector_update_pos" ^ ord_suffix
+ else "update_pos" ^ ord_suffix in
+ let epp = string call ^^ space ^^ parens (separate comma_sp [expY v;expY e1;expY e2]) in
if aexp_needed then parens (align epp) else epp
| E_vector_update_subrange(v,e1,e2,e3) ->
let t = typ_of full_exp in
+ let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+ let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
let call =
if is_bitvector_typ t (*&& mwords*)
- then "bitvector_update"
- else "update" in
- let epp = align (string call ^//^
- group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^
- group (expY e3)) in
+ then "bitvector_update" ^ ord_suffix
+ else "update" ^ ord_suffix in
+ let epp =
+ align (string call ^//^
+ parens (separate comma_sp
+ [group (expY v); group (expY e1); group (expY e2); group (expY e3)])) in
if aexp_needed then parens (align epp) else epp
| E_list exps ->
brackets (separate_map semi (expN) exps)
@@ -1001,6 +1014,7 @@ let doc_exp_lem, doc_let_lem =
top_exp sequential mwords early_ret true e])
| LEXP_id id -> doc_id_lem id
| LEXP_cast (typ,id) -> doc_id_lem id
+ | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem sequential mwords early_ret) lexps)
| _ ->
raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Shouldn't happen"))
(* expose doc_exp_lem and doc_let *)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index c75c102f..5edf9d12 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -328,6 +328,7 @@ let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
| P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")"
| P_wild -> "P_wild"
| P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")"
+ | P_var(kid) -> "(P_var " ^ pp_format_var_lem kid ^ ")"
| P_as(pat,id) -> "(P_as " ^ pp_format_pat_lem pat ^ " " ^ pp_format_id_lem id ^ ")"
| P_typ(typ,pat) -> "(P_typ " ^ pp_format_typ_lem typ ^ " " ^ pp_format_pat_lem pat ^ ")"
| P_app(id,pats) -> "(P_app " ^ pp_format_id_lem id ^ " [" ^
diff --git a/src/process_file.ml b/src/process_file.ml
index 46b6538e..0f789c9d 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -41,6 +41,8 @@
(**************************************************************************)
let opt_new_parser = ref false
+let opt_lem_sequential = ref false
+let opt_lem_mwords = ref false
type out_type =
| Lem_ast_out
@@ -136,31 +138,28 @@ let generated_line f =
let output_lem filename libs defs =
let generated_line = generated_line filename in
- let types_module = (filename ^ "_embed_types") in
- let types_module_seq = (filename ^ "_embed_types_sequential") in
- let libs_seq = List.map (fun lib -> lib ^ "_sequential") libs in
+ let seq_suffix = if !opt_lem_sequential then "_sequential" else "" in
+ let types_module = (filename ^ "_embed_types" ^ seq_suffix) in
+ let monad_module = if !opt_lem_sequential then "State" else "Prompt" in
+ let operators_module = if !opt_lem_mwords then "Sail_operators_mwords" else "Sail_operators" in
+ let libs = List.map (fun lib -> lib ^ seq_suffix) libs in
+ let base_imports = [
+ "Pervasives_extra";
+ "Sail_impl_base";
+ "Sail_values";
+ operators_module;
+ monad_module
+ ] in
let ((ot,_, _) as ext_ot) =
- open_output_with_check_unformatted (filename ^ "_embed_types.lem") in
- let ((ots,_, _) as ext_ots) =
- open_output_with_check_unformatted (filename ^ "_embed_types_sequential.lem") in
+ open_output_with_check_unformatted (filename ^ "_embed_types" ^ seq_suffix ^ ".lem") in
let ((o,_, _) as ext_o) =
- open_output_with_check_unformatted (filename ^ "_embed.lem") in
- let ((os,_, _) as ext_os) =
- open_output_with_check_unformatted (filename ^ "_embed_sequential.lem") in
- (Pretty_print.pp_defs_lem false false
- (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt"])
- (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt";
- String.capitalize types_module] @ libs)
- defs generated_line);
- (Pretty_print.pp_defs_lem true true
- (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State"])
- (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State";
- String.capitalize types_module_seq] @ libs_seq)
+ open_output_with_check_unformatted (filename ^ "_embed" ^ seq_suffix ^ ".lem") in
+ (Pretty_print.pp_defs_lem !opt_lem_sequential !opt_lem_mwords
+ (ot, base_imports)
+ (o, base_imports @ (String.capitalize types_module :: libs))
defs generated_line);
close_output_with_check ext_ot;
- close_output_with_check ext_ots;
- close_output_with_check ext_o;
- close_output_with_check ext_os
+ close_output_with_check ext_o
let output1 libpath out_arg filename defs =
let f' = Filename.basename (Filename.chop_extension filename) in
diff --git a/src/process_file.mli b/src/process_file.mli
index cd867b0d..53a6f3f2 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -52,6 +52,8 @@ 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_new_parser : bool ref
+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
@@ -73,4 +75,3 @@ val output :
files existed before. If it is set to [false] and an output file already exists,
the output file is only updated, if its content really changes. *)
val always_replace_files : bool ref
-
diff --git a/src/rewriter.ml b/src/rewriter.ml
index b180b0a1..78b29200 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2183,6 +2183,15 @@ let id_is_local_var id env = match Env.lookup_id id env with
| Local _ -> true
| _ -> false
+let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
+ | LEXP_memory _ -> false
+ | LEXP_id id
+ | LEXP_cast (_, id) -> id_is_local_var id env
+ | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps
+ | LEXP_vector (lexp,_)
+ | LEXP_vector_range (lexp,_,_)
+ | LEXP_field (lexp,_) -> lexp_is_local lexp env
+
let id_is_unbound id env = match Env.lookup_id id env with
| Unbound -> true
| _ -> false
@@ -2203,6 +2212,13 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
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))
| LEXP_vector (lexp, e) ->
let (lexp, access, rexp) = rewrite_local_lexp lexp in
(lexp, E_aux (E_vector_access (access, e), annot),
@@ -2233,7 +2249,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
let rec walker exps = match exps with
| [] -> []
| (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)->
+ when lexp_is_local_intro le env && not (lexp_is_effectful le) ->
let (le', _, re') = rewrite_local_lexp le in
let e' = re' (rewrite_base e) in
let exps' = walker exps in
@@ -2371,12 +2387,11 @@ let rewrite_defs_early_return =
| _ -> exp in
let e_block es =
- (* let rec walker = function
- | e :: es -> if is_return e then [e] else e :: walker es
- | [] -> [] in
- let es = walker es in *)
match es with
| [E_aux (e, _)] -> e
+ | _ :: _ when is_return (Util.last es) ->
+ let (E_aux (_, annot) as e) = Util.last es in
+ E_return (E_aux (E_block (Util.butlast es @ [get_return e]), annot))
| _ -> E_block es in
let e_if (e1, e2, e3) =
@@ -2404,14 +2419,19 @@ let rewrite_defs_early_return =
| _ -> full_exp in
let rewrite_funcl_early_return _ (FCL_aux (FCL_Funcl (id, pat, exp), a)) =
- let exp = fold_exp
- { id_exp_alg with e_block = e_block; e_if = e_if; e_case = e_case;
- e_aux = e_aux } exp in
+ let exp =
+ exp
+ (* Pull early returns out as far as possible *)
+ |> fold_exp { id_exp_alg with e_block = e_block; e_if = e_if; e_case = e_case }
+ (* Remove singleton E_return *)
+ |> get_return
+ (* Fix effect annotations *)
+ |> fold_exp { id_exp_alg with e_aux = e_aux } in
let a = match a with
| (l, Some (env, typ, eff)) ->
(l, Some (env, typ, union_effects eff (effect_of exp)))
| _ -> a in
- FCL_aux (FCL_Funcl (id, pat, get_return exp), a) in
+ FCL_aux (FCL_Funcl (id, pat, exp), a) in
let rewrite_fun_early_return rewriters
(FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), a)) =
@@ -2948,8 +2968,19 @@ let rewrite_defs_letbind_effects =
let rewrite_defs_effectful_let_expressions =
+ let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with
+ | LEXP_id id -> P_aux (P_id id, annot)
+ | LEXP_cast (typ, id) -> P_aux (P_typ (typ, P_aux (P_id id, annot)), annot)
+ | LEXP_tup lexps -> P_aux (P_tup (List.map pat_of_local_lexp lexps), annot)
+ | _ -> raise (Reporting_basic.err_unreachable l "unexpected local lexp") in
+
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) ->
+ (* Rewrite assignments to local variables into let bindings *)
+ 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') ->
if effectful exp'
@@ -3261,7 +3292,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
"tail-position": check the definition nexp_term and where it is used. *)
| _ -> exp
-let replace_memwrite_e_assign exp =
+let replace_memwrite_e_assign exp =
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)
@@ -3395,7 +3426,8 @@ let rewrite_defs_remove_e_assign =
let recheck_defs defs = fst (check initial_env defs)
let rewrite_defs_lem =[
- top_sort_defs;
+ (* top_sort_defs; *)
+ rewrite_trivial_sizeof;
rewrite_sizeof;
rewrite_defs_remove_vector_concat;
rewrite_defs_remove_bitvector_pats;
diff --git a/src/sail.ml b/src/sail.ml
index 5e979738..b63f807c 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -65,7 +65,7 @@ let options = Arg.align ([
Arg.Set opt_print_lem,
" output a Lem translated version of the input");
( "-ocaml",
- Arg.Set opt_print_ocaml,
+ Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen],
" output an OCaml translated version of the input");
( "-lem_lib",
Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem),
@@ -73,6 +73,12 @@ let options = Arg.align ([
( "-ocaml_lib",
Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml),
"<filename> provide additional library to open in OCaml output");
+ ( "-lem_sequential",
+ Arg.Set Process_file.opt_lem_sequential,
+ " use sequential state monad for Lem output");
+ ( "-lem_mwords",
+ Arg.Set Process_file.opt_lem_mwords,
+ " use native machine word library for Lem output");
(*
( "-i",
Arg.String (fun l -> lib := l::!lib),
@@ -93,7 +99,7 @@ let options = Arg.align ([
" (experimental) use new parser");
( "-just_check",
Arg.Set opt_just_check,
- " (experimental) terminate immediately after typechecking, implies -new_typecheck");
+ " (experimental) terminate immediately after typechecking");
( "-ddump_tc_ast",
Arg.Set opt_ddump_tc_ast,
" (debug) dump the typechecked ast to stdout");
@@ -109,6 +115,9 @@ let options = Arg.align ([
( "-no_effects",
Arg.Set Type_check.opt_no_effects,
" turn off effect checking");
+ ( "-undefined-gen",
+ Arg.Set Initial_check.opt_undefined_gen,
+ " generate undefined_type functions for types in the specification");
( "-v",
Arg.Set opt_print_version,
" print version");
diff --git a/src/util.ml b/src/util.ml
index c89cc1ef..335fd36f 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -86,6 +86,15 @@
(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)
(**************************************************************************)
+let rec last = function
+ | [x] -> x
+ | _ :: xs -> last xs
+ | [] -> raise (Failure "last")
+
+let rec butlast = function
+ | [x] -> []
+ | x :: xs -> x :: butlast xs
+ | [] -> []
module Duplicate(S : Set.S) = struct
diff --git a/src/util.mli b/src/util.mli
index f1182c61..11588de2 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -40,6 +40,11 @@
(* SUCH DAMAGE. *)
(**************************************************************************)
+(* Last element of a list *)
+val last : 'a list -> 'a
+
+val butlast : 'a list -> 'a list
+
(** Mixed useful things *)
module Duplicate(S : Set.S) : sig
type dups =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 06:58:42 +0000