summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/constant_fold.ml2
-rw-r--r--src/gdbmi.ml31
-rw-r--r--src/interactive.ml68
-rw-r--r--src/interactive.mli15
-rw-r--r--src/isail.ml131
-rw-r--r--src/jib/c_backend.ml9
-rw-r--r--src/jib/jib_ir.ml8
-rw-r--r--src/jib/jib_smt_fuzz.ml2
-rw-r--r--src/jib/jib_util.ml13
-rw-r--r--src/sail.ml25
-rw-r--r--src/slice.ml30
-rw-r--r--src/smtlib.ml2
-rw-r--r--src/specialize.ml8
-rw-r--r--src/value.ml261
14 files changed, 355 insertions, 250 deletions
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 7a7067ef..0b76a633 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -91,7 +91,7 @@ and exp_of_value =
let safe_primops =
List.fold_left
(fun m k -> StringMap.remove k m)
- Value.primops
+ !Value.primops
[ "print_endline";
"prerr_endline";
"putchar";
diff --git a/src/gdbmi.ml b/src/gdbmi.ml
index c992a713..00408388 100644
--- a/src/gdbmi.ml
+++ b/src/gdbmi.ml
@@ -108,32 +108,27 @@ let () =
register_command
~name:"gdb_command"
- ~help:(sprintf ":gdb_command %s - Use specified gdb. Default is \
- gdb-multiarch. This is the correct version on \
- Ubuntu, but other Linux distros and operating \
- systems may differ in how they package gdb with \
- support for multiple architectures."
- (arg "gdb"))
- (fun arg -> gdb_command := arg);
+ ~help:"Use specified gdb. Default is gdb-multiarch. This is the \
+ correct version on Ubuntu, but other Linux distros and \
+ operating systems may differ in how they package gdb with \
+ support for multiple architectures."
+ (ArgString ("gdb", fun arg -> Action (fun () -> gdb_command := arg)));
register_command
~name:"gdb_start"
- ~help:(sprintf ":gdb_start %s? - Start a child GDB process sending %s as the first command, waiting for it to complete"
- (arg "command") (arg "command"))
- gdb_start;
+ ~help:"Start a child GDB process sending :0 as the first command, waiting for it to complete"
+ (ArgString ("command", fun cmd -> Action (fun () -> gdb_start cmd)));
- (fun port ->
+ (ArgString ("port", fun port -> Action (fun () ->
if port = "" then
gdb_start "target-select remote localhost:1234"
else
gdb_start ("target-select remote localhost:" ^ port)
- ) |> register_command
- ~name:"gdb_qemu"
- ~help:(sprintf ":gdb_qemu %s? - Connect GDB to a remote QEMU target on localhost:%s (default is 1234, as per -s option for QEMU)"
- (arg "port") (arg "port"));
+ ))) |> register_command
+ ~name:"gdb_qemu"
+ ~help:"Connect GDB to a remote QEMU target on localhost port :0 (default is 1234, as per -s option for QEMU)";
register_command
~name:"gdb_send"
- ~help:(sprintf ":gdb_send %s? - Send a GDB/MI command to a child GDB process and wait for it to complete"
- (arg "command"))
- gdb_send;
+ ~help:"Send a GDB/MI command to a child GDB process and wait for it to complete"
+ (ArgString ("command", fun cmd -> Action (fun () -> gdb_send cmd)));
diff --git a/src/interactive.ml b/src/interactive.ml
index 12a1be64..0fad3caf 100644
--- a/src/interactive.ml
+++ b/src/interactive.ml
@@ -48,21 +48,85 @@
(* SUCH DAMAGE. *)
(**************************************************************************)
+open Ast
+open Ast_util
+open Printf
+
let opt_interactive = ref false
let opt_emacs_mode = ref false
let opt_suppress_banner = ref false
let env = ref Type_check.initial_env
-let ast = ref (Ast.Defs [])
+let ast = ref (Defs [])
let arg str =
("<" ^ str ^ ">") |> Util.yellow |> Util.clear
let command str =
- (":" ^ str) |> Util.green |> Util.clear
+ str |> Util.green |> Util.clear
+
+type action =
+ | ArgString of string * (string -> action)
+ | ArgInt of string * (int -> action)
+ | Action of (unit -> unit)
let commands = ref []
+
+let reflect_typ action =
+ let open Type_check in
+ let rec arg_typs = function
+ | ArgString (_, next) -> string_typ :: arg_typs (next "")
+ | ArgInt (_, next) -> int_typ :: arg_typs (next 0)
+ | Action _ -> []
+ in
+ function_typ (arg_typs action) unit_typ no_effect
+
+let generate_help name help action =
+ let rec args = function
+ | ArgString (hint, next) -> arg hint :: args (next "")
+ | ArgInt (hint, next) -> arg hint :: args (next 0)
+ | Action _ -> []
+ in
+ let args = args action in
+ let help = match String.split_on_char ':' help with
+ | [] -> assert false
+ | (prefix :: splits) ->
+ List.map (fun split ->
+ match String.split_on_char ' ' split with
+ | [] -> assert false
+ | (subst :: rest) ->
+ if Str.string_match (Str.regexp "^[0-9]+") subst 0 then
+ let num_str = Str.matched_string subst in
+ let num_end = Str.match_end () in
+ let punct = String.sub subst num_end (String.length subst - num_end) in
+ List.nth args (int_of_string num_str) ^ punct ^ " " ^ String.concat " " rest
+ else
+ command (":" ^ subst) ^ " " ^ String.concat " " rest
+ ) splits
+ |> String.concat ""
+ |> (fun rest -> prefix ^ rest)
+ in
+ sprintf "%s %s - %s" Util.(name |> green |> clear) (String.concat ", " args) help
+let run_action cmd argument action =
+ let args = String.split_on_char ',' argument in
+ let rec call args action =
+ match args, action with
+ | (x :: xs), ArgString (hint, next) ->
+ call xs (next (String.trim x))
+ | (x :: xs), ArgInt (hint, next) ->
+ let x = String.trim x in
+ if Str.string_match (Str.regexp "^[0-9]+$") x 0 then
+ call xs (next (int_of_string x))
+ else
+ print_endline (sprintf "%s argument %s must be an non-negative integer" (command cmd) (arg hint))
+ | _, Action act ->
+ act ()
+ | _, _ ->
+ print_endline (sprintf "Bad arguments for %s, see (%s %s)" (command cmd) (command ":help") (command cmd))
+ in
+ call args action
+
let register_command ~name:name ~help:help action =
commands := (":" ^ name, (help, action)) :: !commands
diff --git a/src/interactive.mli b/src/interactive.mli
index b1df0630..933d0a46 100644
--- a/src/interactive.mli
+++ b/src/interactive.mli
@@ -62,6 +62,17 @@ val env : Env.t ref
val arg : string -> string
val command : string -> string
-val commands : (string * (string * (string -> unit))) list ref
+type action =
+ | ArgString of string * (string -> action)
+ | ArgInt of string * (int -> action)
+ | Action of (unit -> unit)
-val register_command : name:string -> help:string -> (string -> unit) -> unit
+val reflect_typ : action -> typ
+
+val commands : (string * (string * action)) list ref
+
+val register_command : name:string -> help:string -> action -> unit
+
+val generate_help : string -> string -> action -> string
+
+val run_action : string -> string -> action -> unit
diff --git a/src/isail.ml b/src/isail.ml
index 68be2bc9..138d8d31 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -109,28 +109,73 @@ let sail_logo =
in
List.map banner logo @ [""] @ help @ [""]
+let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear
+
let vs_ids = ref (val_spec_ids !Interactive.ast)
-let interactive_state = ref (initial_state ~registers:false !Interactive.ast !Interactive.env Value.primops)
-
-let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear
+let interactive_state = ref (initial_state ~registers:false !Interactive.ast !Interactive.env !Value.primops)
+(* We can't set up the elf commands in elf_loader.ml because it's used
+ by Sail OCaml emulators at runtime, so set them up here. *)
let () =
let open Interactive in
let open Elf_loader in
- let open Printf in
- register_command ~name:"elf" ~help:(sprintf ":elf %s - Load an elf file" (arg "file")) load_elf;
+ ArgString ("file", fun file -> Action (fun () -> load_elf file))
+ |> register_command ~name:"elf" ~help:"Load an elf file";
+
+ ArgString ("addr", fun addr_s -> ArgString ("file", fun filename -> Action (fun () ->
+ let addr = Big_int.of_string addr_s in
+ load_binary addr filename
+ ))) |> register_command ~name:"bin" ~help:"Load a raw binary file at :0. Use :elf to load an ELF"
- (fun iarg ->
- match Util.split_on_char ' ' iarg with
- | [addr_s; filename] ->
- let addr = Big_int.of_string addr_s in
- load_binary addr filename
- | _ ->
- printf "Invalid argument for :bin, expected %s %s" (arg "addr") (arg "file")
- ) |> register_command ~name:"bin" ~help:(sprintf ":bin %s %s - Load a binary file at a given address" (arg "addr") (arg "file"))
+(* This is a feature that lets us take interpreter commands like :foo
+ x, y and turn the into functions that can be called by sail as
+ foo(x, y), which lets us use sail to script itself. The
+ sail_scripting_primops_once variable ensures we only add the
+ commands to the interpreter primops list once, although we may have
+ to reset the AST and env changes when we :load and :unload
+ files by calling this function multiple times. *)
+let sail_scripting_primops_once = ref true
+let setup_sail_scripting () =
+ let open Interactive in
+
+ let sail_command_name cmd = "sail_" ^ String.sub cmd 1 (String.length cmd - 1) in
+
+ let val_specs =
+ List.map (fun (cmd, (_, action)) ->
+ let name = sail_command_name cmd in
+ let typschm = mk_typschm (mk_typquant []) (reflect_typ action) in
+ mk_val_spec (VS_val_spec (typschm, mk_id name, [("_", name)], false))
+ ) !commands in
+ let val_specs, env' = Type_check.check !env (Defs val_specs) in
+ ast := append_ast !ast val_specs;
+ env := env';
+
+ if !sail_scripting_primops_once then (
+ List.iter (fun (cmd, (help, action)) ->
+ let open Value in
+ let name = sail_command_name cmd in
+ let impl values =
+ let rec call values action =
+ match values, action with
+ | (v :: vs), ArgString (_, next) ->
+ call vs (next (coerce_string v))
+ | (v :: vs), ArgInt (_, next) ->
+ call vs (next (Big_int.to_int (coerce_int v)))
+ | _, Action act ->
+ act (); V_unit
+ | _, _ ->
+ failwith help
+ in
+ call values action
+ in
+ Value.add_primop name impl
+ ) !commands;
+ sail_scripting_primops_once := false
+ )
+
let print_program () =
match !current_mode with
| Normal | Emacs -> ()
@@ -283,7 +328,7 @@ let help =
(color green ":commands") (color green ":help") (color yellow "<command>")
| cmd ->
match List.assoc_opt cmd !Interactive.commands with
- | Some (help, _) -> help
+ | Some (help_message, action) -> Interactive.generate_help cmd help_message action
| None ->
sprintf "Either invalid command passed to help, or no documentation for %s. Try %s."
(color green cmd) (color green ":help :help")
@@ -466,13 +511,13 @@ let handle_input' input =
let files = Util.split_on_char ' ' arg in
let (_, ast, env) = load_files !Interactive.env files in
Interactive.ast := append_ast !Interactive.ast ast;
- interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
Interactive.env := env;
vs_ids := val_spec_ids !Interactive.ast
| ":u" | ":unload" ->
Interactive.ast := Ast.Defs [];
Interactive.env := Type_check.initial_env;
- interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
vs_ids := val_spec_ids !Interactive.ast;
(* See initial_check.mli for an explanation of why we need this. *)
Initial_check.have_undefined_builtins := false;
@@ -494,7 +539,7 @@ let handle_input' input =
let ast, env = Type_check.check !Interactive.env (Defs [DEF_val (mk_letbind (mk_pat (P_id (mk_id v))) exp)]) in
Interactive.ast := append_ast !Interactive.ast ast;
Interactive.env := env;
- interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
| _ -> print_endline "Invalid arguments for :let"
end
| ":def" ->
@@ -502,7 +547,7 @@ let handle_input' input =
let ast, env = Type_check.check !Interactive.env ast in
Interactive.ast := append_ast !Interactive.ast ast;
Interactive.env := env;
- interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
| ":list_rewrites" ->
let print_rewrite (name, rw) =
print_endline (name ^ " " ^ Util.(String.concat " " (describe_rewrite rw) |> yellow |> clear))
@@ -538,17 +583,17 @@ let handle_input' input =
let new_ast, new_env = Process_file.rewrite_ast_target arg !Interactive.env !Interactive.ast in
Interactive.ast := new_ast;
Interactive.env := new_env;
- interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
+ interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops
| ":prover_regstate" ->
let env, ast = prover_regstate (Some arg) !Interactive.ast !Interactive.env in
Interactive.env := env;
Interactive.ast := ast;
- interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
+ interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops
| ":recheck" ->
let ast, env = Type_check.check Type_check.initial_env !Interactive.ast in
Interactive.env := env;
Interactive.ast := ast;
- interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
vs_ids := val_spec_ids !Interactive.ast
| ":recheck_types" ->
let ast, env = Type_check.check Type_check.initial_env !Interactive.ast in
@@ -563,7 +608,7 @@ let handle_input' input =
target (Some arg) out_name !Interactive.ast !Interactive.env
| _ ->
match List.assoc_opt cmd !Interactive.commands with
- | Some (_, action) -> action arg
+ | Some (_, action) -> Interactive.run_action cmd arg action
| None -> unrecognised_command cmd
end
| Expression str ->
@@ -585,7 +630,7 @@ let handle_input' input =
load_into_session arg;
let (_, ast, env) = load_files ~check:true !Interactive.env [arg] in
Interactive.ast := append_ast !Interactive.ast ast;
- interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
Interactive.env := env;
vs_ids := val_spec_ids !Interactive.ast;
print_endline ("(message \"Checked " ^ arg ^ " done\")\n");
@@ -596,7 +641,7 @@ let handle_input' input =
| ":unload" ->
Interactive.ast := Ast.Defs [];
Interactive.env := Type_check.initial_env;
- interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
vs_ids := val_spec_ids !Interactive.ast;
Initial_check.have_undefined_builtins := false;
Process_file.clear_symbols ()
@@ -775,28 +820,26 @@ let () =
);
(* Read the script file if it is set with the -is option, and excute them *)
- begin
- match !opt_interactive_script with
- | None -> ()
- | Some file ->
- let chan = open_in file in
- try
- while true do
- let line = input_line chan in
- handle_input line;
- done;
- with
- | End_of_file -> ()
+ begin match !opt_interactive_script with
+ | None -> ()
+ | Some file ->
+ let chan = open_in file in
+ try
+ while true do
+ let line = input_line chan in
+ handle_input line;
+ done;
+ with
+ | End_of_file -> ()
end;
LNoise.history_load ~filename:"sail_history" |> ignore;
LNoise.history_set ~max_length:100 |> ignore;
- if !Interactive.opt_interactive then
- begin
- if not !Interactive.opt_emacs_mode then
- List.iter print_endline sail_logo
- else (current_mode := Emacs; Util.opt_colors := false);
- user_input handle_input
- end
- else ()
+ if !Interactive.opt_interactive then (
+ if not !Interactive.opt_emacs_mode then
+ List.iter print_endline sail_logo
+ else (current_mode := Emacs; Util.opt_colors := false);
+ setup_sail_scripting ();
+ user_input handle_input
+ )
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 98ee5bc1..c1f2d24c 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -1022,7 +1022,7 @@ let optimize recursive_functions cdefs =
let sgen_id id = Util.zencode_string (string_of_id id)
let sgen_uid uid = zencode_uid uid
-let sgen_name id = string_of_name id
+let sgen_name id = string_of_name ~deref_current_exception:true ~zencode:true id
let codegen_id id = string (sgen_id id)
let codegen_uid id = string (sgen_uid id)
@@ -1110,8 +1110,8 @@ let sgen_value = function
| VL_string str -> "\"" ^ str ^ "\""
let rec sgen_cval = function
- | V_id (id, ctyp) -> string_of_name id
- | V_ref (id, _) -> "&" ^ string_of_name id
+ | V_id (id, ctyp) -> sgen_name id
+ | V_ref (id, _) -> "&" ^ sgen_name id
| V_lit (vl, ctyp) -> sgen_value vl
| V_call (op, cvals) -> sgen_call op cvals
| V_field (f, field) ->
@@ -2182,7 +2182,8 @@ let compile_ast env output_chan c_includes ast =
let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in
let cdefs, ctx = jib_of_ast env ast in
- Jib_interactive.ir := cdefs;
+ let cdefs', _ = Jib_optimize.remove_tuples cdefs ctx in
+ Jib_interactive.ir := cdefs';
let cdefs = insert_heap_returns Bindings.empty cdefs in
let cdefs = optimize recursive_functions cdefs in
diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml
index c5f2b20a..2fdc4b88 100644
--- a/src/jib/jib_ir.ml
+++ b/src/jib/jib_ir.ml
@@ -244,7 +244,7 @@ let () =
let open Interactive in
let open Jib_interactive in
- (fun arg ->
+ ArgString ("(val|register)? identifier", fun arg -> Action (fun () ->
let is_def id = function
| CDEF_fundef (id', _, _, _) -> Id.compare id id' = 0
| CDEF_spec (id', _, _) -> Id.compare id (prepend_id "val " id') = 0
@@ -258,12 +258,12 @@ let () =
let buf = Buffer.create 256 in
with_colors (fun () -> Flat_ir_formatter.output_def buf cdef);
print_endline (Buffer.contents buf)
- ) |> Interactive.(register_command ~name:"ir" ~help:(sprintf ":ir %s - Print the ir representation of a toplevel definition" (arg "(val|register)? identifier")));
+ )) |> Interactive.register_command ~name:"ir" ~help:"Print the ir representation of a toplevel definition";
- (fun file ->
+ ArgString ("file", fun file -> Action (fun () ->
let buf = Buffer.create 256 in
let out_chan = open_out file in
Flat_ir_formatter.output_defs buf !ir;
output_string out_chan (Buffer.contents buf);
close_out out_chan
- ) |> Interactive.(register_command ~name:"dump_ir" ~help:(sprintf ":dump_ir %s - Dump the ir to a file" (arg "file")))
+ )) |> Interactive.register_command ~name:"dump_ir" ~help:"Dump the ir to a file"
diff --git a/src/jib/jib_smt_fuzz.ml b/src/jib/jib_smt_fuzz.ml
index 846d0178..02e70e29 100644
--- a/src/jib/jib_smt_fuzz.ml
+++ b/src/jib/jib_smt_fuzz.ml
@@ -158,7 +158,7 @@ let fuzz_cdef ctx all_cdefs = function
if Env.is_extern id ctx.tc_env "smt" then (
let extern = Env.get_extern id ctx.tc_env "smt" in
let typq, (Typ_aux (aux, _) as typ) = Env.get_val_spec id ctx.tc_env in
- let istate = initial_state ctx.ast ctx.tc_env Value.primops in
+ let istate = initial_state ctx.ast ctx.tc_env !Value.primops in
let header = smt_header ctx all_cdefs in
prerr_endline (Util.("Fuzz: " |> cyan |> clear) ^ string_of_id id ^ " = \"" ^ extern ^ "\" : " ^ string_of_typ typ);
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 13438208..bec4ce75 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -257,8 +257,7 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) =
(* 1. Instruction pretty printer *)
(**************************************************************************)
-
-let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) =
+let string_of_name ?deref_current_exception:(dce=false) ?zencode:(zencode=true) =
let ssa_num n = if n = -1 then "" else ("/" ^ string_of_int n) in
function
| Name (id, n) ->
@@ -377,16 +376,10 @@ let rec string_of_cval = function
Printf.sprintf "%s.%s" (string_of_cval f) (string_of_uid field)
| V_tuple_member (f, _, n) ->
Printf.sprintf "%s.ztup%d" (string_of_cval f) n
- | V_ctor_kind (f, ctor, [], _) ->
- string_of_cval f ^ " is " ^ Util.zencode_string (string_of_id ctor)
| V_ctor_kind (f, ctor, unifiers, _) ->
- string_of_cval f ^ " is " ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
- | V_ctor_unwrap (ctor, f, [], _) ->
- Printf.sprintf "%s as %s" (string_of_cval f) (string_of_id ctor)
+ string_of_cval f ^ " is " ^ string_of_uid (ctor, unifiers)
| V_ctor_unwrap (ctor, f, unifiers, _) ->
- Printf.sprintf "%s as %s"
- (string_of_cval f)
- (Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers))
+ string_of_cval f ^ " as " ^ string_of_uid (ctor, unifiers)
| V_struct (fields, _) ->
Printf.sprintf "{%s}"
(Util.string_of_list ", " (fun (field, cval) -> string_of_uid field ^ " = " ^ string_of_cval cval) fields)
diff --git a/src/sail.ml b/src/sail.ml
index e792e652..0656aefa 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -418,21 +418,19 @@ let load_files ?check:(check=false) type_envs files =
if !opt_memo_z3 then Constraint.save_digests () else ();
- if check then
- ("out.sail", ast, type_envs)
- else
- let ast = Scattered.descatter ast in
- let ast, type_envs = rewrite_ast_initial type_envs ast in
- (* Recheck after descattering so that the internal type environments always
- have complete variant types *)
- let ast, type_envs = Type_error.check Type_check.initial_env ast in
+ let out_name = match !opt_file_out with
+ | None when parsed = [] -> "out.sail"
+ | None -> fst (List.hd parsed)
+ | Some f -> f ^ ".sail" in
- let out_name = match !opt_file_out with
- | None when parsed = [] -> "out.sail"
- | None -> fst (List.hd parsed)
- | Some f -> f ^ ".sail" in
+ (out_name, ast, type_envs)
- (out_name, ast, type_envs)
+let descatter type_envs ast =
+ let ast = Scattered.descatter ast in
+ let ast, type_envs = rewrite_ast_initial type_envs ast in
+ (* Recheck after descattering so that the internal type environments
+ always have complete variant types *)
+ Type_error.check Type_check.initial_env ast
let prover_regstate tgt ast type_envs =
match tgt with
@@ -577,6 +575,7 @@ let main () =
else
begin
let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in
+ let ast, type_envs = descatter type_envs ast in
let ast, type_envs =
List.fold_right (fun file (ast,_) -> Splice.splice ast file)
(!opt_splice) (ast, type_envs)
diff --git a/src/slice.ml b/src/slice.ml
index 1ac390bd..83010733 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -361,24 +361,20 @@ let () =
let slice_roots = ref IdSet.empty in
let slice_cuts = ref IdSet.empty in
- (fun arg ->
+ ArgString ("identifiers", fun arg -> Action (fun () ->
let args = Str.split (Str.regexp " +") arg in
let ids = List.map mk_id args |> IdSet.of_list in
Specialize.add_initial_calls ids;
slice_roots := IdSet.union ids !slice_roots
- ) |> register_command
- ~name:"slice_roots"
- ~help:(sprintf ":slice_roots %s - Set the roots for %s" (arg "identifiers") (command "slice"));
+ )) |> register_command ~name:"slice_roots" ~help:"Set the roots for :slice";
- (fun arg ->
+ ArgString ("identifiers", fun arg -> Action (fun () ->
let args = Str.split (Str.regexp " +") arg in
let ids = List.map mk_id args |> IdSet.of_list in
slice_cuts := IdSet.union ids !slice_cuts
- ) |> register_command
- ~name:"slice_cuts"
- ~help:(sprintf ":slice_cuts %s - Set the roots for %s" (arg "identifiers") (command "slice"));
+ )) |> register_command ~name:"slice_cuts" ~help:"Set the cuts for :slice";
- (fun arg ->
+ Action (fun () ->
let module NodeSet = Set.Make(Node) in
let module G = Graph.Make(Node) in
let g = graph_of_ast !ast in
@@ -388,10 +384,11 @@ let () =
ast := filter_ast cuts g !ast
) |> register_command
~name:"slice"
- ~help:(sprintf ":slice - Slice AST to the definitions which the functions given by %s depend on, up to the functions given by %s"
- (command "slice_roots") (command "slice_cuts"));
+ ~help:"Slice AST to the definitions which the functions given \
+ by :slice_roots depend on, up to the functions given \
+ by :slice_cuts";
- (fun arg ->
+ Action (fun () ->
let module NodeSet = Set.Make(Node) in
let module NodeMap = Map.Make(Node) in
let module G = Graph.Make(Node) in
@@ -409,7 +406,7 @@ let () =
~name:"thin_slice"
~help:(sprintf ":thin_slice - Slice AST to the function definitions given with %s" (command "slice_roots"));
- (fun arg ->
+ ArgString ("format", fun arg -> Action (fun () ->
let format = if arg = "" then "svg" else arg in
let dotfile, out_chan = Filename.open_temp_file "sail_graph_" ".gz" in
let image = Filename.temp_file "sail_graph_" ("." ^ format) in
@@ -418,9 +415,8 @@ let () =
let _ = Unix.system (Printf.sprintf "dot -T%s %s -o %s" format dotfile image) in
let _ = Unix.system (Printf.sprintf "xdg-open %s" image) in
()
- ) |> register_command
- ~name:"graph"
- ~help:(sprintf ":graph %s - Draw a callgraph using dot in %s (default svg if none provided), and open with xdg-open"
- (arg "format") (arg "format"));
+ )) |> register_command
+ ~name:"graph"
+ ~help:"Draw a callgraph using dot in :0 (e.g. svg), and open with xdg-open"
diff --git a/src/smtlib.ml b/src/smtlib.ml
index b90f33a7..06386f61 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -529,7 +529,7 @@ let check_counterexample ast env fname function_id args arg_ctyps arg_smt_names
prerr_endline (sprintf "Solver found counterexample: %s" Util.("ok" |> green |> clear));
let counterexample = build_counterexample args arg_ctyps arg_smt_names model in
List.iter (fun (id, v) -> prerr_endline (" " ^ string_of_id id ^ " -> " ^ string_of_value v)) counterexample;
- let istate = initial_state ast env primops in
+ let istate = initial_state ast env !primops in
let annot = (Parse_ast.Unknown, Type_check.mk_tannot env bool_typ no_effect) in
let call = E_aux (E_app (function_id, List.map (fun (_, v) -> E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot))) counterexample), annot) in
let result = run (Step (lazy "", istate, return call, [])) in
diff --git a/src/specialize.ml b/src/specialize.ml
index 483697ce..e2b0075d 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -602,11 +602,9 @@ let rec specialize_passes n spec env ast =
let specialize = specialize_passes (-1)
let () =
- let open Printf in
let open Interactive in
-
- (fun _ ->
+ Action (fun () ->
let ast', env' = specialize typ_ord_specialization !env !ast in
ast := ast';
- env := env')
- |> register_command ~name:"specialize" ~help:":specialize - Specialize Type and Order type variables in the AST"
+ env := env'
+ ) |> register_command ~name:"specialize" ~help:"Specialize Type and Order type variables in the AST"
diff --git a/src/value.ml b/src/value.ml
index 71d9ffe6..751c10d7 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -620,131 +620,136 @@ let value_decimal_string_of_bits = function
| [v] -> V_string (Sail_lib.decimal_string_of_bits (coerce_bv v))
| _ -> failwith "value decimal_string_of_bits"
-let primops =
- List.fold_left
- (fun r (x, y) -> StringMap.add x y r)
- StringMap.empty
- [ ("and_bool", and_bool);
- ("or_bool", or_bool);
- ("print", value_print);
- ("prerr", fun vs -> (prerr_string (string_of_value (List.hd vs)); V_unit));
- ("dec_str", fun _ -> V_string "X");
- ("print_endline", value_print_endline);
- ("prerr_endline", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit));
- ("putchar", value_putchar);
- ("string_of_int", fun vs -> V_string (string_of_value (List.hd vs)));
- ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs)));
- ("decimal_string_of_bits", value_decimal_string_of_bits);
- ("print_bits", value_print_bits);
- ("print_int", value_print_int);
- ("print_string", value_print_string);
- ("prerr_bits", value_print_bits);
- ("prerr_int", value_print_int);
- ("prerr_string", value_prerr_string);
- ("concat_str", value_concat_str);
- ("eq_int", value_eq_int);
- ("lteq", value_lteq);
- ("gteq", value_gteq);
- ("lt", value_lt);
- ("gt", value_gt);
- ("eq_list", value_eq_list);
- ("eq_bool", value_eq_bool);
- ("eq_string", value_eq_string);
- ("string_startswith", value_string_startswith);
- ("string_drop", value_string_drop);
- ("string_take", value_string_take);
- ("string_length", value_string_length);
- ("eq_bit", value_eq_bit);
- ("eq_anything", value_eq_anything);
- ("length", value_length);
- ("subrange", value_subrange);
- ("access", value_access);
- ("update", value_update);
- ("update_subrange", value_update_subrange);
- ("slice", value_slice);
- ("append", value_append);
- ("append_list", value_append_list);
- ("not", value_not);
- ("not_vec", value_not_vec);
- ("and_vec", value_and_vec);
- ("or_vec", value_or_vec);
- ("xor_vec", value_xor_vec);
- ("uint", value_uint);
- ("sint", value_sint);
- ("get_slice_int", value_get_slice_int);
- ("set_slice_int", value_set_slice_int);
- ("set_slice", value_set_slice);
- ("hex_slice", value_hex_slice);
- ("zero_extend", value_zero_extend);
- ("sign_extend", value_sign_extend);
- ("zeros", value_zeros);
- ("ones", value_ones);
- ("shiftr", value_shiftr);
- ("shiftl", value_shiftl);
- ("shift_bits_left", value_shift_bits_left);
- ("shift_bits_right", value_shift_bits_right);
- ("add_int", value_add_int);
- ("sub_int", value_sub_int);
- ("sub_nat", value_sub_nat);
- ("div_int", value_quotient);
- ("mult_int", value_mult);
- ("mult", value_mult);
- ("quotient", value_quotient);
- ("modulus", value_modulus);
- ("negate", value_negate);
- ("pow2", value_pow2);
- ("int_power", value_int_power);
- ("shr_int", value_shr_int);
- ("shl_int", value_shl_int);
- ("max_int", value_max_int);
- ("min_int", value_min_int);
- ("abs_int", value_abs_int);
- ("add_vec_int", value_add_vec_int);
- ("sub_vec_int", value_sub_vec_int);
- ("add_vec", value_add_vec);
- ("sub_vec", value_sub_vec);
- ("vector_truncate", value_vector_truncate);
- ("vector_truncateLSB", value_vector_truncateLSB);
- ("read_ram", value_read_ram);
- ("write_ram", value_write_ram);
- ("trace_memory_read", fun _ -> V_unit);
- ("trace_memory_write", fun _ -> V_unit);
- ("get_time_ns", fun _ -> V_int (Sail_lib.get_time_ns()));
- ("load_raw", value_load_raw);
- ("to_real", value_to_real);
- ("eq_real", value_eq_real);
- ("lt_real", value_lt_real);
- ("gt_real", value_gt_real);
- ("lteq_real", value_lteq_real);
- ("gteq_real", value_gteq_real);
- ("add_real", value_add_real);
- ("sub_real", value_sub_real);
- ("mult_real", value_mult_real);
- ("round_up", value_round_up);
- ("round_down", value_round_down);
- ("quot_round_zero", value_quot_round_zero);
- ("rem_round_zero", value_rem_round_zero);
- ("quotient_real", value_quotient_real);
- ("abs_real", value_abs_real);
- ("div_real", value_div_real);
- ("sqrt_real", value_sqrt_real);
- ("print_real", value_print_real);
- ("random_real", value_random_real);
- ("undefined_unit", fun _ -> V_unit);
- ("undefined_bit", fun _ -> V_bit Sail_lib.B0);
- ("undefined_int", fun _ -> V_int Big_int.zero);
- ("undefined_nat", fun _ -> V_int Big_int.zero);
- ("undefined_bool", fun _ -> V_bool false);
- ("undefined_bitvector", value_undefined_bitvector);
- ("undefined_vector", value_undefined_vector);
- ("undefined_string", fun _ -> V_string "");
- ("internal_pick", value_internal_pick);
- ("replicate_bits", value_replicate_bits);
- ("Elf_loader.elf_entry", fun _ -> V_int (!Elf_loader.opt_elf_entry));
- ("Elf_loader.elf_tohost", fun _ -> V_int (!Elf_loader.opt_elf_tohost));
- ("string_append", value_string_append);
- ("string_length", value_string_length);
- ("string_startswith", value_string_startswith);
- ("string_drop", value_string_drop);
- ("skip", fun _ -> V_unit);
- ]
+let primops = ref
+ (List.fold_left
+ (fun r (x, y) -> StringMap.add x y r)
+ StringMap.empty
+ [ ("and_bool", and_bool);
+ ("or_bool", or_bool);
+ ("print", value_print);
+ ("prerr", fun vs -> (prerr_string (string_of_value (List.hd vs)); V_unit));
+ ("dec_str", fun _ -> V_string "X");
+ ("print_endline", value_print_endline);
+ ("prerr_endline", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit));
+ ("putchar", value_putchar);
+ ("string_of_int", fun vs -> V_string (string_of_value (List.hd vs)));
+ ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs)));
+ ("decimal_string_of_bits", value_decimal_string_of_bits);
+ ("print_bits", value_print_bits);
+ ("print_int", value_print_int);
+ ("print_string", value_print_string);
+ ("prerr_bits", value_print_bits);
+ ("prerr_int", value_print_int);
+ ("prerr_string", value_prerr_string);
+ ("concat_str", value_concat_str);
+ ("eq_int", value_eq_int);
+ ("lteq", value_lteq);
+ ("gteq", value_gteq);
+ ("lt", value_lt);
+ ("gt", value_gt);
+ ("eq_list", value_eq_list);
+ ("eq_bool", value_eq_bool);
+ ("eq_string", value_eq_string);
+ ("string_startswith", value_string_startswith);
+ ("string_drop", value_string_drop);
+ ("string_take", value_string_take);
+ ("string_length", value_string_length);
+ ("eq_bit", value_eq_bit);
+ ("eq_anything", value_eq_anything);
+ ("length", value_length);
+ ("subrange", value_subrange);
+ ("access", value_access);
+ ("update", value_update);
+ ("update_subrange", value_update_subrange);
+ ("slice", value_slice);
+ ("append", value_append);
+ ("append_list", value_append_list);
+ ("not", value_not);
+ ("not_vec", value_not_vec);
+ ("and_vec", value_and_vec);
+ ("or_vec", value_or_vec);
+ ("xor_vec", value_xor_vec);
+ ("uint", value_uint);
+ ("sint", value_sint);
+ ("get_slice_int", value_get_slice_int);
+ ("set_slice_int", value_set_slice_int);
+ ("set_slice", value_set_slice);
+ ("hex_slice", value_hex_slice);
+ ("zero_extend", value_zero_extend);
+ ("sign_extend", value_sign_extend);
+ ("zeros", value_zeros);
+ ("ones", value_ones);
+ ("shiftr", value_shiftr);
+ ("shiftl", value_shiftl);
+ ("shift_bits_left", value_shift_bits_left);
+ ("shift_bits_right", value_shift_bits_right);
+ ("add_int", value_add_int);
+ ("sub_int", value_sub_int);
+ ("sub_nat", value_sub_nat);
+ ("div_int", value_quotient);
+ ("mult_int", value_mult);
+ ("mult", value_mult);
+ ("quotient", value_quotient);
+ ("modulus", value_modulus);
+ ("negate", value_negate);
+ ("pow2", value_pow2);
+ ("int_power", value_int_power);
+ ("shr_int", value_shr_int);
+ ("shl_int", value_shl_int);
+ ("max_int", value_max_int);
+ ("min_int", value_min_int);
+ ("abs_int", value_abs_int);
+ ("add_vec_int", value_add_vec_int);
+ ("sub_vec_int", value_sub_vec_int);
+ ("add_vec", value_add_vec);
+ ("sub_vec", value_sub_vec);
+ ("vector_truncate", value_vector_truncate);
+ ("vector_truncateLSB", value_vector_truncateLSB);
+ ("read_ram", value_read_ram);
+ ("write_ram", value_write_ram);
+ ("trace_memory_read", fun _ -> V_unit);
+ ("trace_memory_write", fun _ -> V_unit);
+ ("get_time_ns", fun _ -> V_int (Sail_lib.get_time_ns()));
+ ("load_raw", value_load_raw);
+ ("to_real", value_to_real);
+ ("eq_real", value_eq_real);
+ ("lt_real", value_lt_real);
+ ("gt_real", value_gt_real);
+ ("lteq_real", value_lteq_real);
+ ("gteq_real", value_gteq_real);
+ ("add_real", value_add_real);
+ ("sub_real", value_sub_real);
+ ("mult_real", value_mult_real);
+ ("round_up", value_round_up);
+ ("round_down", value_round_down);
+ ("quot_round_zero", value_quot_round_zero);
+ ("rem_round_zero", value_rem_round_zero);
+ ("quotient_real", value_quotient_real);
+ ("abs_real", value_abs_real);
+ ("div_real", value_div_real);
+ ("sqrt_real", value_sqrt_real);
+ ("print_real", value_print_real);
+ ("random_real", value_random_real);
+ ("undefined_unit", fun _ -> V_unit);
+ ("undefined_bit", fun _ -> V_bit Sail_lib.B0);
+ ("undefined_int", fun _ -> V_int Big_int.zero);
+ ("undefined_nat", fun _ -> V_int Big_int.zero);
+ ("undefined_bool", fun _ -> V_bool false);
+ ("undefined_bitvector", value_undefined_bitvector);
+ ("undefined_vector", value_undefined_vector);
+ ("undefined_string", fun _ -> V_string "");
+ ("internal_pick", value_internal_pick);
+ ("replicate_bits", value_replicate_bits);
+ ("Elf_loader.elf_entry", fun _ -> V_int (!Elf_loader.opt_elf_entry));
+ ("Elf_loader.elf_tohost", fun _ -> V_int (!Elf_loader.opt_elf_tohost));
+ ("string_append", value_string_append);
+ ("string_length", value_string_length);
+ ("string_startswith", value_string_startswith);
+ ("string_drop", value_string_drop);
+ ("skip", fun _ -> V_unit);
+ ])
+
+let add_primop name impl =
+ primops := StringMap.add name impl !primops
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:01:15 +0000