let () =
let exit_code = ref 0 in
try
if Array.length Sys.argv < 2 then
invalid_arg "usage: reorder check|repair|replay|contrast|compare|graph|audit|laws|layout|emit [file] [options]";
let command = Sys.argv.(1) in
let files = ref [] in
let model = ref Syntax.Tso in
let bound = ref None in
let fences = ref [] in
let folder = ref None in
let animate = ref false in
let delay = ref 0.7 in
let width = ref 148 in
let timeout = ref 300000 in
let location text = match String.split_on_char ':' text with
| [t; pc] -> int_of_string t, int_of_string pc
| _ -> invalid_arg "fence locations use thread:instruction" in
let options = [
"--model", Arg.String (fun text -> model := Syntax.model text), "sc or tso";
"--bound", Arg.Int (fun value -> bound := Some value), "maximum scheduler transitions";
"--fence", Arg.String (fun text -> fences := !fences @ [location text]), "thread:instruction";
"--out", Arg.String (fun path -> folder := Some path), "output file or directory";
"--animate", Arg.Set animate, "animate actual execution and solver progress";
"--delay", Arg.Set_float delay, "seconds per displayed transition";
"--width", Arg.Set_int width, "terminal width between 78 and 180 columns";
"--timeout", Arg.Set_int timeout, "solver budget in milliseconds";
] in
let current = ref 1 in
Arg.parse_argv ~current Sys.argv options (fun path -> files := !files @ [path]) "reorder";
if !timeout < 1 || !timeout > 3600000 then invalid_arg "timeout outside 1..3600000 milliseconds";
if not (Float.is_finite !delay) || !delay < 0. || !delay > 10. then
invalid_arg "delay outside 0..10 seconds";
let minimum, maximum = match command with
| "layout" | "laws" -> 0, 0
| "contrast" -> 2, 2
| "graph" -> 1, 2
| "check" | "repair" | "replay" | "compare" | "audit" | "emit" -> 1, 1
| _ -> invalid_arg "unknown command" in
let count = List.length !files in
if count < minimum || count > maximum then
invalid_arg (Printf.sprintf "%s expects %d..%d input files" command minimum maximum);
let file () = match !files with path :: _ -> path | [] -> invalid_arg "missing input file" in
let output fallback = Option.value !folder ~default:fallback in
let load () =
let case = Syntax.load (file ()) in
let case = match !bound with None -> case | Some bound -> {case with Syntax.bound} in
Syntax.validate case;
case in
let with_view case action =
let view = View.create ~width:!width ~delay:!delay ~animate:!animate case in
Fun.protect ~finally:(fun () -> View.finish view) (fun () -> action view) in
let report case result =
Printf.printf "%s\nmodel=%s bound=%d buffer<=8\n" (View.headline case.Syntax.name)
(Syntax.model_name !model) case.bound;
match result.Engine.witness with
| None -> print_endline "UNSAT requested outcome excluded within the bound"
| Some witness ->
Printf.printf "SAT %d transitions; independent replay passed\n"
(Array.fold_left (fun n actor -> if actor = 4 then n else n + 1) 0 witness.actors);
exit_code := 1 in
begin match command with
| "check" ->
let case = load () in
let result = with_view case (fun view ->
Engine.check ~timeout:!timeout ~tick:(fun () -> View.tick view)
~fences:!fences ~folder:(output "build/check") case !model) in
report case result
| "repair" ->
let case = load () in
let result = with_view case (fun view ->
Engine.repair ~timeout:!timeout ~tick:(fun () -> View.tick view)
~notify:(View.notify view) case (output "build/repair")) in
begin match result with
| None -> print_endline "No repair exists at the candidate locations"; exit_code := 1
| Some result ->
Printf.printf "Minimum repair: %d fences; bound %d; %d checked counterexamples\n"
(List.length result.fences) result.bound (List.length result.clauses)
end
| "replay" ->
let witness = Engine.load_witness (file ()) in
with_view witness.case (fun view -> View.play view witness)
| "contrast" ->
let witness_path, repair_path = match !files with
| [left; right] -> left, right | _ -> invalid_arg "contrast needs a witness and a repair" in
let witness = Engine.load_witness witness_path in
let repair = Engine.certify ~timeout:!timeout repair_path in
with_view witness.case (fun view -> View.contrast view witness repair)
| "compare" ->
let case = load () in
with_view case (fun view ->
View.phase view "enumerating sequentially consistent outcomes";
let sc = Engine.outcomes ~timeout:!timeout ~tick:(fun () -> View.tick view) case Syntax.Sc in
View.phase view "enumerating TSO outcomes";
let tso = Engine.outcomes ~timeout:!timeout ~tick:(fun () -> View.tick view) case Syntax.Tso in
View.outcomes view sc tso)
| "graph" ->
let case = load () in
let fences = match !files with
| [_; path] ->
let repair = Engine.certify ~timeout:!timeout path in
if case <> repair.case then invalid_arg "graph and repair cases differ";
repair.fences
| [_] -> !fences
| _ -> invalid_arg "graph expects a case and an optional repair" in
with_view case (fun view -> ignore (View.graph view fences))
| "audit" ->
let repair = Engine.audit ~timeout:!timeout (file ()) (output "build/audit") in
Printf.printf "repair verified at bound %d\n%d witnesses replayed; lower-budget certificate UNSAT\n"
repair.bound (List.length repair.clauses)
| "layout" ->
let path = output "build/layout.smt2" in
Store.write path (Layout.generate ~timeout:!timeout);
print_endline path
| "emit" ->
let case = load () in
let query = Solver.compile ~timeout:!timeout case !model !fences case.bound in
let path = output "build/query.smt2" in
Store.write path (Solver.standalone query);
print_endline path
| "laws" ->
let root = Store.root () in
let text = Layout.generate ~timeout:!timeout ^
Store.read (Filename.concat root "smt/machine.smt2") ^ "\n" ^
Store.read (Filename.concat root "smt/laws.smt2") in
Store.write (output "build/laws.smt2") text;
let responses = Sexp.parse (Solver.script ~timeout:!timeout text) in
if responses <> List.init 16 (fun _ -> Sexp.Atom "unsat") then failwith "machine law check failed";
print_endline "16 SMT machine laws verified"
| _ -> invalid_arg "unknown command"
end;
exit !exit_code
with
| Invalid_argument message | Failure message | Sys_error message ->
Printf.eprintf "reorder: %s\n" message;
exit 2
| Unix.Unix_error (error, operation, _) ->
Printf.eprintf "reorder: %s: %s\n" operation (Unix.error_message error);
exit 2
| Arg.Bad message -> prerr_string message; exit 2
| Arg.Help message -> print_string message