let checks = ref 0
let visited = ref 0

let require condition message =
  if not condition then failwith message;
  incr checks

let rejects action message =
  let failed = try action (); false with Invalid_argument _ | Failure _ -> true in
  require failed message

let read name = Syntax.load ("cases/" ^ name ^ ".sexp")

let storage folder =
  let folder = Filename.concat folder "storage" in
  let path = Filename.concat folder "nested/artefact" in
  Store.write path "first";
  let previous = open_in_bin path in
  Fun.protect ~finally:(fun () -> close_in_noerr previous) (fun () ->
    Store.write path "replacement";
    require (Store.read path = "replacement") "artefact replacement";
    require (really_input_string previous 5 = "first") "open reader retains previous artefact");
  let target = Filename.concat folder "directory" in
  Store.mkdir target;
  let failed = try Store.write target "invalid"; false with Sys_error _ -> true in
  require failed "directory cannot be replaced by an artefact";
  require (Sys.is_directory target) "failed replacement preserves destination";
  require (List.sort compare (Array.to_list (Sys.readdir folder)) = ["directory"; "nested"])
    "failed replacement removes temporary file"

let transport folder =
  let previous = Option.value (Sys.getenv_opt "Z3") ~default:"z3" in
  let descriptors () = Array.length (Sys.readdir "/proc/self/fd") in
  let before = descriptors () in
  Fun.protect ~finally:(fun () -> Unix.putenv "Z3" previous) (fun () ->
    Unix.putenv "Z3" (Filename.concat folder "missing");
    for _ = 1 to 32 do
      let failed = try ignore (Solver.script ""); false with
        | Unix.Unix_error (Unix.ENOENT, _, _) -> true in
      require failed "missing solver reports process creation failure"
    done);
  require (descriptors () = before) "failed solver spawn closes every pipe"

let laws () =
  let source = Layout.generate ~timeout:300000 ^ Store.read "smt/machine.smt2" ^
    "\n" ^ Store.read "smt/laws.smt2" in
  let answers = Sexp.parse (Solver.script source) in
  require (answers = List.init 16 (fun _ -> Sexp.Atom "unsat")) "SMT machine laws";
  print_endline "16 SMT machine laws passed"

let codec () =
  List.iter (fun text ->
    let value = Sexp.Atom text in
    require (Sexp.one (Sexp.print value) = value) "string round trip")
    [""; "hello"; "with spaces"; "a\"b\\c"; "a\nb\tc"; "lambda \206\187"];
  List.iter (fun text -> rejects (fun () -> ignore (Sexp.one text)) "malformed expression")
    ["("; ")"; "(a"; "\"unfinished"; "a b"; "\"\\z\""];
  require (Sexp.word (Sexp.Atom "#xffffffffffffffff") = -1L) "unsigned 64-bit model value";
  List.iter (fun name ->
    let case = read name in
    require (Syntax.decode (Syntax.encode case) = case) "case round trip")
    ["buffering"; "forwarding"; "fifo"; "fenced"; "peterson"; "spinlock"]

let fixtures () =
  List.iter (fun (name, expected) ->
    let case = read name in
    let result = Engine.check case Syntax.Tso in
    let reachable, count = Machine.reachable case Syntax.Tso [] case.bound in
    visited := !visited + count;
    require ((result.witness <> None) = expected && reachable = expected) ("fixture " ^ name);
    Option.iter (fun witness ->
      let states, _ = Engine.replay witness in
      require (Machine.bad case states.(witness.bound)) "witness final state";
      require (List.length (View.frame ~width:148 witness witness.bound) < 52) "trace display height") result.witness;
    Printf.printf "%-12s %-5s %5d reference states\n%!" name
      (if result.witness = None then "unsat" else "sat") count)
    ["buffering", true; "forwarding", false; "fifo", false;
     "fenced", false; "peterson", true; "spinlock", false]

let differential () =
  let random = Random.State.make [|731|] in
  let choose n = Random.State.int random n in
  let instruction () = match choose 5 with
    | 0 -> Syntax.Store (choose 2, Int64.of_int (choose 3))
    | 1 -> Syntax.Load (choose 2, choose 2)
    | 2 -> Syntax.Move (choose 2, Int64.of_int (choose 3))
    | 3 -> Syntax.Fence
    | _ -> Syntax.Exchange (choose 2, choose 2, 1L) in
  for number = 0 to 17 do
    let case = {
      Syntax.name=Printf.sprintf "generated%d" number; names=[|"x"; "y"|]; bound=6;
      threads=Array.init 2 (fun _ -> Array.init 2 (fun _ -> instruction ()));
      candidates=[]; goal=Syntax.Outcome {
        registers=[0, 0, Int64.of_int (choose 2); 1, 0, Int64.of_int (choose 2)];
        memory=[]; drained=false};
    } in
    List.iter (fun model ->
      let expected, count = Machine.reachable case model [] case.bound in
      visited := !visited + count;
      let result = Engine.check case model in
      require ((result.witness <> None) = expected) "seeded differential query") [Syntax.Sc; Syntax.Tso]
  done;
  print_endline "36 seeded SMT queries matched exhaustive reference execution"

let buffers () =
  let stores = Array.init 10 (fun value -> Syntax.Store (0, Int64.of_int value)) in
  let case = {Syntax.name="ring wrap"; names=[|"x"|]; bound=22;
    threads=[|Array.append stores [|Syntax.Load (0, 0)|]; [|Syntax.Move (0, -1L)|]|];
    candidates=[]; goal=Syntax.Outcome {registers=[0, 0, 9L; 1, 0, -1L]; memory=[]; drained=false}} in
  List.iter (fun drained ->
    let actors = Array.of_list (List.concat (List.init drained (fun _ -> [0; 2])) @
      List.init (11 - drained) (fun _ -> 0) @ [1]) in
    let result = Engine.check ~bound:(Array.length actors) ~fixed:actors case Syntax.Tso in
    require (result.witness <> None) "ring reuse and last buffered write") [9; 10];
  let initial = Machine.initial case in
  let state = ref initial in
  for _ = 0 to 7 do
    match Machine.step case Syntax.Tso [] !state 0 with
    | Some (next, _) -> state := next | None -> failwith "unexpected full buffer"
  done;
  require (Machine.step case Syntax.Tso [] !state 0 = None) "full FIFO blocks ninth store";
  require (initial.pc = [|0; 0|] && initial.buffers = [|[]; []|]) "transition preserves previous state";
  require (Machine.step case Syntax.Tso [] initial 2 = None) "empty FIFO cannot drain"

let outcomes () =
  let case = read "buffering" in
  let sc = Engine.outcomes case Syntax.Sc in
  let tso = Engine.outcomes case Syntax.Tso in
  require (sc = [0L, 1L; 1L, 0L; 1L, 1L]) "SC outcome enumeration";
  require (tso = [0L, 0L; 0L, 1L; 1L, 0L; 1L, 1L]) "TSO outcome enumeration";
  print_endline "complete register outcome sets: SC=3, TSO=4"

let graph () =
  let case = read "peterson" in
  let graph = Machine.explore case Syntax.Tso [] in
  require (List.length graph.violations > 0) "unfenced graph exposes overlap";
  let seen = Hashtbl.create (Array.length graph.states) in
  Array.iter (fun state -> Hashtbl.add seen state ()) graph.states;
  let edges = ref 0 in
  Array.iter (fun state ->
    for actor = 0 to 3 do
      match Machine.step case Syntax.Tso [] state actor with
      | None -> ()
      | Some (next, _) -> incr edges; require (Hashtbl.mem seen next) "closed graph successor"
    done) graph.states;
  require (!edges = graph.edges) "graph edge count";
  rejects (fun () -> ignore (Machine.explore ~limit:10 case Syntax.Tso [])) "exploration limit is explicit";
  Printf.printf "unfenced graph closed: %d states, %d edges, %d violating states\n%!"
    (Array.length graph.states) graph.edges (List.length graph.violations)

let constraints () =
  List.iter (fun (count, clauses) ->
    rejects (fun () -> ignore (Solver.candidate ~count ~budget:1 clauses))
      "invalid fence constraint")
    [-1, []; 1, [[-1]]; 1, [[1]]; 0, [[0]]];
  let solve count budget clauses = Solver.solve (Solver.candidate ~count ~budget clauses) in
  require (solve 0 0 [] = Solver.Sat []) "empty candidate set satisfies zero budget";
  require (solve 0 (-1) [] = Solver.Unsat) "negative lower budget remains unsatisfiable";
  require (solve 2 0 [[0; 1]] = Solver.Unsat) "zero budget cannot hit a nonempty clause";
  require (solve 2 1 [[0]; [1]] = Solver.Unsat) "independent singleton clauses require two fences";
  require (solve 2 2 [[0]; [1]] = Solver.Sat [Solver.Truth true; Solver.Truth true])
    "candidate values follow clause indices"

let validation () =
  let case = read "buffering" in
  let open Sexp in
  let entries = List.tl (list (Syntax.encode case)) in
  let decode entries = ignore (Syntax.decode (List (Atom "case" :: entries))) in
  List.iter (fun extra ->
    rejects (fun () -> decode (extra :: entries)) "unexpected case field")
    [List [Atom "bounds"; i 8]; Atom "extra"; List []; List [List []]];
  List.iter (fun extra ->
    let entries = List.map (function
      | List [Atom "goal"; List (Atom "outcome" :: goal)] ->
          List [Atom "goal"; List (Atom "outcome" :: extra :: goal)]
      | field -> field) entries in
    rejects (fun () -> decode entries) "unexpected outcome field")
    [List [Atom "drain"; Atom "true"]; Atom "extra"; List []];
  List.iter (fun case -> rejects (fun () -> Syntax.validate case) "invalid case") [
    {case with bound=0}; {case with bound=65}; {case with names=[||]};
    {case with threads=[||]}; {case with candidates=[0, 9]};
    {case with candidates=[0, 1; 0, 1]};
    {case with threads=[|[|Syntax.Load (0, 4)|]; case.threads.(1)|]};
    {case with threads=[|[|Syntax.Branch (0, 0L, 3)|]; case.threads.(1)|]}];
  rejects (fun () -> ignore (Engine.check ~fixed:[|0|] case Syntax.Tso)) "fixed schedule bound mismatch"

let cli folder =
  let descriptor = Unix.openfile "/dev/null" [Unix.O_RDWR; Unix.O_CLOEXEC] 0 in
  Fun.protect ~finally:(fun () -> Unix.close descriptor) (fun () ->
    let run arguments =
      let arguments = Array.of_list ("./src/main.exe" :: arguments) in
      let pid = Unix.create_process "./src/main.exe" arguments descriptor descriptor descriptor in
      snd (Unix.waitpid [] pid) in
    List.iter (fun arguments ->
      require (run arguments = Unix.WEXITED 2) "CLI rejects invalid input count")
      [["layout"; "extra"]; ["laws"; "extra"];
       ["check"; "cases/buffering.sexp"; "extra"];
       ["graph"; "cases/buffering.sexp"; "a"; "b"];
       ["replay"]; ["contrast"; "one"]];
    List.iter (fun delay ->
      require (run ["layout"; "--delay"; delay] = Unix.WEXITED 2)
        "CLI rejects invalid delay") ["nan"; "infinity"; "-infinity"; "-0.1"; "10.1"];
    let path = Filename.concat folder "layout.smt2" in
    require (run ["layout"; "--delay"; "0"; "--out"; path] = Unix.WEXITED 0)
      "CLI accepts zero delay";
    require (String.starts_with ~prefix:"(set-logic QF_BV)" (Store.read path))
      "CLI writes the requested layout");
  let case = read "buffering" in
  List.iter (fun delay ->
    rejects (fun () -> ignore (View.create ~animate:false ~delay case))
      "view rejects nonfinite delay") [Float.nan; Float.infinity; Float.neg_infinity]

let repair folder =
  let case = read "peterson" in
  let report = match Engine.repair case folder with
    | Some report -> report | None -> failwith "expected repair" in
  require (List.length report.fences = 2) "minimum repair has two fences";
  let checked = Engine.audit (Filename.concat folder "repair.sexp") (Filename.concat folder "audit") in
  require (report = checked) "repair certificate audit";
  List.iter (fun fences ->
    let found, _ = Machine.reachable case Syntax.Tso fences case.bound in
    require found "every cheaper fence placement still fails") ([] :: List.map (fun location -> [location]) case.candidates);
  let graph = Machine.explore case Syntax.Tso report.fences in
  require (graph.violations = []) "repaired complete state graph excludes overlap";
  let witness = Engine.load_witness (Filename.concat folder "witness.sexp") in
  let fixed = Machine.reschedule case report.fences witness.actors in
  Engine.validate_schedule case report.fences fixed;
  let states, _ = Machine.replay case Syntax.Tso report.fences fixed in
  require (not (Machine.bad case states.(Array.length states - 1))) "repaired requested schedule avoids overlap";
  rejects (fun () -> ignore (Engine.replay {witness with actors=[|2|]})) "tampered witness rejected";
  let unrepairable = {(read "buffering") with candidates=[]} in
  require (Engine.repair unrepairable (Filename.concat folder "impossible") = None) "unrepairable case terminates";
  Printf.printf "minimum repair checked: 2 fences; repaired graph closed with %d states and no overlap\n%!"
    (Array.length graph.states)

let () =
  let started = Unix.gettimeofday () in
  let folder = Filename.concat (Filename.get_temp_dir_name ()) (Printf.sprintf "reorder%d" (Unix.getpid ())) in
  Store.mkdir folder;
  storage folder;
  transport folder;
  codec ();
  laws ();
  fixtures ();
  differential ();
  buffers ();
  outcomes ();
  graph ();
  constraints ();
  validation ();
  cli folder;
  repair folder;
  Printf.printf "%d checks passed; %d bounded reference states; %.1fs\n%!"
    !checks !visited (Unix.gettimeofday () -. started)