summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml7
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/c_backend.ml9
-rw-r--r--src/constraint.ml19
-rw-r--r--src/latex.ml77
-rw-r--r--src/monomorphise.ml9
-rw-r--r--src/optimize.ml100
-rw-r--r--src/pretty_print_lem.ml16
-rw-r--r--src/process_file.ml45
-rw-r--r--src/process_file.mli4
-rw-r--r--src/rewrites.ml2
-rw-r--r--src/sail.ml12
-rw-r--r--src/sail_lib.ml7
-rw-r--r--src/state.ml25
-rw-r--r--src/type_check.ml16
-rw-r--r--src/type_check.mli4
16 files changed, 277 insertions, 77 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index c0e9fe02..26c6b9df 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -165,7 +165,7 @@ module Kind = struct
| K_type, _ -> 1 | _, K_type -> -1
| K_order, _ -> 1 | _, K_order -> -1
end
-
+
module KOpt = struct
type t = kinded_id
let compare kopt1 kopt2 =
@@ -1362,6 +1362,9 @@ let is_fundef id = function
| DEF_fundef (FD_aux (FD_function (_, _, _, FCL_aux (FCL_Funcl (id', _), _) :: _), _)) when Id.compare id' id = 0 -> true
| _ -> false
+let rename_valspec id (VS_aux (VS_val_spec (typschm, _, externs, is_cast), annot)) =
+ VS_aux (VS_val_spec (typschm, id, externs, is_cast), annot)
+
let rename_funcl id (FCL_aux (FCL_Funcl (_, pexp), annot)) = FCL_aux (FCL_Funcl (id, pexp), annot)
let rename_fundef id (FD_aux (FD_function (ropt, topt, eopt, funcls), annot)) =
@@ -1498,7 +1501,7 @@ let locate_id f (Id_aux (name, l)) = Id_aux (name, f l)
let locate_kid f (Kid_aux (name, l)) = Kid_aux (name, f l)
let locate_kind f (K_aux (kind, l)) = K_aux (kind, f l)
-
+
let locate_kinded_id f (KOpt_aux (KOpt_kind (k, kid), l)) =
KOpt_aux (KOpt_kind (locate_kind f k, locate_kid f kid), f l)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 8787dbff..d9b0110a 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -385,6 +385,8 @@ val is_valspec : id -> 'a def -> bool
val is_fundef : id -> 'a def -> bool
+val rename_valspec : id -> 'a val_spec -> 'a val_spec
+
val rename_fundef : id -> 'a fundef -> 'a fundef
val split_defs : ('a def -> bool) -> 'a defs -> ('a defs * 'a def * 'a defs) option
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 6e21dab6..5e600918 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1399,9 +1399,11 @@ let compile_type_def ctx (TD_aux (type_def, _)) =
CTD_struct (id, Bindings.bindings ctors),
{ ctx with records = Bindings.add id ctors ctx.records }
- | TD_variant (id, _, tus, _) ->
+ | TD_variant (id, typq, tus, _) ->
let compile_tu = function
- | Tu_aux (Tu_ty_id (typ, id), _) -> ctyp_of_typ ctx typ, id
+ | Tu_aux (Tu_ty_id (typ, id), _) ->
+ let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in
+ ctyp_of_typ ctx typ, id
in
let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in
CTD_variant (id, Bindings.bindings ctus),
@@ -1763,6 +1765,9 @@ let rec compile_def n total ctx = function
(* Only the parser and sail pretty printer care about this. *)
| DEF_fixity _ -> [], ctx
+ (* We just ignore any pragmas we don't want to deal with. *)
+ | DEF_pragma _ -> [], ctx
+
| DEF_internal_mutrec fundefs ->
let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in
List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def n total ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs
diff --git a/src/constraint.ml b/src/constraint.ml
index af024ce3..b7fa50c3 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -133,16 +133,17 @@ let to_smt l vars constr =
| _ ->
raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function")
in
- var_decs l vars, smt_constraint constr
+ var_decs l vars, smt_constraint constr, smt_var
-let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string =
- let variables, problem = to_smt l vars constr in
+let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string * (kid -> sexpr) =
+ let variables, problem, var_map = to_smt l vars constr in
"(push)\n"
^ variables ^ "\n"
^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; problem])
^ "\n(assert constraint)\n(check-sat)"
^ (if get_model then "\n(get-model)" else "")
- ^ "\n(pop)"
+ ^ "\n(pop)",
+ var_map
type smt_result = Unknown | Sat | Unsat
@@ -185,7 +186,7 @@ let save_digests () =
let call_z3' l vars constraints : smt_result =
let problems = [constraints] in
- let z3_file = smtlib_of_constraints l vars constraints in
+ let z3_file, _ = smtlib_of_constraints l vars constraints in
if !opt_smt_verbose then
prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file)
@@ -243,9 +244,11 @@ let call_z3 l vars constraints =
result
let rec solve_z3 l vars constraints var =
- let z3_file = smtlib_of_constraints ~get_model:true l vars constraints in
+ let z3_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in
+ let z3_var = pp_sexpr (smt_var var) in
- (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *)
+ (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file);
+ prerr_endline ("Solving for " ^ z3_var); *)
let rec input_all chan =
try
@@ -270,7 +273,7 @@ let rec solve_z3 l vars constraints var =
raise (Reporting.err_general l ("Got error when calling z3: " ^ Printexc.to_string exn))
in
Sys.remove input_file;
- let regexp = {|(define-fun v|} ^ Util.zencode_string (string_of_kid var) ^ {| () Int[ ]+\([0-9]+\))|} in
+ let regexp = {|(define-fun |} ^ z3_var ^ {| () Int[ ]+\([0-9]+\))|} in
try
let _ = Str.search_forward (Str.regexp regexp) z3_output 0 in
let result = Big_int.of_string (Str.matched_group 1 z3_output) in
diff --git a/src/latex.ml b/src/latex.ml
index 2f578f2c..a0660daa 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -57,6 +57,7 @@ module StringSet = Set.Make(String);;
let opt_prefix = ref "sail"
let opt_directory = ref "sail_latex"
+let opt_simple_val = ref true
let rec unique_postfix n =
if n < 0 then
@@ -97,13 +98,13 @@ let rec unique_postfix n =
type id_category =
| Function
| Val
- | Overload
+ | Overload of int
| FunclCtor of id * int
| FunclNum of int
| FunclApp of string
+ | Type
-let replace_numbers str =
- let replacements =
+let number_replacements =
[ ("0", "Zero");
("1", "One");
("2", "Two");
@@ -114,16 +115,28 @@ let replace_numbers str =
("7", "Seven");
("8", "Eight");
("9", "Nine") ]
- in
+
+(* add to this as needed *)
+let other_replacements =
+ [ ("_", "Underscore") ]
+
+let char_replace str replacements =
List.fold_left (fun str (from, into) -> Str.global_replace (Str.regexp_string from) into str) str replacements
+let replace_numbers str =
+ char_replace str number_replacements
+
+let replace_others str =
+ char_replace str other_replacements
+
let category_name = function
| Function -> "fn"
| Val -> "val"
- | Overload -> "overload"
+ | Type -> "type"
+ | Overload n -> "overload" ^ unique_postfix n
| FunclNum n -> "fcl" ^ unique_postfix n
| FunclCtor (id, n) ->
- let str = replace_numbers (Util.zencode_string (string_of_id id)) in
+ let str = replace_others (replace_numbers (Util.zencode_string (string_of_id id))) in
"fcl" ^ String.sub str 1 (String.length str - 1) ^ unique_postfix n
| FunclApp str -> "fcl" ^ str
@@ -134,7 +147,8 @@ let category_name_val = function
let category_name_simple = function
| Function -> "fn"
| Val -> "val"
- | Overload -> "overload"
+ | Type -> "type"
+ | Overload n -> "overload"
| FunclNum _ -> "fcl"
| FunclCtor (_, _) -> "fcl"
| FunclApp _ -> "fcl"
@@ -162,8 +176,8 @@ let latex_id id =
(* If we have any other weird symbols in the id, remove them using Util.zencode_string (removing the z prefix) *)
let str = Util.zencode_string str in
let str = String.sub str 1 (String.length str - 1) in
- (* Latex only allows letters in identifiers, so replace all numbers *)
- let str = replace_numbers str in
+ (* Latex only allows letters in identifiers, so replace all numbers and other characters *)
+ let str = replace_others (replace_numbers str) in
let generated = state.generated_names |> Bindings.bindings |> List.map snd |> StringSet.of_list in
@@ -290,10 +304,10 @@ let latex_loc no_loc l =
let commands = ref StringSet.empty
-let doc_spec_simple (VS_val_spec(ts,id,ext,is_cast)) =
- Pretty_print_sail.doc_id id ^^ space
- ^^ colon ^^ space
- ^^ Pretty_print_sail.doc_typschm ~simple:true ts
+let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext, is_cast), _)) =
+ Pretty_print_sail.doc_id id ^^ space
+ ^^ colon ^^ space
+ ^^ Pretty_print_sail.doc_typschm ~simple:true ts
let rec latex_command cat id no_loc ((l, _) as annot) =
state.this <- Some id;
@@ -309,7 +323,7 @@ let rec latex_command cat id no_loc ((l, _) as annot) =
output_string chan (Pretty_print_sail.to_string doc);
close_out chan;
- ksprintf string "\\newcommand{\\sail%s%s}{\\phantomsection%s\\saildoc%s{" (category_name cat) (latex_id id) labelling (category_name_simple cat)
+ ksprintf string "\\newcommand{\\%s%s%s}{\\phantomsection%s\\saildoc%s{" !opt_prefix (category_name cat) (latex_id id) labelling (category_name_simple cat)
^^ docstring l ^^ string "}{"
^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}" (Filename.concat !opt_directory code_file)
@@ -381,30 +395,47 @@ let process_pragma l command =
Util.warn (Printf.sprintf "Bad latex pragma %s" (Reporting.loc_to_string l));
None
+let tdef_id = function
+ | TD_abbrev (id, _, _) -> id
+ | TD_record (id, _, _, _) -> id
+ | TD_variant (id, _, _, _) -> id
+ | TD_enum (id, _, _) -> id
+ | TD_bitfield (id, _, _) -> id
+
let defs (Defs defs) =
reset_state state;
+ let overload_counter = ref 0 in
+
let valspecs = ref IdSet.empty in
let fundefs = ref IdSet.empty in
+ let typedefs = ref IdSet.empty in
let latex_def def =
match def with
- | DEF_overload (id, ids) -> None
- (*
+ | DEF_overload (id, ids) ->
let doc =
string (Printf.sprintf "overload %s = {%s}" (string_of_id id) (Util.string_of_list ", " string_of_id ids))
in
- Some (latex_command Overload id doc (id_loc id, None))
- *)
+ incr overload_counter;
+ Some (latex_command (Overload !overload_counter) id doc (id_loc id, None))
- | DEF_spec (VS_aux (VS_val_spec (_, id, _, _) as vs, annot)) as def ->
+ | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), annot) as vs) as def ->
valspecs := IdSet.add id !valspecs;
- Some (latex_command Val id (doc_spec_simple vs) annot)
+ if !opt_simple_val then
+ Some (latex_command Val id (doc_spec_simple vs) annot)
+ else
+ Some (latex_command Val id (Pretty_print_sail.doc_spec ~comment:false vs) annot)
| DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), annot)) as def ->
fundefs := IdSet.add id !fundefs;
Some (latex_command Function id (Pretty_print_sail.doc_def def) annot)
+ | DEF_type (TD_aux (tdef, annot)) as def ->
+ let id = tdef_id tdef in
+ typedefs := IdSet.add id !typedefs;
+ Some (latex_command Type id (Pretty_print_sail.doc_def def) annot)
+
| DEF_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) as def ->
Some (latex_funcls def funcls)
@@ -432,7 +463,7 @@ let defs (Defs defs) =
identifiers then outputs the correct mangled command. *)
let id_command cat ids =
sprintf "\\newcommand{\\%s%s}[1]{\n " !opt_prefix (category_name cat)
- ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\sail%s%s}{}" (string_of_id id) (category_name cat) (latex_id id))
+ ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s%s%s}{}" (string_of_id id) !opt_prefix (category_name cat) (latex_id id))
(IdSet.elements ids)
^ "}"
|> string
@@ -449,5 +480,7 @@ let defs (Defs defs) =
^^ separate (twice hardline) [id_command Val !valspecs;
ref_command Val !valspecs;
id_command Function !fundefs;
- ref_command Function !fundefs]
+ ref_command Function !fundefs;
+ id_command Type !typedefs;
+ ref_command Type !typedefs]
^^ hardline
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 1b7fb3b4..2124c11e 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3424,7 +3424,7 @@ let rec sets_from_assert e =
match e with
| E_app (Id_aux (Id "or_bool",_),[e1;e2]) ->
aux e1 @ aux e2
- | E_app (Id_aux (Id "eq_atom",_),
+ | E_app (Id_aux (Id "eq_int",_),
[E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_);
E_aux (E_lit (L_aux (L_num i,_)),_)]) ->
(check_kid kid; [i])
@@ -4040,7 +4040,7 @@ let rec extract_value_from_guard var (E_aux (e,_)) =
match e with
| E_app (op, ([E_aux (E_id var',_); E_aux (E_lit (L_aux (L_num i,_)),_)] |
[E_aux (E_lit (L_aux (L_num i,_)),_); E_aux (E_id var',_)]))
- when string_of_id op = "eq_atom" && Id.compare var var' == 0 ->
+ when string_of_id op = "eq_int" && Id.compare var var' == 0 ->
Some i
| E_app (op, [e1;e2]) when string_of_id op = "and_bool" ->
(match extract_value_from_guard var e1 with
@@ -4053,7 +4053,8 @@ let fill_in_type env typ =
let subst = KidSet.fold (fun kid subst ->
match Env.get_typ_var kid env with
| K_type
- | K_order -> subst
+ | K_order
+ | K_bool -> subst
| K_int ->
(match solve env (nvar kid) with
| None -> subst
@@ -4108,7 +4109,7 @@ let add_bitvector_casts (Defs defs) =
| E_app (op,
([E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); y] |
[y; E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_)]))
- when string_of_id op = "eq_atom" ->
+ when string_of_id op = "eq_int" ->
(match destruct_atom_nexp (env_of y) (typ_of y) with
| Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)]
| _ -> [])
diff --git a/src/optimize.ml b/src/optimize.ml
new file mode 100644
index 00000000..a372abf4
--- /dev/null
+++ b/src/optimize.ml
@@ -0,0 +1,100 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Rewriter
+
+let recheck (Defs defs) =
+ let defs = Type_check.check_with_envs Type_check.initial_env defs in
+
+ let rec find_optimizations = function
+ | ([DEF_pragma ("optimize", pragma, p_l)], env)
+ :: ([DEF_spec vs as def1], _)
+ :: ([DEF_fundef fdef as def2], _)
+ :: defs ->
+ let id = id_of_val_spec vs in
+ let args = Str.split (Str.regexp " +") (String.trim pragma) in
+ begin match args with
+ | ["unroll"; n]->
+ let n = int_of_string n in
+
+ let rw_app subst (fn, args) =
+ if Id.compare id fn = 0 then E_app (subst, args) else E_app (fn, args)
+ in
+ let rw_exp subst = { id_exp_alg with e_app = rw_app subst } in
+ let rw_defs subst = { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rw_exp subst)) } in
+
+ let specs = ref [def1] in
+ let bodies = ref [rewrite_def (rw_defs (append_id id "_unroll_1")) def2] in
+
+ for i = 1 to n do
+ let current_id = append_id id ("_unroll_" ^ string_of_int i) in
+ let next_id = if i = n then current_id else append_id id ("_unroll_" ^ string_of_int (i + 1)) in
+ (* Create a valspec for the new unrolled function *)
+ specs := !specs @ [DEF_spec (rename_valspec current_id vs)];
+ (* Then duplicate it's function body and make it call the next unrolled function *)
+ bodies := !bodies @ [rewrite_def (rw_defs next_id) (DEF_fundef (rename_fundef current_id fdef))]
+ done;
+
+ !specs @ !bodies @ find_optimizations defs
+
+ | _ ->
+ Util.warn ("Unrecognised optimize pragma in this context: " ^ pragma);
+ def1 :: def2 :: find_optimizations defs
+ end
+
+ | (defs, _) :: defs' ->
+ defs @ find_optimizations defs'
+
+ | [] -> []
+ in
+
+ Defs (find_optimizations defs)
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 169bd824..8cef3529 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -359,14 +359,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
let mk_typ nexp =
Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
in
- match Type_check.solve env size with
- | Some n -> mk_typ (nconstant n)
- | None ->
- let is_equal nexp =
- prove __POS__ env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
- in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
- | nexp -> mk_typ nexp
- | exception Not_found -> None
+ let is_equal nexp =
+ prove __POS__ env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
+ in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
+ | nexp -> mk_typ nexp
+ | exception Not_found ->
+ match Type_check.solve env size with
+ | Some n -> mk_typ (nconstant n)
+ | None -> None
end
| _ -> None
diff --git a/src/process_file.ml b/src/process_file.ml
index ed34238b..00013775 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -51,6 +51,10 @@
open PPrint
open Pretty_print_common
+let opt_lem_output_dir = ref None
+let opt_isa_output_dir = ref None
+let opt_coq_output_dir = ref None
+
type out_type =
| Lem_out of string list
| Coq_out of string list
@@ -254,19 +258,24 @@ let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tanno
(ast, env)
-let open_output_with_check file_name =
+let open_output_with_check opt_dir file_name =
let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
let o' = Format.formatter_of_out_channel o in
- (o', (o, temp_file_name, file_name))
+ (o', (o, temp_file_name, opt_dir, file_name))
-let open_output_with_check_unformatted file_name =
+let open_output_with_check_unformatted opt_dir file_name =
let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
- (o, temp_file_name, file_name)
+ (o, temp_file_name, opt_dir, file_name)
let always_replace_files = ref true
-let close_output_with_check (o, temp_file_name, file_name) =
+let close_output_with_check (o, temp_file_name, opt_dir, file_name) =
let _ = close_out o in
+ let file_name = match opt_dir with
+ | None -> file_name
+ | Some dir -> if Sys.file_exists dir then ()
+ else Unix.mkdir dir 0o775;
+ Filename.concat dir file_name in
let do_replace = !always_replace_files || (not (Util.same_content_files temp_file_name file_name)) in
let _ = if (not do_replace) then Sys.remove temp_file_name
else Util.move_file temp_file_name file_name in
@@ -308,22 +317,22 @@ let output_lem filename libs type_env defs =
string "end"
] ^^ hardline
in
- let ((ot,_, _) as ext_ot) =
- open_output_with_check_unformatted (filename ^ "_types" ^ ".lem") in
- let ((o,_, _) as ext_o) =
- open_output_with_check_unformatted (filename ^ ".lem") in
+ let ((ot,_,_,_) as ext_ot) =
+ open_output_with_check_unformatted !opt_lem_output_dir (filename ^ "_types" ^ ".lem") in
+ let ((o,_,_,_) as ext_o) =
+ open_output_with_check_unformatted !opt_lem_output_dir (filename ^ ".lem") in
(Pretty_print.pp_defs_lem
(ot, base_imports)
(o, base_imports @ (String.capitalize_ascii types_module :: libs))
type_env defs generated_line);
close_output_with_check ext_ot;
close_output_with_check ext_o;
- let ((ol, _, _) as ext_ol) =
- open_output_with_check_unformatted (isa_thy_name ^ ".thy") in
+ let ((ol,_,_,_) as ext_ol) =
+ open_output_with_check_unformatted !opt_isa_output_dir (isa_thy_name ^ ".thy") in
print ol isa_lemmas;
close_output_with_check ext_ol
-let output_coq filename libs defs =
+let output_coq opt_dir filename libs defs =
let generated_line = generated_line filename in
let types_module = (filename ^ "_types") in
let monad_modules = ["Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_state"] in
@@ -336,10 +345,10 @@ let output_coq filename libs defs =
operators_module
] @ monad_modules
in
- let ((ot,_, _) as ext_ot) =
- open_output_with_check_unformatted (filename ^ "_types" ^ ".v") in
- let ((o,_, _) as ext_o) =
- open_output_with_check_unformatted (filename ^ ".v") in
+ let ((ot,_,_,_) as ext_ot) =
+ open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in
+ let ((o,_,_,_) as ext_o) =
+ open_output_with_check_unformatted opt_dir (filename ^ ".v") in
(Pretty_print_coq.pp_defs_coq
(ot, base_imports)
(o, base_imports @ (types_module :: libs))
@@ -357,7 +366,7 @@ let output1 libpath out_arg filename type_env defs =
| Lem_out libs ->
output_lem f' libs type_env defs
| Coq_out libs ->
- output_coq f' libs defs
+ output_coq !opt_coq_output_dir f' libs defs
let output libpath out_arg files =
List.iter
@@ -374,7 +383,7 @@ let rewrite_step n total defs (name, rewriter) =
begin
let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in
(* output "" Lem_ast_out [filename, defs]; *)
- let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in
+ let ((ot,_,_,_) as ext_ot) = open_output_with_check_unformatted None filename in
Pretty_print_sail.pp_defs ot defs;
close_output_with_check ext_ot;
opt_ddump_rewrite_ast := Some (f, i + 1)
diff --git a/src/process_file.mli b/src/process_file.mli
index 181443fb..74d847a5 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -71,6 +71,10 @@ val opt_ddump_tc_ast : bool ref
val opt_ddump_rewrite_ast : ((string * int) option) ref
val opt_dno_cast : bool ref
+val opt_lem_output_dir : (string option) ref
+val opt_isa_output_dir : (string option) ref
+val opt_coq_output_dir : (string option) ref
+
type out_type =
| Lem_out of string list (* If present, the strings are files to open in the lem backend*)
| Coq_out of string list (* If present, the strings are files to open in the coq backend*)
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 19ec6db7..67b6518f 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5162,7 +5162,7 @@ let rewrite_defs_c = [
("trivial_sizeof", rewrite_trivial_sizeof);
("sizeof", rewrite_sizeof);
("merge_function_clauses", merge_funcls);
- ("recheck_defs", recheck_defs)
+ ("recheck_defs", Optimize.recheck)
]
let rewrite_defs_interpreter = [
diff --git a/src/sail.ml b/src/sail.ml
index 6e5e7556..be2a6198 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -111,6 +111,9 @@ let options = Arg.align ([
( "-latex",
Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ],
" pretty print the input to latex");
+ ( "-latex_full_valspecs",
+ Arg.Clear Latex.opt_simple_val,
+ " print full valspecs in latex output latex");
( "-c",
Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen],
" output a C translated version of the input");
@@ -149,6 +152,12 @@ let options = Arg.align ([
( "-lem",
Arg.Set opt_print_lem,
" output a Lem translated version of the input");
+ ( "-lem_output_dir",
+ Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir),
+ " set a custom directory to output generated Lem");
+ ( "-isa_output_dir",
+ Arg.String (fun dir -> Process_file.opt_isa_output_dir := Some dir),
+ " set a custom directory to output generated Isabelle auxiliary theories");
( "-lem_lib",
Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem),
"<filename> provide additional library to open in Lem output");
@@ -161,6 +170,9 @@ let options = Arg.align ([
( "-coq",
Arg.Set opt_print_coq,
" output a Coq translated version of the input");
+ ( "-coq_output_dir",
+ Arg.String (fun dir -> Process_file.opt_coq_output_dir := Some dir),
+ " set a custom directory to output generated Coq");
( "-coq_lib",
Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq),
"<filename> provide additional library to open in Coq output");
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index c0bf80fa..d1a21b73 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -508,6 +508,13 @@ let read_ram (addr_size, data_size, hex_ram, addr) =
Bytes.iter (fun byte -> vector := (byte_of_int (int_of_char byte)) @ !vector) bytes;
!vector
+let fast_read_ram (data_size, addr) =
+ let addr = uint addr in
+ let bytes = read_mem_bytes addr (Big_int.to_int data_size) in
+ let vector = ref [] in
+ Bytes.iter (fun byte -> vector := (byte_of_int (int_of_char byte)) @ !vector) bytes;
+ !vector
+
let tag_ram = (ref Mem.empty : (bool Mem.t) ref);;
let write_tag_bool (addr, tag) =
diff --git a/src/state.ml b/src/state.ml
index fb065440..74bc97b2 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -135,20 +135,20 @@ let generate_initial_regstate defs =
let typ_subst_typquant tq args typ =
List.fold_left2 typ_subst_quant_item typ (quant_items tq) args
in
- let add_typ_init_val vals = function
+ let add_typ_init_val (defs', vals) = function
| TD_enum (id, id1 :: _, _) ->
(* Choose the first value of an enumeration type as default *)
- Bindings.add id (fun _ -> string_of_id id1) vals
+ (defs', Bindings.add id (fun _ -> string_of_id id1) vals)
| TD_variant (id, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) ->
(* Choose the first variant of a union type as default *)
let init_val args =
let typ1 = typ_subst_typquant tq args typ1 in
string_of_id id1 ^ " (" ^ lookup_init_val vals typ1 ^ ")"
in
- Bindings.add id init_val vals
+ (defs', Bindings.add id init_val vals)
| TD_abbrev (id, tq, A_aux (A_typ typ, _)) ->
let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in
- Bindings.add id init_val vals
+ (defs', Bindings.add id init_val vals)
| TD_record (id, tq, fields, _) ->
let init_val args =
let init_field (typ, id) =
@@ -157,16 +157,21 @@ let generate_initial_regstate defs =
in
"struct { " ^ (String.concat ", " (List.map init_field fields)) ^ " }"
in
- Bindings.add id init_val vals
+ let def_name = "initial_" ^ string_of_id id in
+ if quant_items tq = [] && not (is_defined defs def_name) then
+ (defs' @ ["let " ^ def_name ^ " : " ^ string_of_id id ^ " = " ^ init_val []],
+ Bindings.add id (fun _ -> def_name) vals)
+ else (defs', Bindings.add id init_val vals)
| TD_bitfield (id, typ, _) ->
- Bindings.add id (fun _ -> lookup_init_val vals typ) vals
- | _ -> vals
+ (defs', Bindings.add id (fun _ -> lookup_init_val vals typ) vals)
+ | _ -> (defs', vals)
in
- let init_vals = List.fold_left (fun vals def -> match def with
- | DEF_type (TD_aux (td, _)) -> add_typ_init_val vals td
- | _ -> vals) Bindings.empty defs
+ let (init_defs, init_vals) = List.fold_left (fun inits def -> match def with
+ | DEF_type (TD_aux (td, _)) -> add_typ_init_val inits td
+ | _ -> inits) ([], Bindings.empty) defs
in
let init_reg (typ, id) = string_of_id id ^ " = " ^ lookup_init_val init_vals typ in
+ init_defs @
["let initial_regstate : regstate = struct { " ^ (String.concat ", " (List.map init_reg registers)) ^ " }"]
with
| _ -> [] (* Do not generate an initial register state if anything goes wrong *)
diff --git a/src/type_check.ml b/src/type_check.ml
index 11d5e6a0..0da7bb8e 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -4448,14 +4448,18 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm));
let env = Env.add_extern id ext_opt env in
let env = if is_cast then Env.add_cast id env else env in
+ let typq', typ' = expand_bind_synonyms ts_l env (typq, typ) in
+ (* !opt_expand_valspec controls whether the actual valspec in
+ the AST is expanded, the val_spec type stored in the
+ environment is always expanded and uses typq' and typ' *)
let typq, typ =
if !opt_expand_valspec then
- expand_bind_synonyms ts_l env (typq, typ)
+ (typq', typ')
else
(typq, typ)
in
let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in
- (vs, id, typq, typ, env)
+ (vs, id, typq', typ', env)
in
let eff =
match typ with
@@ -4635,6 +4639,14 @@ and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot defs * Env.t =
and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
fun env (Defs defs) -> let total = List.length defs in check_defs 1 total env defs
+and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list =
+ fun env defs ->
+ match defs with
+ | [] -> []
+ | def :: defs ->
+ let def, env = check_def env def in
+ (def, env) :: check_with_envs env defs
+
let initial_env =
Env.empty
|> Env.add_prover (prove __POS__)
diff --git a/src/type_check.mli b/src/type_check.mli
index 522074b3..2663c1c7 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -417,5 +417,9 @@ Some invariants that will hold of a fully checked AST are:
Type_error.check *)
val check : Env.t -> 'a defs -> tannot defs * Env.t
+(** The same as [check], but exposes the intermediate type-checking
+ environments so we don't have to always re-check the entire AST *)
+val check_with_envs : Env.t -> 'a def list -> (tannot def list * Env.t) list
+
(** The initial type checking environment *)
val initial_env : Env.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 02:00:30 +0000