Merge pull request #15 from formalsec/commands

Add subcommands and man pages

bin/commands/cmd_execute.ml

@@ -0,0 +1,84 @@
+open Whilloc
+open Utils
+module C_Choice = ListChoice.Make (EvalConcrete.M) (HeapConcrete.M)
+module SAF_Choice = ListChoice.Make (EvalSymbolic.M) (HeapArrayFork.M)
+module SAITE_Choice = ListChoice.Make (EvalSymbolic.M) (HeapArrayITE.M)
+module ST_Choice = ListChoice.Make (EvalSymbolic.M) (HeapTree.M)
+module SOPL_Choice = ListChoice.Make (EvalSymbolic.M) (HeapOpList.M)
+module C = Interpreter.Make (EvalConcrete.M) (DFS.M) (HeapConcrete.M) (C_Choice)
+
+module SAF =
+  Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapArrayFork.M) (SAF_Choice)
+
+module SAITE =
+  Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapArrayITE.M) (SAITE_Choice)
+
+module ST = Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapTree.M) (ST_Choice)
+
+module SOPL =
+  Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapOpList.M) (SOPL_Choice)
+
+type mode = 
+  | Concrete
+  | Saf
+  | Saite
+  | St
+  | Sopl
+
+type options = {
+  input : Fpath.t;
+  mode : mode;
+  output : Fpath.t option;
+  verbose : bool;
+}
+
+let mode_to_string = function
+  | Concrete -> "c"
+  | Saf -> "saf"
+  | Saite -> "saite"
+  | St -> "st"
+  | Sopl -> "sopl"
+
+let run ?(no_values = false) input mode =
+  let start = Sys.time () in
+  print_header ();
+  let program = input |> read_file |> parse_program |> create_program in
+  Printf.printf "Input file: %s\nExecution mode: %s\n\n" input (mode_to_string mode);
+  (match mode with
+  | Concrete ->
+      let rets = C.interpret program in
+      List.iter
+        (fun (out, _) ->
+          Format.printf "Outcome: %a@." (Outcome.pp ~no_values) out)
+        rets
+  | Saf ->
+      let rets = SAF.interpret program in
+      List.iter
+        (fun (out, _) ->
+          Format.printf "Outcome: %a@." (Outcome.pp ~no_values) out)
+        rets
+  | Saite ->
+      let rets = SAITE.interpret program in
+      List.iter
+        (fun (out, _) ->
+          Format.printf "Outcome: %a@." (Outcome.pp ~no_values) out)
+        rets
+  | St ->
+      let rets = ST.interpret program in
+      List.iter
+        (fun (out, _) ->
+          Format.printf "Outcome: %a@." (Outcome.pp ~no_values) out)
+        rets
+  | Sopl ->
+      let rets = SOPL.interpret program in
+      List.iter
+        (fun (out, _) ->
+          Format.printf "Outcome: %a@." (Outcome.pp ~no_values) out)
+        rets)
+  (* ;Printf.printf "Total Execution time of Solver: %f\n" (!Translator.solver_time) *);
+  if !Utils.verbose then
+    Printf.printf "Total Execution time: %f\n" (Sys.time () -. start)
+
+let main (opts : options) =
+  Utils.verbose := opts.verbose;
+  run (Fpath.to_string opts.input) opts.mode

bin/commands/cmd_test.ml

@@ -0,0 +1,48 @@
+open Whilloc
+
+exception Timeout
+
+type options = {
+  inputs : Fpath.t;
+  mode : Cmd_execute.mode;
+  timeout : float option;
+  verbose : bool;
+}
+
+let _max_timeout = ref 0.0
+let unset () = Sys.set_signal Sys.sigalrm Sys.Signal_ignore
+
+let set =
+  let raise n = if n = -2 then raise Timeout in
+  fun () ->
+    Sys.set_signal Sys.sigalrm (Sys.Signal_handle raise);
+    ignore
+    @@ (Unix.setitimer Unix.ITIMER_REAL
+          { Unix.it_interval = 0.; Unix.it_value = !_max_timeout }
+         : Unix.interval_timer_status)
+
+let run_single mode file =
+  try
+    Fun.protect ~finally:unset (fun () ->
+        set ();
+        try Cmd_execute.run file mode ~no_values:true with
+        | Timeout ->
+            Printf.printf
+              "Timeout occurred while processing file: %s (Max Timeout: %f \
+               seconds)\n"
+              file !_max_timeout
+        (* maybe is not the best way to treat exceptions *)
+        | ex ->
+            Printf.printf "Fatal error: exception %s\n" (Printexc.to_string ex))
+  with Timeout -> Printf.printf "General timeout\n"
+
+let run (opts : options) : unit =
+  let files = Dir.get_files opts.inputs in
+  List.iter (run_single opts.mode)
+    (List.map Fpath.to_string (List.sort Fpath.compare files));
+  Printf.printf "Total number of files tested: %d\n" (List.length files)
+
+let main (opts : options) =
+  _max_timeout := Option.value ~default:0.0 opts.timeout;
+  Utils.verbose := opts.verbose;
+  run opts

bin/docs/doc_execute.ml

@@ -0,0 +1,34 @@
+open Cmdliner
+
+let doc = "Executes a program concretely or symbolically depending on the mode"
+let sdocs = Manpage.s_common_options
+
+let description =
+  [
+    "Given a program in the simple \"While\" language, executes the program \
+     concretely or symbolically depending on the mode.";
+    "To run the program concretely, use the mode 'c'.";
+    "To run the program symbolically, there are several modes to choose from. \
+     These modes differs on the memory model that it uses to execute the \
+     program.";
+  ]
+
+let man =
+  [
+    `S Manpage.s_description;
+    `P (List.nth description 0);
+    `P (List.nth description 1);
+    `P (List.nth description 2);
+  ]
+
+let man_xrefs = []
+
+let cmd_options input mode output verbose : Cmd_execute.options =
+  { input; mode; output; verbose }
+
+let options =
+  Term.(
+    const cmd_options $ Options.File.input $ Options.mode $ Options.File.output
+    $ Options.verbose)
+
+let term = Term.(const Cmd_execute.main $ options)

bin/docs/doc_test.ml

@@ -0,0 +1,37 @@
+open Cmdliner
+
+let doc =
+  "Executes all programs with the extension .wl in the given directory and \
+   mode."
+
+let sdocs = Manpage.s_common_options
+
+let description =
+  [
+    "Executes all programs with the extension .wl in the given directory and \
+     mode.";
+    "The difference of running programs using this command and command 'wl \
+     execute' is that this command will run all programs in the given \
+     directory. In addition, this command have the option to set a time limit \
+     for each program's execution. When the time limit is exceeded, the \
+     execution is killed.";
+  ]
+
+let man =
+  [
+    `S Manpage.s_description;
+    `P (List.nth description 0);
+    `P (List.nth description 1);
+  ]
+
+let man_xrefs = [ `Page ("wl execute", 2) ]
+
+let cmd_options inputs mode timeout verbose : Cmd_test.options =
+  { inputs; mode; timeout; verbose }
+
+let options =
+  Term.(
+    const cmd_options $ Options.File.inputs $ Options.mode $ Options.timeout
+    $ Options.verbose)
+
+let term = Term.(const Cmd_test.main $ options)

bin/dune

@@ -1,5 +1,7 @@
+(include_subdirs unqualified)
+
 (executable
  (public_name wl)
  (name main)
- (modules main)
- (libraries whilloc))
+ (modules main options dir cmd_execute cmd_test doc_execute doc_test)
+ (libraries whilloc cmdliner bos))