diff options
| -rw-r--r-- | src/constant_fold.ml | 8 | ||||
| -rw-r--r-- | src/interactive.ml | 5 | ||||
| -rw-r--r-- | src/interactive.mli | 1 | ||||
| -rw-r--r-- | src/interpreter.ml | 2 | ||||
| -rw-r--r-- | src/isail.ml | 22 | ||||
| -rw-r--r-- | src/sail.ml | 14 | ||||
| -rw-r--r-- | test/c/execute.isail | 1 | ||||
| -rwxr-xr-x | test/c/run_tests.py | 6 |
8 files changed, 49 insertions, 10 deletions
diff --git a/src/constant_fold.ml b/src/constant_fold.ml index 35417ac8..1c273df1 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -374,4 +374,10 @@ let () = ~name:"fix_registers" ~help:"Fix the value of specified registers, specified as a \ list of <register>=<value>. Can also fix a specific \ - register field as <register>.<field>=<value>." + register field as <register>.<field>=<value>. Note that \ + this is not used to set registers normally, but instead \ + fixes their value such that the constant folding rewrite \ + (which is subsequently invoked by this command) will \ + replace register reads with the fixed values. Requires a \ + target (c, lem, etc.), as the set of functions that can \ + be constant folded can differ on a per-target basis." diff --git a/src/interactive.ml b/src/interactive.ml index 2cca944c..93df1dc0 100644 --- a/src/interactive.ml +++ b/src/interactive.ml @@ -55,6 +55,7 @@ open Printf let opt_interactive = ref false let opt_emacs_mode = ref false let opt_suppress_banner = ref false +let opt_auto_interpreter_rewrites = ref false let env = ref Type_check.initial_env @@ -80,7 +81,9 @@ let reflect_typ action = | ArgInt (_, next) -> int_typ :: arg_typs (next 0) | Action _ -> [] in - function_typ (arg_typs action) unit_typ no_effect + match action with + | Action _ -> function_typ [unit_typ] unit_typ no_effect + | _ -> function_typ (arg_typs action) unit_typ no_effect let generate_help name help action = let rec args = function diff --git a/src/interactive.mli b/src/interactive.mli index 933d0a46..b0cce425 100644 --- a/src/interactive.mli +++ b/src/interactive.mli @@ -54,6 +54,7 @@ open Type_check val opt_interactive : bool ref val opt_emacs_mode : bool ref val opt_suppress_banner : bool ref +val opt_auto_interpreter_rewrites : bool ref val ast : tannot defs ref diff --git a/src/interpreter.ml b/src/interpreter.ml index a30e90bc..b3e8fe31 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -961,7 +961,7 @@ let rec initialize_registers allow_registers gstate = begin let env = Type_check.env_of_annot annot in let typ = Type_check.Env.expand_synonyms env typ in - let exp = mk_exp (E_cast (typ, mk_exp (E_lit (mk_lit (L_undef))))) in + let exp = mk_exp (E_cast (typ, mk_exp (E_lit (mk_lit L_undef)))) in let exp = Type_check.check_exp env exp typ in { gstate with registers = Bindings.add id (eval_exp (initial_lstate, gstate) exp) gstate.registers } end diff --git a/src/isail.ml b/src/isail.ml index 02908321..7c4affa3 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -113,7 +113,8 @@ let sep = "-----------------------------------------------------" |> Util.blue | let vs_ids = ref (val_spec_ids !Interactive.ast) -let interactive_state = ref (initial_state ~registers:false !Interactive.ast !Interactive.env !Value.primops) +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. *) @@ -314,6 +315,8 @@ let help = | ":option" -> sprintf ":option %s - Parse string as if it was an option passed on the command line. e.g. :option -help." (color yellow "<string>") + | ":recheck" -> + sprintf ":recheck - Re type-check the Sail AST, and synchronize the interpreters internal state to that AST." | ":rewrite" -> sprintf ":rewrite %s - Apply a rewrite to the AST. %s shows all possible rewrites. See also %s" (color yellow "<rewrite> <args>") (color green ":list_rewrites") (color green ":rewrites") @@ -468,7 +471,7 @@ let handle_input' input = let more_commands = Util.string_of_list " " fst !Interactive.commands in let commands = [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :prove :assume :clear :commands :help :output :option"; - "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :rewrite :rewrites :list_rewrites :compile " ^ more_commands; + "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :recheck :rewrite :rewrites :list_rewrites :compile " ^ more_commands; "Evaluation mode commands - :(r)un :(s)tep :(n)ormal"; ""; ":(c)ommand can be called as either :c or :command." ] @@ -510,9 +513,15 @@ let handle_input' input = | ":l" | ":load" -> let files = Util.split_on_char ' ' arg in let (_, ast, env) = Process_file.load_files options !Interactive.env files in + let ast, env = + if !Interactive.opt_auto_interpreter_rewrites then + Process_file.rewrite_ast_target "interpreter" env ast + else + ast, env + in Interactive.ast := append_ast !Interactive.ast ast; - interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; Interactive.env := env; + interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; vs_ids := val_spec_ids !Interactive.ast | ":u" | ":unload" -> Interactive.ast := Ast.Defs []; @@ -819,6 +828,13 @@ let () = | _ -> None ); + if !Interactive.opt_auto_interpreter_rewrites then ( + let new_ast, new_env = Process_file.rewrite_ast_target "interpreter" !Interactive.env !Interactive.ast in + Interactive.ast := new_ast; + Interactive.env := new_env; + interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops + ); + (* Read the script file if it is set with the -is option, and excute them *) begin match !opt_interactive_script with | None -> () diff --git a/src/sail.ml b/src/sail.ml index ea642470..64e4f8c6 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -77,14 +77,24 @@ let options = Arg.align ([ Arg.String (fun f -> opt_file_out := Some f), "<prefix> select output filename prefix"); ( "-i", - Arg.Tuple [Arg.Set Interactive.opt_interactive], + Arg.Tuple [Arg.Set Interactive.opt_interactive; + Arg.Set Interactive.opt_auto_interpreter_rewrites; + Arg.Set Initial_check.opt_undefined_gen], " start interactive interpreter"); ( "-is", - Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.String (fun s -> opt_interactive_script := Some s)], + Arg.Tuple [Arg.Set Interactive.opt_interactive; + Arg.Set Interactive.opt_auto_interpreter_rewrites; + Arg.Set Initial_check.opt_undefined_gen; + Arg.String (fun s -> opt_interactive_script := Some s)], "<filename> start interactive interpreter and execute commands in script"); ( "-iout", Arg.String (fun file -> Value.output_redirect (open_out file)), "<filename> print interpreter output to file"); + ( "-interact_custom", + Arg.Set Interactive.opt_interactive, + " drop to an interactive session after running Sail. Differs from \ + -i in that it does not set up the interpreter in the interactive \ + shell."); ( "-emacs", Arg.Set Interactive.opt_emacs_mode, " run sail interactively as an emacs mode child process"); diff --git a/test/c/execute.isail b/test/c/execute.isail index 018dd92c..f4b5ea0f 100644 --- a/test/c/execute.isail +++ b/test/c/execute.isail @@ -1,4 +1,3 @@ -:rewrites interpreter initialize_registers() :run main() diff --git a/test/c/run_tests.py b/test/c/run_tests.py index 64c3ae42..c4f0e591 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -26,6 +26,7 @@ def test_c(name, c_opts, sail_opts, valgrind): step('diff {}.result {}.expect'.format(basename, basename)) if valgrind: step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}".format(basename), expected_status = 1 if basename == "exception" else 0) + step('rm {}.c {} {}.result'.format(basename, basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) @@ -40,8 +41,9 @@ def test_interpreter(name): basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: - step('sail -undefined_gen -is execute.isail -iout {}.iresult {}'.format(basename, filename)) + step('sail -is execute.isail -iout {}.iresult {}'.format(basename, filename)) step('diff {}.iresult {}.expect'.format(basename, basename)) + step('rm {}.iresult'.format(basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) @@ -59,6 +61,8 @@ def test_ocaml(name): step('sail -ocaml -ocaml_build_dir _sbuild_{} -o {} {}'.format(basename, basename, filename)) step('./{} 1> {}.oresult'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) step('diff {}.oresult {}.expect'.format(basename, basename)) + step('rm -r _sbuild_{}'.format(basename)) + step('rm {}.oresult {}'.format(basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) |