summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/interactive.ml62
-rw-r--r--src/interactive.mli59
-rw-r--r--src/interpreter.ml2
-rw-r--r--src/isail.ml109
-rw-r--r--src/slice.ml70
5 files changed, 220 insertions, 82 deletions
diff --git a/src/interactive.ml b/src/interactive.ml
index e5fda4cf..cf5c955b 100644
--- a/src/interactive.ml
+++ b/src/interactive.ml
@@ -1,3 +1,52 @@
+(**************************************************************************)
+(* 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. *)
+(**************************************************************************)
let opt_interactive = ref false
let opt_emacs_mode = ref false
@@ -6,3 +55,16 @@ let opt_suppress_banner = ref false
let env = ref Type_check.initial_env
let ast = ref (Ast.Defs [])
+
+let ir = ref []
+
+let arg str =
+ ("<" ^ str ^ ">") |> Util.yellow |> Util.clear
+
+let command str =
+ (":" ^ str) |> Util.green |> Util.clear
+
+let commands = ref []
+
+let register_command ~name:name ~help:help action =
+ commands := (":" ^ name, (help, action)) :: !commands
diff --git a/src/interactive.mli b/src/interactive.mli
index 915193ec..a092ee33 100644
--- a/src/interactive.mli
+++ b/src/interactive.mli
@@ -1,3 +1,53 @@
+(**************************************************************************)
+(* 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 Type_check
@@ -8,3 +58,12 @@ val opt_suppress_banner : bool ref
val ast : tannot defs ref
val env : Env.t ref
+
+val ir : Jib.cdef list ref
+
+val arg : string -> string
+val command : string -> string
+
+val commands : (string * (string * (string -> unit))) list ref
+
+val register_command : name:string -> help:string -> (string -> unit) -> unit
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 6707bc0b..dd322369 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -52,8 +52,6 @@ open Ast
open Ast_util
open Value
-
-
type gstate =
{ registers : value Bindings.t;
allow_registers : bool; (* For some uses we want to forbid touching any registers. *)
diff --git a/src/isail.ml b/src/isail.ml
index bb42804a..7db28ddf 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -55,6 +55,8 @@ open Ast_util
open Interpreter
open Pretty_print_sail
+module Slice = Slice
+
type mode =
| Evaluation of frame
| Normal
@@ -110,10 +112,24 @@ let vs_ids = ref (val_spec_ids !Interactive.ast)
let interactive_state = ref (initial_state !Interactive.ast !Interactive.env Value.primops)
-let interactive_bytecode = ref []
-
let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear
+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;
+
+ (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"))
+
let print_program () =
match !current_mode with
| Normal | Emacs -> ()
@@ -230,11 +246,6 @@ let help =
| ":help" ->
sprintf ":help %s - Get a description of <command>. Commands are prefixed with a colon, e.g. %s."
(color yellow "<command>") (color green ":help :type")
- | ":elf" ->
- sprintf ":elf %s - Load an ELF file."
- (color yellow "<file>")
- | ":bin" ->
- ":bin <address> <file> - Load a binary file at the given address."
| ":r" | ":run" ->
"(:r | :run) - Completely evaluate the currently evaluating expression."
| ":s" | ":step" ->
@@ -266,16 +277,15 @@ let help =
| ":compile" ->
sprintf ":compile %s - Compile AST to a specified target, valid targets are lem, coq, ocaml, c, and ir (intermediate representation)"
(color yellow "<target>")
- | ":slice" ->
- ":slice - Slice AST to the definitions which the functions given by :slice_roots depend on, up to the functions given by :slice_cuts"
- | ":thin_slice" ->
- ":thin_slice - Slice AST to the function definitions given with :slice_roots"
| "" ->
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 "<command>")
| cmd ->
- sprintf "Either invalid command passed to help, or no documentation for %s. Try %s."
- (color green cmd) (color green ":help :help")
+ match List.assoc_opt cmd !Interactive.commands with
+ | Some (help, _) -> help
+ | None ->
+ sprintf "Either invalid command passed to help, or no documentation for %s. Try %s."
+ (color green cmd) (color green ":help :help")
let format_pos_emacs p1 p2 contents =
let open Lexing in
@@ -409,9 +419,10 @@ let handle_input' input =
eval_clear := false
else print_endline "Invalid argument for :clear, expected either :clear on or :clear off"
| ":commands" ->
+ 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";
+ "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :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." ]
@@ -436,18 +447,6 @@ let handle_input' input =
interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
| ":pretty" ->
print_endline (Pretty_print_sail.to_string (Latex.defs !Interactive.ast))
- | ":ir" ->
- print_endline arg;
- let open Jib in
- let open Jib_util in
- let open PPrint in
- let is_cdef = function
- | CDEF_fundef (id, _, _, _) when Id.compare id (mk_id arg) = 0 -> true
- | CDEF_spec (id, _, _) when Id.compare id (mk_id arg) = 0 -> true
- | _ -> false
- in
- let cdefs = List.filter is_cdef !interactive_bytecode in
- print_endline (Pretty_print_sail.to_string (separate_map hardline pp_cdef cdefs))
| ":ast" ->
let chan = open_out arg in
Pretty_print_sail.pp_defs chan !Interactive.ast;
@@ -467,7 +466,6 @@ let handle_input' input =
| Command (cmd, arg) ->
(* Normal mode commands *)
begin match cmd with
- | ":elf" -> Elf_loader.load_elf arg
| ":l" | ":load" ->
let files = Util.split_on_char ' ' arg in
let (_, ast, env) = load_files !Interactive.env files in
@@ -475,16 +473,6 @@ let handle_input' input =
interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
Interactive.env := env;
vs_ids := val_spec_ids !Interactive.ast
- | ":bin" ->
- begin
- let args = Util.split_on_char ' ' arg in
- match args with
- | [addr_s; filename] ->
- let addr = Big_int.of_string addr_s in
- Elf_loader.load_binary addr filename
- | _ ->
- print_endline "Invalid argument for :bin, expected <addr> <filename>"
- end
| ":u" | ":unload" ->
Interactive.ast := Ast.Defs [];
Interactive.env := Type_check.initial_env;
@@ -519,48 +507,6 @@ let handle_input' input =
Interactive.ast := append_ast !Interactive.ast ast;
Interactive.env := env;
interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
- | ":graph" ->
- 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
- Slice.dot_of_ast out_chan !Interactive.ast;
- close_out out_chan;
- 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
- ()
- | ":slice_roots" ->
- 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
- | ":slice_cuts" ->
- 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
- | ":slice" ->
- let open Slice in
- let module SliceNodeSet = Set.Make(Slice.Node) in
- let module G = Graph.Make(Slice.Node) in
- let g = Slice.graph_of_ast !Interactive.ast in
- let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
- let cuts = !slice_cuts |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
- let g = G.prune roots cuts g in
- Interactive.ast := Slice.filter_ast cuts g !Interactive.ast
- | ":thin_slice" ->
- let open Slice in
- let module SliceNodeSet = Set.Make(Slice.Node) in
- let module SliceNodeMap = Map.Make(Slice.Node) in
- let module G = Graph.Make(Slice.Node) in
- let g = Slice.graph_of_ast !Interactive.ast in
- let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
- let keep = function
- | (Function id,_) when IdSet.mem id (!slice_roots) -> None
- | (Function id,_) -> Some (Function id)
- | _ -> None
- in
- let cuts = SliceNodeMap.bindings g |> Util.map_filter keep |> SliceNodeSet.of_list in
- let g = G.prune roots cuts g in
- Interactive.ast := Slice.filter_ast cuts g !Interactive.ast
| ":list_rewrites" ->
let print_rewrite (name, rw) =
print_endline (name ^ " " ^ Util.(String.concat " " (describe_rewrite rw) |> yellow |> clear))
@@ -619,7 +565,10 @@ let handle_input' input =
| Some f -> f ^ ".sail"
in
target (Some arg) out_name !Interactive.ast !Interactive.env
- | _ -> unrecognised_command cmd
+ | _ ->
+ match List.assoc_opt cmd !Interactive.commands with
+ | Some (_, action) -> action arg
+ | None -> unrecognised_command cmd
end
| Expression str ->
(* An expression in normal mode is type checked, then puts
diff --git a/src/slice.ml b/src/slice.ml
index 0011bb4d..1ac390bd 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -354,3 +354,73 @@ let dot_of_ast out_chan ast =
let module NodeSet = Set.Make(Node) in
let g = graph_of_ast ast in
G.make_dot (node_color NodeSet.empty) edge_color node_string out_chan g
+
+let () =
+ let open Printf in
+ let open Interactive in
+ let slice_roots = ref IdSet.empty in
+ let slice_cuts = ref IdSet.empty in
+
+ (fun arg ->
+ 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"));
+
+ (fun arg ->
+ 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"));
+
+ (fun arg ->
+ let module NodeSet = Set.Make(Node) in
+ let module G = Graph.Make(Node) in
+ let g = graph_of_ast !ast in
+ let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> NodeSet.of_list in
+ let cuts = !slice_cuts |> IdSet.elements |> List.map (fun id -> Function id) |> NodeSet.of_list in
+ let g = G.prune roots cuts g in
+ 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"));
+
+ (fun arg ->
+ let module NodeSet = Set.Make(Node) in
+ let module NodeMap = Map.Make(Node) in
+ let module G = Graph.Make(Node) in
+ let g = graph_of_ast !ast in
+ let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> NodeSet.of_list in
+ let keep = function
+ | (Function id,_) when IdSet.mem id (!slice_roots) -> None
+ | (Function id,_) -> Some (Function id)
+ | _ -> None
+ in
+ let cuts = NodeMap.bindings g |> Util.map_filter keep |> NodeSet.of_list in
+ let g = G.prune roots cuts g in
+ ast := filter_ast cuts g !ast
+ ) |> register_command
+ ~name:"thin_slice"
+ ~help:(sprintf ":thin_slice - Slice AST to the function definitions given with %s" (command "slice_roots"));
+
+ (fun arg ->
+ 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
+ dot_of_ast out_chan !ast;
+ close_out out_chan;
+ 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"));
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 22:16:41 +0000