From e1e79f46a0d0ad69104e5244916df35056dd1256 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Sat, 15 Jun 2024 23:00:22 +0100 Subject: [PATCH] Change interpreter to not reset state between commands --- src/bin/repl.ml | 74 ++++++++++++++++++++++++++++++++++------ src/lib/jib_util.ml | 2 +- test/c/cheri_capreg.sail | 2 +- test/sailtest.py | 4 +-- test/sv/run_tests.py | 1 + 5 files changed, 69 insertions(+), 14 deletions(-) diff --git a/src/bin/repl.ml b/src/bin/repl.ml index 3c94f3a18..21f6e76bb 100644 --- a/src/bin/repl.ml +++ b/src/bin/repl.ml @@ -77,6 +77,8 @@ module Callgraph_commands = Callgraph_commands type mode = Evaluation of frame | Normal +type display_options = { clear : bool; registers : IdSet.t } + type istate = { ast : Type_check.typed_ast; effect_info : Effects.side_effect_info; @@ -85,7 +87,7 @@ type istate = { vs_ids : IdSet.t ref; options : (Arg.key * Arg.spec * Arg.doc) list; mode : mode; - clear : bool; + display_options : display_options; state : Interpreter.lstate * Interpreter.gstate; default_sail_dir : string; config : Yojson.Basic.t option; @@ -109,8 +111,8 @@ let initial_istate config options env effect_info ast = vs_ids = ref (val_spec_ids ast.defs); options; mode = Normal; - clear = true; - state = initial_state ~registers:false empty_ast Type_check.initial_env !Value.primops; + display_options = { clear = true; registers = IdSet.empty }; + state = initial_state ast env !Value.primops; default_sail_dir = Locations.sail_dir; config; } @@ -124,12 +126,27 @@ let setup_interpreter_state istate = default_sail_dir = istate.default_sail_dir; config = istate.config; }; - { istate with state = initial_state istate.ast istate.env !Value.primops } - -let prompt istate = match istate.mode with Normal -> "sail> " | Evaluation _ -> "eval> " + istate + +let prompt istate = + if not (IdSet.is_empty istate.display_options.registers) then ( + let _, gstate = istate.state in + print_endline ("---- registers ----" |> Util.cyan |> Util.clear); + List.iter + (fun reg -> + match Bindings.find_opt reg gstate.registers with + | Some value -> + print_endline (string_of_id reg ^ " = " ^ (Value.string_of_value value |> Util.green |> Util.clear)) + | None -> print_endline ("No register " ^ string_of_id reg) + ) + (IdSet.elements istate.display_options.registers) + ); + match istate.mode with Normal -> "sail> " | Evaluation _ -> "eval> " let mode_clear istate = - match istate.mode with Normal -> () | Evaluation _ -> if istate.clear then LNoise.clear_screen () else () + match istate.mode with + | Normal -> () + | Evaluation _ -> if istate.display_options.clear then LNoise.clear_screen () else () let rec user_input istate callback = match LNoise.linenoise (prompt istate) with @@ -382,6 +399,12 @@ let help = | ":rewrite" -> sprintf ":rewrite %s - Apply a rewrite to the AST. %s shows all possible rewrites. See also %s" (color yellow " ") (color green ":list_rewrites") (color green ":rewrites") + | ":show_register" | ":show_registers" -> + sprintf ":show_register %s - Print the value of the registers above the prompt." + (color yellow " ...") + | ":hide_register" | ":hide_registers" -> + sprintf ":hide_register %s - Do not print the value of the registers above the prompt." + (color yellow " ...") | "" -> sprintf "Type %s for a list of commands, and %s %s for information about a specific command" (color green ":commands") (color green ":help") (color yellow "") @@ -453,8 +476,10 @@ let handle_input' istate input = Type_check.set_tc_debug (int_of_string arg); istate | ":clear" -> - if arg = "on" || arg = "true" then { istate with clear = true } - else if arg = "off" || arg = "false" then { istate with clear = false } + if arg = "on" || arg = "true" then + { istate with display_options = { istate.display_options with clear = true } } + else if arg = "off" || arg = "false" then + { istate with display_options = { istate.display_options with clear = false } } else ( print_endline "Invalid argument for :clear, expected either :clear on or :clear off"; istate @@ -464,7 +489,7 @@ let handle_input' istate input = let commands = [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :prove :assume :clear :commands :help \ - :output :option"; + :output :option :show_register :hide_register"; "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :recheck :compile " ^ more_commands; "Evaluation mode commands - :(r)un :(s)tep :step_(f)unction :(n)ormal"; ""; @@ -507,6 +532,35 @@ let handle_input' istate input = | ":help" -> print_endline (help arg); istate + | ":show_register" | ":show_registers" -> + let args = Str.split (Str.regexp " +") arg in + List.fold_left + (fun istate arg -> + let display_options = istate.display_options in + let display_options = + { display_options with registers = IdSet.add (mk_id arg) display_options.registers } + in + { istate with display_options } + ) + istate args + | ":hide_register" | ":hide_registers" -> + let args = Str.split (Str.regexp " +") arg in + List.fold_left + (fun istate arg -> + let display_options = istate.display_options in + let reg = mk_id arg in + if IdSet.mem reg display_options.registers then ( + let display_options = + { display_options with registers = IdSet.remove (mk_id arg) display_options.registers } + in + { istate with display_options } + ) + else ( + print_endline ("Register " ^ arg ^ " is not being displayed"); + istate + ) + ) + istate args | _ -> recognised := false; istate diff --git a/src/lib/jib_util.ml b/src/lib/jib_util.ml index fa1fd1019..131c91426 100644 --- a/src/lib/jib_util.ml +++ b/src/lib/jib_util.ml @@ -322,7 +322,7 @@ let string_of_value = function let rec string_of_cval = function | V_id (id, _) -> string_of_name id - | V_member (id, _) -> string_of_id id + | V_member (id, _) -> Util.zencode_string (string_of_id id) | V_lit (VL_undefined, ctyp) -> string_of_value VL_undefined ^ " : " ^ string_of_ctyp ctyp | V_lit (vl, ctyp) -> string_of_value vl | V_call (op, cvals) -> Printf.sprintf "%s(%s)" (string_of_op op) (Util.string_of_list ", " string_of_cval cvals) diff --git a/test/c/cheri_capreg.sail b/test/c/cheri_capreg.sail index 8c9cb3411..5e4c0247d 100644 --- a/test/c/cheri_capreg.sail +++ b/test/c/cheri_capreg.sail @@ -133,7 +133,7 @@ function capRegToCapStruct(capReg) : CapReg -> CapStruct = length = capReg[63..0] } -function getCapPerms(cap) : CapStruct -> bits(31) = +function getCapPerms(cap) : CapStruct -> bits(31) = ( cap.uperms @ cap.perm_reserved11_14 diff --git a/test/sailtest.py b/test/sailtest.py index 08b076d3e..b3f36ee00 100644 --- a/test/sailtest.py +++ b/test/sailtest.py @@ -6,7 +6,7 @@ import argparse parser = argparse.ArgumentParser("run_tests.py") -parser.add_argument("--hide-errors", help="Hide error information.", action='store_true') +parser.add_argument("--hide-error-output", help="Hide error information.", action='store_true') parser.add_argument("--compact", help="Compact output.", action='store_true') args = parser.parse_args() @@ -91,7 +91,7 @@ def step(string, expected_status=0): compact_char(color.FAIL, 'X') else: print("{}Failed{}: {}".format(color.FAIL, color.END, string)) - if not args.hide_errors: + if not args.hide_error_output: print('{}stdout{}:'.format(color.NOTICE, color.END)) print(out.decode('utf-8')) print('{}stderr{}:'.format(color.NOTICE, color.END)) diff --git a/test/sv/run_tests.py b/test/sv/run_tests.py index 66e4b0f96..f15abb7f1 100755 --- a/test/sv/run_tests.py +++ b/test/sv/run_tests.py @@ -55,6 +55,7 @@ 'lib_hex_bits', # bitvector parsing 'lib_hex_bits_signed', # bitvector parsing 'lib_valid_hex_bits', # bitvector parsing + 'issue202_1', # lists } print("Sail is {}".format(sail))