Skip to content

Commit

Permalink
Merge pull request #17 from formalsec/pp_function
Browse files Browse the repository at this point in the history
Make filenames consistent and complete remaining pp functions
  • Loading branch information
julianayang777 authored Mar 11, 2024
2 parents c9da7be + ce48bad commit b3b871a
Show file tree
Hide file tree
Showing 54 changed files with 1,328 additions and 1,324 deletions.
43 changes: 43 additions & 0 deletions .ocamlformat
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
version=0.26.1
assignment-operator=end-line
break-cases=fit
break-fun-decl=wrap
break-fun-sig=wrap
break-infix=wrap
break-infix-before-func=false
break-separators=before
break-sequences=true
cases-exp-indent=2
cases-matching-exp-indent=normal
doc-comments=before
doc-comments-padding=2
doc-comments-tag-only=default
dock-collection-brackets=false
exp-grouping=preserve
field-space=loose
if-then-else=compact
indicate-multiline-delimiters=space
indicate-nested-or-patterns=unsafe-no
infix-precedence=indent
leading-nested-match-parens=false
let-and=sparse
let-binding-spacing=compact
let-module=compact
margin=80
max-indent=2
module-item-spacing=compact
ocaml-version=4.14.0
ocp-indent-compat=false
parens-ite=false
parens-tuple=always
parse-docstrings=true
sequence-blank-line=preserve-one
sequence-style=terminator
single-case=compact
space-around-arrays=true
space-around-lists=true
space-around-records=true
space-around-variants=true
type-decl=sparse
wrap-comments=false
wrap-fun-args=true
158 changes: 84 additions & 74 deletions bin/commands/cmd_execute.ml
Original file line number Diff line number Diff line change
@@ -1,42 +1,53 @@
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)

(* Choice *)
module C_Choice = List_choice.Make (Eval_concrete.M) (Heap_concrete.M)
module SAF_Choice = List_choice.Make (Eval_symbolic.M) (Heap_array_fork.M)
module SAITE_Choice = List_choice.Make (Eval_symbolic.M) (Heap_arrayite.M)
module ST_Choice = List_choice.Make (Eval_symbolic.M) (Heap_tree.M)
module SOPL_Choice = List_choice.Make (Eval_symbolic.M) (Heap_oplist.M)

(* Interpreter *)
module C =
Interpreter.Make (Eval_concrete.M) (Dfs.M) (Heap_concrete.M) (C_Choice)

module SAF =
Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapArrayFork.M) (SAF_Choice)
Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_array_fork.M) (SAF_Choice)

module SAITE =
Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapArrayITE.M) (SAITE_Choice)
Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_arrayite.M) (SAITE_Choice)

module ST = Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapTree.M) (ST_Choice)
module ST = Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_tree.M) (ST_Choice)

module SOPL =
Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapOpList.M) (SOPL_Choice)
Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_oplist.M) (SOPL_Choice)

type mode = Concrete | Saf | Saite | St | Sopl [@@deriving yojson]
type mode =
| Concrete
| Saf
| Saite
| St
| Sopl
[@@deriving yojson]

type report = {
filename : string;
mode : mode;
execution_time : float;
solver_time : float;
num_paths : int;
num_problems : int;
problems : Outcome.t list;
}
type report =
{ filename : string
; mode : mode
; execution_time : float
; solver_time : float
; num_paths : int
; num_problems : int
; problems : Outcome.t list
}
[@@deriving yojson]

type options = {
input : Fpath.t;
mode : mode;
output : Fpath.t option;
verbose : bool;
}
type options =
{ input : Fpath.t
; mode : mode
; output : Fpath.t option
; verbose : bool
}

let mode_to_string = function
| Concrete -> "c"
Expand All @@ -61,50 +72,50 @@ let run input mode =
let problems, num_paths =
match mode with
| Concrete ->
let rets = C.interpret program in
( List.filter_map
(fun (out, _) ->
match out with
| Outcome.Error _ | Outcome.EndGas -> Some out
| _ -> None)
rets,
List.length rets )
let rets = C.interpret program in
( List.filter_map
(fun (out, _) ->
match out with
| Outcome.Error _ | Outcome.EndGas -> Some out
| _ -> None )
rets
, List.length rets )
| Saf ->
let rets = SAF.interpret program in
( List.filter_map
(fun (out, _) ->
match out with
| Outcome.Error _ | Outcome.EndGas -> Some out
| _ -> None)
rets,
List.length rets )
let rets = SAF.interpret program in
( List.filter_map
(fun (out, _) ->
match out with
| Outcome.Error _ | Outcome.EndGas -> Some out
| _ -> None )
rets
, List.length rets )
| Saite ->
let rets = SAITE.interpret program in
( List.filter_map
(fun (out, _) ->
match out with
| Outcome.Error _ | Outcome.EndGas -> Some out
| _ -> None)
rets,
List.length rets )
let rets = SAITE.interpret program in
( List.filter_map
(fun (out, _) ->
match out with
| Outcome.Error _ | Outcome.EndGas -> Some out
| _ -> None )
rets
, List.length rets )
| St ->
let rets = ST.interpret program in
( List.filter_map
(fun (out, _) ->
match out with
| Outcome.Error _ | Outcome.EndGas -> Some out
| _ -> None)
rets,
List.length rets )
let rets = ST.interpret program in
( List.filter_map
(fun (out, _) ->
match out with
| Outcome.Error _ | Outcome.EndGas -> Some out
| _ -> None )
rets
, List.length rets )
| Sopl ->
let rets = SOPL.interpret program in
( List.filter_map
(fun (out, _) ->
match out with
| Outcome.Error _ | Outcome.EndGas -> Some out
| _ -> None)
rets,
List.length rets )
let rets = SOPL.interpret program in
( List.filter_map
(fun (out, _) ->
match out with
| Outcome.Error _ | Outcome.EndGas -> Some out
| _ -> None )
rets
, List.length rets )
in
let execution_time = Sys.time () -. start in
let num_problems = List.length problems in
Expand All @@ -118,14 +129,13 @@ let run input mode =
Total Solver time: %f\n"
execution_time !Translator.solver_time;
write_report
{
execution_time;
mode;
num_paths;
num_problems;
problems;
filename = input;
solver_time = !Translator.solver_time;
{ execution_time
; mode
; num_paths
; num_problems
; problems
; filename = input
; solver_time = !Translator.solver_time
}

let main (opts : options) =
Expand Down
28 changes: 14 additions & 14 deletions bin/commands/cmd_test.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,12 @@ open Whilloc

exception Timeout

type options = {
inputs : Fpath.t;
mode : Cmd_execute.mode;
timeout : float option;
verbose : bool;
}
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
Expand All @@ -17,23 +17,23 @@ let set =
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)
@@ ( 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 with
| Timeout ->
Printf.printf
"Timeout occurred while processing file: %s (Max Timeout: %f \
seconds)\n"
file !_max_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))
Printf.printf "Fatal error: exception %s\n" (Printexc.to_string ex) )
with Timeout -> Printf.printf "General timeout\n"

let run (opts : options) : unit =
Expand Down
22 changes: 10 additions & 12 deletions bin/docs/doc_execute.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,23 +4,21 @@ 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 \
[ "Given a program in the simple \"While\" language, executes the program \
concretely or symbolically depending on the mode. At the end, it \
generates a report named 'report.json' that includes some execution \
metrics and counter models that were found.";
"To run the program concretely, use the mode 'c'.";
"To run the program symbolically, there are several modes to choose from. \
metrics and counter models that were found."
; "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.";
program."
]

let man =
[
`S Manpage.s_description;
`P (List.nth description 0);
`P (List.nth description 1);
`P (List.nth description 2);
[ `S Manpage.s_description
; `P (List.nth description 0)
; `P (List.nth description 1)
; `P (List.nth description 2)
]

let man_xrefs = []
Expand All @@ -31,6 +29,6 @@ let cmd_options input mode output verbose : Cmd_execute.options =
let options =
Term.(
const cmd_options $ Options.File.input $ Options.mode $ Options.File.output
$ Options.verbose)
$ Options.verbose )

let term = Term.(const Cmd_execute.main $ options)
18 changes: 8 additions & 10 deletions bin/docs/doc_test.ml
Original file line number Diff line number Diff line change
Expand Up @@ -7,21 +7,19 @@ let doc =
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 \
[ "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.";
execution is killed."
]

let man =
[
`S Manpage.s_description;
`P (List.nth description 0);
`P (List.nth description 1);
[ `S Manpage.s_description
; `P (List.nth description 0)
; `P (List.nth description 1)
]

let man_xrefs = [ `Page ("wl execute", 2) ]
Expand All @@ -32,6 +30,6 @@ let cmd_options inputs mode timeout verbose : Cmd_test.options =
let options =
Term.(
const cmd_options $ Options.File.inputs $ Options.mode $ Options.timeout
$ Options.verbose)
$ Options.verbose )

let term = Term.(const Cmd_test.main $ options)
Loading

0 comments on commit b3b871a

Please sign in to comment.