summaryrefslogtreecommitdiff
path: root/src/slice.ml
diff options
context:
space:
mode:
authorAlasdair2019-10-31 22:08:38 +0000
committerAlasdair2019-10-31 22:31:21 +0000
commitd61c5160a637479c264b74d8cefc5c0a67942795 (patch)
treecb7c7a9c14141a2c889f56b55e25bb2bbcba5820 /src/slice.ml
parentb53e4e02517624edaab08f5583d24f6fbaa385fd (diff)
Allow sail to be scripted using sail
Currently the -is option allows a list of interactive commands to be passed to the interactive toplevel, however this is only capable of executing a sequential list of instructions which is quite limiting. This commit allows sail interactive commands to be invoked from sail functions running in the interpreter which can be freely interleaved with ordinary sail code, for example one could test an assertion at each QEMU/GDB breakpoint like so: $include <aarch64.sail> function main() -> unit = { sail_gdb_start("target-select remote localhost:1234"); while true do { sail_gdb_continue(); // Run until breakpoint sail_gdb_sync(); // Sync register state with QEMU if not(my_assertion()) { print_endline("Assertion failed") } } }
Diffstat (limited to 'src/slice.ml')
-rw-r--r--src/slice.ml30
1 files changed, 13 insertions, 17 deletions
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"