Source file Engine.ml

(******************************************************************************)
(*                                                                            *)
(*                                  Monolith                                  *)
(*                                                                            *)
(*                              François Pottier                              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU Lesser General Public License as published by the Free   *)
(*  Software Foundation, either version 3 of the License, or (at your         *)
(*  option) any later version, as described in the file LICENSE.              *)
(*                                                                            *)
(******************************************************************************)

open Printf
open Misc
open Error
open Eq
open Spec
open Env
open Ops

type document =
  PPrint.document

(* -------------------------------------------------------------------------- *)

(* This defines a function [log] which can be used for debugging. *)

include Debug.Make(struct let debug = false end)

(* -------------------------------------------------------------------------- *)

(* Turn on the recording of backtraces, so an uncaught exception causes a
   backtrace to be printed before the process is aborted. *)

let () =
  Printexc.record_backtrace true

(* -------------------------------------------------------------------------- *)

(* DSL syntax. *)

(* It is worth noting that we do not need an *interpreter* for this syntax;
   we only need a *printer*. Indeed, the engine generates a program and
   executes it on the fly. Since generation and execution are not separate,
   there is no need for communication between them. Instead, the syntax is
   used by the engine as a way of recording its actions. Thus, when a fault
   is discovered, a scenario can be printed. *)

(* An argument of an operation is one of the following: *)

type arg =

  (* A constant (of an arbitrary and unknown type). *)
  | ArgConstant of document

  (* A variable (of abstract type). *)
  | ArgVar of var

  (* A unit argument. *)
  | ArgUnit

  (* A pair of arguments. *)
  | ArgPair of arg * arg

  (* An argument of type [option]. *)
  | ArgOption of arg option

  (* An argument of type [result]. *)
  | ArgResult of (arg, arg) result

  (* An argument of type [either]. *)
  | ArgEither of (arg, arg) Either.t

  (* An argument of type [list]. *)
  | ArgList of arg list

  (* An application of a constant to an argument. *)
  | ArgAppConstant of document * arg

(* An operation is used inside an expression. An expression is one of the
   following. (Note the linear structure of this type, as opposed to a
   tree-like structure which would be more standard.) *)

type expr =

  (* At the heart of an expression lies an operation that we wish to use. *)
  | EOp of string

  (* An application of an expression to an argument. *)
  | EAppL of expr * arg

  (* An application of some constant to an expression. *)
  (* At the time of writing, this constant must originate in a use of the
     combinator [map_into]. *)
  (* This constant is represented as a function of type [document list ->
     document]. Thus, an application of this constant to a sufficient number
     of arguments can possibly be beta-reduced on the fly and printed in
     a simpler way. *)
  | EAppR of (document list -> document) * expr

(* An OCaml assertion is represented as a piece of text. *)

type assertion =
  document

(* A pattern indicates what to do with the result of an operation. We construct
   a pattern only after the two implementations (candidate and reference) have
   run. We use this pattern to explain the disagreement when there is one and
   to deconstruct the result value when there is agreement. *)

type pat =
  | PatWildcard
      (* [PatWildcard] can be used at an arbitrary type. *)
  | PatBind of var
      (* [PatBind] can be used only at an abstract base type. It indicates
         that a variable should be bound to this value, so that this value
         can be used in future instructions. *)
  | PatRawVar of string
      (* [PatRawVar] represents a temporary variable. This variable is not
         known to the engine: it does not appear in the environment. Temporary
         variables are introduced by the function [break_instruction]. *)
  | PatObserveAgreement
      (* [PatObserveAgreement] is printed like a wildcard pattern. It is
         used only at a concrete base type. It indicates that both sides
         agree on this value. *)
  | PatObserveDisagreement of assertion
      (* [PatObserveDisagreement] is used only at a concrete base type.
         It indicates that there is a disagreement, and carries a string
         representation of an OCaml instruction that explains the problem.
         An example is "assert (observed = 0);; (* candidate finds 1 *)".
         This pattern plays the double role of binding the observation
         variable [ovar] and of carrying this OCaml instruction, which
         refers to the variable [ovar]. *)
  | PatUnit
      (* [PatUnit] is used at the [unit] type. *)
  | PatPair of pat * pat
      (* [PatPair] is used at a pair type. *)
  | PatOption of pat option
      (* [PatOption is used at an option type. *)
  | PatResult of (pat, pat) result
      (* [PatResult] is used at a result type. *)
  | PatEither of (pat, pat) Either.t
      (* [PatResult] is used at type [Either.t]. *)
  | PatNil
  | PatCons of pat
      (* [PatNil] and [PatCons] are used at a list type. [PatCons] carries
         a single pattern, which matches a pair. *)
  | PatAppR of (document list -> document) * pat
      (* [PatAppR] is analogous to [EAppR]; it represents an application of a
         constant to a pattern. This constant is typically a function provided
         by the user via [map_into]. *)
      (* The pattern form [f pat], where [f] is a function and [pat] is a
         pattern, does not exist in OCaml, but exists in other languages, and
         has well-defined meaning: deconstructing a value [v] via the pattern
         [f pat] amounts to deconstructing the value [f v] via the pattern
         [pat]. *)
      (* The fact that this pattern form does not exist in OCaml poses a
         problem when one wishes to print this pattern. Our solution is to
         decompose a single binding [let pat = expr] into a sequence of such
         bindings, connected by temporary variables. The function
         [break_instruction] performs this task. *)

(* An instruction takes (roughly) the following form:

      let pat = expr;;
      assert (observed = ...);;

   The expression [expr] is always a use of an operation [op] within a certain
   context (e.g., an application of this operation to a list of arguments).

   The line [assert (observed = ...);;] is an (optional) observation. If it
   is present, then [observed] is an observation variable bound by [pat], and
   [pat] binds no other variables. This assertion compares an observed result
   with an expected result. It is present only if a mismatch has been
   detected. *)

type instruction =
  | I of pat * expr

(* When an exception is caught and turned into a piece of data, the backtrace
   must be recorded now, as it could otherwise be clobbered by raising another
   exception. *)

type frozen_exn =
  { e: exn; backtrace: string }

let freeze e =
  let backtrace = Printexc.get_backtrace() in
  { e; backtrace }

(* A [failure] records what kind of failure occurred. *)

type failure =

  (* The reference implementation raised an exception. *)
  | ReferenceFailure of frozen_exn

  (* The candidate implementation raised an exception. *)
  | CandidateFailure of frozen_exn

  (* A wrapper inserted by [map_into] or [map_outof] raised an exception. *)
  | ReferenceWrapperFailure of frozen_exn
  | CandidateWrapperFailure of frozen_exn

  (* The candidate produced an incorrect observable result. *)
  | ObservationFailure

  (* A well-formedness check raised an exception. *)
  | CheckFailure of (* x: *) var * frozen_exn

(* -------------------------------------------------------------------------- *)

(* Environments. *)

(* We maintain an environment that maps each variable to a value, that is, a
   triple of a relational specification, a reference value, and a candidate
   value. *)

(* We maintain the invariant that every value in the environment has an
   abstract base type. Thus, every spec in the environment is of the form
   [SpecBaseAbstract _]. Indeed, a value of a concrete type is observed as
   soon as it is produced, and does not need to be bound to a variable.
   A value of a structural type (product, sum, etc.) is deconstructed as
   soon as it is produced. *)

type env =
  value Env.env

(* -------------------------------------------------------------------------- *)

(* Exceptions. *)

(** The exception [PleaseBackOff] can be raised by the reference
    implementation to indicate that this operation (or this particular choice
    of arguments for this operation) should not be exercised. The reason could
    be that it is not permitted, or that this has not been implemented yet.
    This exception causes Monolith to back off and try something else. For this
    reason, the reference implementation must not perform any side effect
    before raising this exception. *)
exception PleaseBackOff

(** The exception [Unimplemented] can be raised by the candidate
    implementation to indicate that this operation (or this particular choice
    of arguments for this operation) should not be exercised. This exception
    causes Monolith to abandon the current scenario and investigate other
    scenarios. *)
exception Unimplemented

(* -------------------------------------------------------------------------- *)

(* [break_instruction i] breaks the instruction [i] down into a sequence of
   instructions whose patterns do not contain the constructor [PAppR]. These
   instructions are connected via temporary variables whose names do not
   matter outside of this sequence of instructions (as long as they do not
   hide existing names). *)

let break_instruction (i : instruction) : instruction list =

  (* A queue of instructions, waiting to be broken down. *)
  let waiting = Queue.create() in

  (* A generator of fresh names for temporary variables. *)
  let c = ref 0 in
  let gensym () = let x = !c in c := x + 1; x in

  (* Breaking down a pattern removes [PatAppR] constructors and enqueues more
     instructions into the waiting queue. *)
  let rec break_pat pat =
    match pat with
    | PatWildcard
    | PatBind _
    | PatObserveAgreement
    | PatObserveDisagreement _
    | PatUnit
    | PatNil
    | PatOption None
    | PatRawVar _
        -> pat
    | PatPair (pat1, pat2) ->
        PatPair (break_pat pat1, break_pat pat2)
    | PatOption (Some pat) ->
        PatOption (Some (break_pat pat))
    | PatResult (Ok pat) ->
        PatResult (Ok (break_pat pat))
    | PatResult (Error pat) ->
        PatResult (Error (break_pat pat))
    | PatEither (Either.Left pat) ->
        PatEither (Either.Left (break_pat pat))
    | PatEither (Either.Right pat) ->
        PatEither (Either.Right (break_pat pat))
    | PatCons pat ->
        PatCons (break_pat pat)
    | PatAppR (constant, pat) ->
        (* Generate a fresh temporary variable [x], which serves to name the
           value that we are currently looking at. *)
        let x = sprintf "_t%d" (gensym()) in
        (* Enqueue an instruction which deconstructs the function application
           [constant x] using the pattern [pat]. *)
        (* We abuse the constructor [EOp x] to print the raw variable [x]. *)
        let i = I (pat, EAppR (constant, EOp x)) in
        Queue.add i waiting;
        (* Done. *)
        PatRawVar x
  in

  (* Begin with the instruction [i] and continue until finished. *)
  Queue.add i waiting;
  let output = ref [] in
  while not (Queue.is_empty waiting) do
    let I (pat, expr) = Queue.take waiting in
    output := I (break_pat pat, expr) :: !output
  done;
  List.rev !output

(* -------------------------------------------------------------------------- *)

(* Printing instructions. *)

include struct

  open Print

  (* [print_var env x] prints the variable [x], which must be bound in [env]. *)

  let print_var env x =
    (* Use a type-specific prefix, followed with the numeric level. *)
    (* We do not need distinct types to be associated with distinct
       prefixes; the presence of the numeric level alone ensures that
       we produce distinct names for distinct variables. *)
    match Env.lookup env x with
    | Value (SpecBaseAbstract (_, properties), _, _) ->
        (* Extract the base name associated with this abstract base type. *)
        let base = properties.aty_var in
        utf8format "%s%d" base (level x)
    | Value _ ->
        assert false (* every variable has abstract type *)

  (* [ovar] is the name of the single observation variable that is needed
     when we wish to name an observed value and indicate that it does not
     meet our expectation. *)

  let ovar =
    utf8format "observed"

  (* [print_arg env a] prints the argument [a], whose free variables must
     be bound in [env]. The resulting string is parenthesized. *)

  let rec print_arg env arg =
    match arg with
    | ArgConstant constant ->
        constant
    | ArgVar x ->
        print_var env x
    | ArgUnit ->
        unit
    | ArgPair (arg1, arg2) ->
        OCaml.tuple [ print_arg env arg1; print_arg env arg2 ]
    | ArgOption oarg ->
        option (print_arg env) oarg
    | ArgResult rarg ->
        result (print_arg env) (print_arg env) rarg
    | ArgEither rarg ->
        either (print_arg env) (print_arg env) rarg
    | ArgList args ->
        list (print_arg env) args
    | ArgAppConstant (constant, arg) ->
        parens (apply constant [ print_arg env arg ])

  (* [print_expr env expr] prints the expression [expr]. The result string
     is not parenthesized. *)

  (* [print_expr] uses an auxiliary function [print_app], which descends into
     the left-hand side of applications and accumulates a list of actual
     arguments. This allows us to print an n-ary application in one swoop, and
     possibly to simplify it on the fly. *)

  let rec print_expr env expr =
    print_app env expr []

  and print_app env expr (actuals : document list) =
    match expr with

    | EOp op ->
        (* We have reached the head of this n-ary application. *)
        apply
          (!^ op)
          actuals

    | EAppL (expr, arg) ->
        (* Descend into the left-hand side, accumulating one more actual
           argument. No parentheses are needed because [print_arg] prints
           a parenthesized string already. *)
        print_app env expr (print_arg env arg :: actuals)

    | EAppR (constant, expr) ->
        (* Descend into the left-hand side and immediately remark that we have
           reached the head of this n-ary application. Parentheses are needed
           because [print_expr] does not produce a parenthesized string. *)
        (* Here, [constant] is a function that expects a list of documents. *)
        constant
          (parens (print_expr env expr) :: actuals)

  (* [print_pat env pat] prints the pattern [pat], whose variables must
     be bound in [env]. The resulting string is parenthesized. *)

  let cons =
    !^ " ::" ^^ break 1

  let rec print_pat env pat =
    match pat with
    | PatWildcard ->
        underscore
    | PatBind x ->
        print_var env x
    | PatRawVar x ->
        utf8string x
    | PatObserveAgreement ->
        underscore
    | PatObserveDisagreement _ ->
        ovar
    | PatUnit ->
        unit
    | PatPair (pat1, pat2) ->
        OCaml.tuple [ print_pat env pat1; print_pat env pat2 ]
    | PatOption opat ->
        option (print_pat env) opat
    | PatResult rpat ->
        result (print_pat env) (print_pat env) rpat
    | PatEither rpat ->
        either (print_pat env) (print_pat env) rpat
    | PatNil
    | PatCons _ ->
        print_pat_list env [] pat
    | PatAppR _ ->
        (* Assuming that this pattern has been preprocessed using [break_pat],
           this case cannot arise. *)
        assert false

  and print_pat_list env accu pat =
    match pat with
    | PatCons (PatPair (pat1, pat2)) ->
        print_pat_list env (pat1 :: accu) pat2
    | PatCons _ ->
        assert false
    | PatNil ->
        (* We have a closed list pattern. We can use list syntax. *)
        let pats = List.rev accu in
        list (print_pat env) pats
    | _ ->
        assert (pat = PatWildcard);
        (* We have an unclosed list pattern. We must use cons syntax. *)
        let pats = List.rev (pat :: accu) in
        group (lparen ^^ nest 2 (
          flow_map cons (print_pat env) pats
        ) ^^ rparen)

  (* [observations pat] extracts the observations (that is, the assertions)
     that appear in the pattern [pat]. *)

  (* In principle, a pattern contains at most one subpattern of the form
     [PatObserveDisagreement _]. This implies that [observations pat] returns
     a list of length at most one. *)

  let rec observations pat : assertion list =
    match pat with
    | PatWildcard
    | PatBind _
    | PatRawVar _
    | PatObserveAgreement
    | PatUnit
    | PatOption None
    | PatNil
        -> []
    | PatObserveDisagreement assertion ->
        [assertion]
    | PatPair (pat1, pat2) ->
        observations pat1 @
        observations pat2
    | PatOption (Some pat)
    | PatResult (Ok pat)
    | PatResult (Error pat)
    | PatEither (Either.Left pat)
    | PatEither (Either.Right pat)
    | PatCons pat
    | PatAppR (_, pat)
        -> observations pat

  let observations (i : instruction) : assertion list =
    let I (pat, _) = i in
    let os = observations pat in
    assert (List.length os <= 1);
    os

  (* [print_simple_instruction env i] prints the instruction [i] as a
     toplevel binding of the form [let pat = expr]. The pattern [pat]
     must not contain any [PAppR] constructor. *)

  let print_simple_instruction env (I (pat, expr)) =
    toplevel_let (print_pat env pat) (print_expr env expr)

  (* [print_instruction env i] prints the instruction [i]. *)

  let print_instruction env i =
    separate hardline (
      (* We expect that the environment [env] has already been extended with
         the variables bound by the pattern [pat]. *)
      (* Because a pattern that contains a [PAppR] constructor cannot be
         printed, we break the instruction [i] into a sequence of instructions
         that do not use this constructor, and print this sequence. *)
      List.map (print_simple_instruction env) (break_instruction i) @
      (* Print the observations that are implicit in the instruction [i]. *)
      observations i
    )

  (* [print_instructions env pc failure is] prints the instruction sequence
     [is]. [pc] is the instruction counter. [failure] indicates the cause of
     the failure that was observed. *)

  let rec print_instructions env pc failure is =
    match is with
    | [] ->
        empty
    | i :: is ->
        (* Print the instruction counter. *)
        utf8format "(* @%02d *) " pc ^^ align (
          (* Print the instruction [i]. *)
          print_instruction env i ^^
          (* If this is the last instruction and if the parameter [failure]
             shows that a well-formedness check caused a failure, print this
             check. Otherwise, continue. *)
          match is, failure with
          | [], CheckFailure (x, _) ->
              begin match Env.lookup env x with
                | Value (SpecBaseAbstract (_, properties), rv, _) ->
                    let check = properties.aty_check rv in
                    hardline ^^
                    Code.print check [ print_var env x ]
                    ^^ utf8format ";; (* this check fails! *)"
                | _ ->
                    assert false (* every variable has abstract type *)
              end
          | _, _ ->
              empty
        ) ^^
        hardline ^^
        let pc = pc + 1 in
        print_instructions env pc failure is

  (* [failure_type failure] is a one-line summary of the failure. *)

  let failure_type failure =
    match failure with
    | ReferenceFailure _ ->
        "Failure in the reference implementation"
    | CandidateFailure _ ->
        "Failure in an instruction"
    | CandidateWrapperFailure _ ->
        sprintf "Failure in a wrapper on the candidate side"
    | ReferenceWrapperFailure _ ->
        sprintf "Failure in a wrapper on the reference side"
    | ObservationFailure ->
        "Failure in an observation: candidate and reference disagree"
    | CheckFailure _ ->
        "Failure in a well-formedness check"

  (* [print_failure_exception failure] returns a string that describes
     the exception associated with the failure, if there is one. *)

  let print_failure_exception pc failure : string =
    match failure with
    | ObservationFailure ->
        (* If the problem is an observation failure, no exception was raised. *)
        ""
    | ReferenceFailure e
    | CandidateFailure e
    | ReferenceWrapperFailure e
    | CandidateWrapperFailure e
    | CheckFailure (_, e) ->
        (* If an exception was raised, print a full backtrace. *)
        sprintf "(* @%02d: The exception %s was raised. *)\n\n%s"
          pc
          (Printexc.to_string e.e)
          e.backtrace

  (* [print_failure env past failure] returns a failure message. (This is done
     immediately before aborting.) [past] is the list of past instructions.
     [failure] is the cause of the failure. *)

  let print_failure env past failure : string =
    let b = Buffer.create 1024 in
    let is = List.rev past in
    let pc = List.length is in
    bprintf b "(* @%02d: %s. *)\n" pc (failure_type failure);
    DelayedOutput.dump b;
    output b (print_instructions env 1 failure is);
    Buffer.add_string b (print_failure_exception pc failure);
    Buffer.contents b

  (* [print_equality_assertion equal rv cv] produces an equality assertion
     that explains why the candidate value [cv] is incorrect. It is an
     equality between the variable [ovar] (which denotes a candidate value)
     and the reference value [rv]. A comment is also printed, in which the
     incorrect candidate value appears. *)

  let print_equality_assertion equal rv cv =
    assert_ (Code.print equal [ ovar; rv ])
    ^^ !^ ";;"
    ^^ candidate_finds cv

end

(* -------------------------------------------------------------------------- *)

(* This exception is used to abort a run. It is handled in different ways
   when running under AFL and when running in purely random mode. *)

(* Its integer argument is the fuel that was necessary to discover a bug. *)

(* Its string argument is the scenario. *)

exception Abort of string * int

let raise_abort env past failure =
  let scenario = print_failure env past failure
  and fuel = List.length past in
  raise (Abort (scenario, fuel))

(* -------------------------------------------------------------------------- *)

(* Constructing an argument for an operation. *)

(* The [true] precondition. *)

let no_requirement _ = true

(* [construct_arg env spec p] constructs an argument that has type [spec] and
   satisfies the precondition [p]. It returns an argument as well as the
   result of evaluating this argument, a pair of a reference value [rv] and a
   candidate value [cv]. [spec] must be constructible. *)

(* [construct_arg] fails if a wrapper raises an exception: see [SpecMapOutof].
   This is an abnormal situation, a fatal error, most likely a programming
   error in the wrapper. We deal with it by wrapping this exception in a
   [ConstructArg] exception. An earlier version of the code used a [result]
   return type, but that was too painful. *)

(* [construct_arg] can also raise [Gen.Reject], causing the generator to
   backtrack and try some other instruction. *)

exception ConstructArg of arg * failure

let rec construct_arg
: type r c . env -> (r, c) spec -> (r -> bool) -> arg * r * c
= fun env spec p ->
  match spec with

  | SpecBaseAbstract (tag, _) ->
      (* Pick a variable in the environment that has the desired type
         and that satisfies the predicate [p]. *)
      Env.choose env (fun x (Value (spec', rv, cv)) ->
        match spec' with
        | SpecBaseAbstract (tag', _) ->
            begin match Tag.equal tag tag' with
            | Eq ->
                (* The success of the tag equality test allows the
                   following two type casts. *)
                let rv : r = rv
                and cv : c = cv in
                if p rv then Some (ArgVar x, rv, cv) else None
            | exception Tag.RuntimeTagError ->
                None
            end
        | _ ->
            assert false (* every variable has abstract type *)
      )

  | SpecSubset (spec, q) ->
      (* This argument must satisfy the precondition [q]. Compute the
         conjunction of our argument [p] with [q], and go down. We do
         not adopt the naive solution of 1- making a recursive call to
         construct a value, and 2- checking a posteriori that this value
         satisfies [q]. Indeed, in the case where there is an abstract
         type below, we can do better -- we can test which values in
         the environment satisfy [q], and select a value from them.
         This eliminates the risk of choosing a value that does not
         satisfy [q]. *)
      construct_arg env spec (fun v -> p v && q v)

  | _ ->
      (* In all other cases, we construct an argument and verify a posteriori
         that the predicate [p] is satisfied. *)
      let (_, rv, _) as outcome = construct_arg_no_requirement env spec in
      if p rv then outcome else Gen.reject()

(* [construct_arg_no_requirement] specializes [construct_arg] to the case
   where the precondition [p] is trivial (always true). This special case
   is common and can be handled more efficiently. *)

and construct_arg_no_requirement
: type r c . env -> (r, c) spec -> arg * r * c
= fun env spec ->
  match spec with

  | SpecBaseAbstract _ ->
      (* To avoid code duplication, jump back to [construct_arg]. *)
      construct_arg env spec no_requirement

  | SpecSubset (spec, q) ->
      (* Easy. *)
      construct_arg env spec q

  | SpecConstructible { generate } ->
      (* We have a generation function, which we can use to obtain a
         value [v]. Because this is a concrete type, the same value
         works on both sides. *)
      let code = generate() in
      let arg = ArgConstant (Code.print code []) in
      let v = Code.value code in
      arg, v, v

  | SpecUnit ->
      ArgUnit, (), ()

  | SpecPair (spec1, spec2) ->
      (* Construct a value for each pair component. *)
      let arg1, rv1, cv1 = construct_arg_no_requirement env spec1
      and arg2, rv2, cv2 = construct_arg_no_requirement env spec2 in
      ArgPair (arg1, arg2), (rv1, rv2), (cv1, cv2)

  | SpecOption spec ->
      (* Choose between constructing [None] and constructing [Some _]. *)
      if Gen.bool() then
        ArgOption None, None, None
      else
        let arg, rv, cv = construct_arg_no_requirement env spec in
        ArgOption (Some arg), Some rv, Some cv

  | SpecResult (spec1, spec2) ->
      if Gen.bool() then
        let arg, rv, cv = construct_arg_no_requirement env spec1 in
        ArgResult (Ok arg), Ok rv, Ok cv
      else
        let arg, rv, cv = construct_arg_no_requirement env spec2 in
        ArgResult (Error arg), Error rv, Error cv

  | SpecEither (spec1, spec2) ->
      if Gen.bool() then
        let arg, rv, cv = construct_arg_no_requirement env spec1 in
        ArgEither (Either.Left arg), Either.Left rv, Either.Left cv
      else
        let arg, rv, cv = construct_arg_no_requirement env spec2 in
        ArgEither (Either.Right arg), Either.Right rv, Either.Right cv

  | SpecList (length, spec) ->
      (* If we view [SpecList] as strictly synonymous with a recursive
         specification that involves a sum type [Nil + Cons], then we should
         flip a coin so as to choose between [Nil] and [Cons] and continue.
         But this doesn't seem very smart, as it amounts to encoding the
         length of the list in unary notation, and yields a small probability
         of generating long lists. For this reason, we prefer to use a
         different generation strategy, where we pick the length of the list
         up front in the semi-open interval [0, n). *)
      let n = length() in
      let args, rvs, cvs = construct_arg_list env spec n [] [] [] in
      ArgList args, rvs, cvs

  | SpecMapOutof (rwrap, cwrap, spec) ->
      begin
        let arg, rv, cv = construct_arg_no_requirement env spec in
        let arg = ArgAppConstant (Code.print cwrap [], arg) in
        match rwrap rv with
        | exception e ->
            raise (ConstructArg (arg, ReferenceWrapperFailure (freeze e)))
        | rv ->
        match Code.value cwrap cv with
        | exception e ->
            raise (ConstructArg (arg, CandidateWrapperFailure (freeze e)))
        | cv ->
        arg, rv, cv
      end

  (* Recursive specifications are unfolded on the fly. *)
  | SpecDeferred spec ->
      construct_arg_no_requirement env (Lazy.force spec)

  (* [SpecIfPol] is interpreted on the fly. Its first argument represents
     the construction side. *)
  | SpecIfPol (spec, _) ->
      construct_arg_no_requirement env spec

  (* We do not expect any of the following cases to arise. *)
  | SpecDeconstructible _ ->
      assert false
  | SpecTop ->
      assert false
  | SpecArrow _ ->
      assert false
  | SpecDependentArrow _ ->
      assert false
  | SpecNondet _ ->
      assert false
  | SpecMapInto _ ->
      assert false

and construct_arg_list
: type r c . env -> (r, c) spec -> int ->
             arg list -> r list -> c list -> arg list * r list * c list
= fun env spec n args rvs cvs ->
  if n = 0 then
    args, rvs, cvs
  else
    let arg, rv, cv = construct_arg_no_requirement env spec in
    construct_arg_list env spec (n-1) (arg :: args) (rv :: rvs) (cv :: cvs)

(* [construct_arg_no_requirement env spec] generates an argument of
   type [spec]. It returns a triple of a reference value, a candidate
   value, and an argument. *)

let construct_arg_no_requirement env spec =
  section @@ fun () ->
  log "Constructing an argument.\n%!";
  construct_arg_no_requirement env spec

(* -------------------------------------------------------------------------- *)

(* Using an operation (by placing it in a context). *)

(* We do this by starting with the trivial expression [EOp op] and growing
   it into a larger expression. *)

(* [use env spec e rv cv] uses the expression [e], whose (dual) value is [rv]
   / [cv], and which conforms to the specification [spec]. Based on [spec], we
   determine how this expression should be used, that is, in what context it
   should be placed: e.g., if it is a function, then it should be applied to
   an appropriate argument. Thus, we build a larger expression, which we
   evaluate, and the process continues.

   This process goes on as long as [spec] is a "negative" type, that is, an
   opaque type, typically a function type. Once a "positive" type is reached,
   this process stops and we move on to a different phase, where the value is
   deconstructed.

   This process can fail if either the reference implementation or the
   candidate implementation raises an exception.

   Regardless of success or failure, [use] always returns the expression that
   was generated. In case of success, it also returns the residual value [v']
   obtained by evaluating the original value in this context. In case of
   failure, it returns the failure observed by evaluating the original value
   in this context. *)

let rec use
: type r c .
  env -> (r, c) spec -> expr -> r -> c -> expr * (value, failure) result
= fun env spec expr rv cv ->
  match spec with

  | SpecArrow (spec1, spec2) ->
      (* Remap this on the fly to a trivial dependent arrow, so as to
         avoid redundancy with the next case. *)
      use env (SpecDependentArrow (spec1, fun _ -> spec2)) expr rv cv

  | SpecDependentArrow (spec1, spec2) ->
      log "use: dependent arrow.\n%!";
      begin
        (* Generate an argument [arg1] of type [spec1]. *)
        match construct_arg_no_requirement env spec1 with
        | exception ConstructArg (arg1, failure) ->
            EAppL (expr, arg1), Error failure
        | arg1, rv1, cv1 ->
        (* Construct the application of [expr] to [arg1]. *)
        let expr = EAppL (expr, arg1) in
        (* [spec2] is a function of [rv1] to a specification. Apply it. *)
        let spec2 = spec2 rv1 in
        (* Evaluate the application [expr arg1] on each side. In the absence
           of failures, it would not matter in which order we evaluate them.
           However, if the reference implementation raises [PleaseBackOff],
           then we wish to back off and try another operation (within the same
           scenario). This is safe only if the candidate implementation has
           not had an opportunity to perform side effects; so the reference
           implementation must run first. The candidate implementation is
           allowed to raise [Unimplemented]; in that case, because the side
           effects of the reference implementation cannot be undone, we start
           afresh. *)
        match rv rv1 with
        | exception e ->
            expr, Error (ReferenceFailure (freeze e))
        | rv2 ->
        match cv cv1 with
        | exception e ->
            expr, Error (CandidateFailure (freeze e))
        | cv2 ->
        (* Continue. *)
        use env spec2 expr rv2 cv2
      end

  | SpecMapInto (rwrap, cwrap, spec) ->
      log "use: transform (map_into).\n%!";
      begin
        (* The user has provided an operation of some unknown type [foo] and
           wants to wrap it so that it appears to have type [spec]. The user
           provides a wrapper of type [foo -> spec], whose implementations on
           the reference side and candidate side are [rwrap] and [cwrap]. *)
        (* Generate the expression [freeze expr]. *)
        let expr = EAppR (Code.print cwrap, expr) in
        (* Evaluate this application on each side. *)
        match rwrap rv with
        | exception e ->
            expr, Error (CandidateWrapperFailure (freeze e))
        | rv ->
        match Code.value cwrap cv with
        | exception e ->
            expr, Error (ReferenceWrapperFailure (freeze e))
        | cv ->
        (* Continue. *)
        use env spec expr rv cv
      end

  (* Recursive specifications are unfolded on the fly. *)
  | SpecDeferred spec ->
      log "use: deferred spec.\n%!";
      use env (Lazy.force spec) expr rv cv

  (* [SpecIfPol] is interpreted on the fly. Its first second represents
     the deconstruction side. *)
  | SpecIfPol (_, spec) ->
      log "use: ifpol.\n%!";
      use env spec expr rv cv

  | spec ->
      (* Done. *)
      log "use: done generating a context.\n%!";
      expr, Ok (Value (spec, rv, cv))

(* [generate_instruction env] generates an instruction of the form
   [let _ = context[op]] and evaluates its right-hand side. (The wildcard
   pattern on the left-hand side is intended to be later replaced with
   a more interesting pattern [pat].) Like [use], this operation always
   produces an instruction; furthermore, it produces a result which tells
   whether evaluation resulted in a value or in a failure. *)

let generate_instruction env : instruction * (value, failure) result =
  log "Generating an instruction.\n%!";
  section @@ fun () ->
  (* Pick an operation. *)
  let op, Value (spec, rv, cv) = pick() in
  log "Picked operation \"%s\".\n%!" op;
  (* Generate an expression that uses this operation,
     and evaluate this expression. *)
  let expr, result = use env spec (EOp op) rv cv in
  (* Generate an instruction. At this point, we have not yet decided
     how to deconstruct the result, so we temporarily use a wildcard
     pattern. *)
  I (PatWildcard, expr), result

(* -------------------------------------------------------------------------- *)

(* Deconstructing a result. *)

(* [deconstruct env rv cv spec] simultaneously deconstructs the reference
   value [rv] and the candidate value [cv], whose relational type is [spec].

   It returns a pair of a Boolean outcome [ok] and a pattern [pat]. In [ok] is
   [true], the values [rv] and [cv] agree, and the pattern [pat] matches both
   of them. If [ok] is [false], the values [rv] and [cv] disagree, and the
   pattern [pat] matches [rv] but not [cv].

   In the case of a success, the environment [env] is appropriately extended.
   In the case of a failure, it is partially extended. That should not be a
   problem; if it turned out to be a problem, we could easily reset it to its
   initial height. *)

(* [deconstruct] fails if the reference implementation of a nondeterministic
   operation raises an exception. This is an abnormal situation. We deal with
   it by wrapping this exception in a [Deconstruct] exception. We lose some
   information as this exception is propagated back up (we forget where we
   were in the tree), but it seems difficult to do better. *)

exception Deconstruct of failure

let rec deconstruct : type r c .
  env -> r -> c -> (r, c) spec -> bool * pat
= fun env rv cv spec ->
  match spec, rv, cv with

  | SpecTop, _, _ ->
      log "deconstruct: top.\n%!";
      true, PatWildcard

  | SpecDeconstructible { equal; print }, _, _ ->
      log "deconstruct: deconstructible type.\n%!";
      (* [equal] is a user-defined notion of equality at this type. *)
      if Code.value equal rv cv then
        (* Agreement. *)
        true, PatObserveAgreement
      else
        (* Disagreement. *)
        let assertion = print_equality_assertion equal (print rv) (print cv) in
        false, PatObserveDisagreement assertion

  | SpecBaseAbstract _, _, _ ->
      log "deconstruct: abstract base type.\n%!";
      let x = Env.limit env in
      Env.bind env (Value (spec, rv, cv));
      true, PatBind x

  | SpecUnit, (), () ->
      log "deconstruct: unit type.\n%!";
      true, PatUnit

  | SpecPair (spec1, spec2), (rv1, rv2), (cv1, cv2) ->
      log "deconstruct: pair type.\n%!";
      section @@ fun () ->
      let ok1, pat1 = deconstruct env rv1 cv1 spec1 in
      if ok1 then
        let ok2, pat2 = deconstruct env rv2 cv2 spec2 in
        if ok2 then
          true, PatPair (pat1, pat2)
        else
          false, PatPair (PatWildcard, pat2)
      else
          false, PatPair (pat1, PatWildcard)

  | SpecOption _, None, None ->
      log "deconstruct: option type (None/None).\n%!";
      true, PatOption None

  | SpecOption spec, Some rv, Some cv ->
      log "deconstruct: option type (Some/Some).\n%!";
      let ok, pat = deconstruct env rv cv spec in
      ok, PatOption (Some pat)

  | SpecOption _, None, Some _ ->
      log "deconstruct: option type (None/Some).\n%!";
      false, PatOption None

  | SpecOption _, Some _, None ->
      log "deconstruct: option type (Some/None).\n%!";
      false, PatOption (Some PatWildcard)

  | SpecResult (spec, _), Ok rv, Ok cv ->
      log "deconstruct: result type (Ok/Ok).\n%!";
      let ok, pat = deconstruct env rv cv spec in
      ok, PatResult (Ok pat)

  | SpecResult (_, spec), Error rv, Error cv ->
      log "deconstruct: result type (Error/Error).\n%!";
      let ok, pat = deconstruct env rv cv spec in
      ok, PatResult (Error pat)

  | SpecResult _, Error _, Ok _ ->
      log "deconstruct: option type (Error/Ok).\n%!";
      false, PatResult (Error PatWildcard)

  | SpecResult _, Ok _, Error _ ->
      log "deconstruct: option type (Ok/Error).\n%!";
      false, PatResult (Ok PatWildcard)

  | SpecEither (spec, _), Either.Left rv, Either.Left cv ->
      log "deconstruct: either type (Left/Left).\n%!";
      let ok, pat = deconstruct env rv cv spec in
      ok, PatEither (Either.Left pat)

  | SpecEither (_, spec), Either.Right rv, Either.Right cv ->
      log "deconstruct: either type (Right/Right).\n%!";
      let ok, pat = deconstruct env rv cv spec in
      ok, PatEither (Either.Right pat)

  | SpecEither _, Either.Right _, Either.Left _ ->
      log "deconstruct: option type (Right/Left).\n%!";
      false, PatEither (Either.Right PatWildcard)

  | SpecEither _, Either.Left _, Either.Right _ ->
      log "deconstruct: option type (Left/Right).\n%!";
      false, PatEither (Either.Left PatWildcard)

  | SpecList _, [], [] ->
      log "deconstruct: list type (Nil/Nil).\n%!";
      true, PatNil

  | SpecList (_, element), rv :: rvs, cv :: cvs ->
      log "deconstruct: list type (Cons/Cons).\n%!";
      (* Unfold [SpecList] on the fly. A nonempty list is viewed as an
         application of a unary [Cons] data constructor to a pair of an
         element and a list. *)
      let ok, pat =
        deconstruct env (rv, rvs) (cv, cvs) (SpecPair (element, spec)) in
      ok, PatCons pat

  | SpecList _, [], _ :: _ ->
      log "deconstruct: list type (Nil/Cons).\n%!";
      false, PatNil

  | SpecList _, _ :: _, [] ->
      log "deconstruct: list type (Cons/Nil).\n%!";
      false, PatCons (PatPair (PatWildcard, PatWildcard))

  | SpecNondet spec, _, _ ->
      log "deconstruct: SpecNondet.\n%!";
      (* We expect the reference value [rv] to be a function, which expects
         the candidate value [cv] as an argument, and returns a diagnostic. *)
      begin match rv cv with
      | Valid rv ->
          (* The reference implementation is happy with the candidate value
             [cv] and produces its own value [rv]. Continue. *)
          deconstruct env rv cv spec
      | Invalid assertion ->
          (* The reference implementation is unhappy with [cv] and produces
             an assertion that explains the problem. *)
          false, PatObserveDisagreement (assertion ovar)
      | exception e ->
          (* The reference implementation inexplicably fails. *)
          raise (Deconstruct (ReferenceFailure (freeze e)))
      end

  | SpecMapInto (rwrap, cwrap, spec), _, _ ->
      log "deconstruct: transform (map_into).\n%!";
      (* Transform the values [rv] and [cv] and continue. *)
      let ok, pat = deconstruct env (rwrap rv) (Code.value cwrap cv) spec in
      (* Generate a function application pattern. *)
      ok, PatAppR (Code.print cwrap, pat)

  (* Recursive specifications are unfolded on the fly. *)
  | SpecDeferred spec, _, _ ->
      deconstruct env rv cv (Lazy.force spec)

  (* [SpecIfPol] is interpreted on the fly. Its first second represents
     the deconstruction side. *)
  | SpecIfPol (_, spec), _, _ ->
      deconstruct env rv cv spec

  (* We do not expect the following cases to arise. *)
  | SpecConstructible _, _, _ ->
      assert false
  | SpecSubset _, _, _ ->
      assert false
  | SpecArrow _, _, _ ->
      assert false
  | SpecDependentArrow _, _, _ ->
      assert false
  | SpecMapOutof _, _, _ ->
      assert false

(* -------------------------------------------------------------------------- *)

(* Well-formedness checks. *)

(* The user-provided function [check] is expected to perform some kind of
   internal well-formedness check. It can fail by raising an arbitrary
   exception [e], perhaps an [Assert_failure]. It has access to both the
   reference value and the candidate value, so (if desired) it can check that
   the candidate data structure conforms to its logical model. *)

let perform_checks env past =
  Env.foreach env (fun x (Value (spec, rv, cv)) ->
    (* We have a variable [x], its relational type [spec],
       its value [rv] in the reference implementation, and
       its value [cv] in the candidate implementation. *)
    match spec with
    | SpecBaseAbstract (_, properties) ->
        let check = Code.value (properties.aty_check rv) in
        begin try
          check cv
        with e ->
          raise_abort env past (CheckFailure (x, (freeze e)))
        end
    | _ ->
        assert false (* every variable has abstract type *)
  )

(* -------------------------------------------------------------------------- *)

(* The engine's main loop. *)

(* [fuel] is the number of instructions that we are still allowed to generate.
   [past] is a reversed list of the instructions generated and executed so
   far. *)

let rec test fuel past env : unit =

  (* If the maximum number of instructions has been reached, stop. Otherwise,
     generate an instruction. *)

  if fuel > 0 then match generate_instruction env with

  | exception Gen.OutOfInputData ->
      (* The generation of a new instruction involves making choices, thus
         consuming input data. This can fail if there is no more input data.
         In that case, the test is over. We do not abort; we terminate
         normally, so another test can run. *)
      let pc = List.length past in
      printf "@%02d: Input data exhausted; end of this test.\n" pc

  | exception Gen.Reject ->
      (* The generation of a new instruction involves making choices, thus
         consuming input data. This can fail if the input data does not suit
         us. In that case, try generating another instruction. *)
      log "Generation of an instruction failed; retrying.\n";
      test fuel past env

  | exception IllFormedSpec (op, msg) ->
      (* The generation of an instruction involves a call to [normalize],
         which can fail if a specification is ill-formed. *)
      error "in the specification of operation `%s`:\n%s" op msg

  | exception e ->
      (* Another exception indicates an abnormal condition, perhaps a mistake
         in the generation code. It should be reported, so it can be fixed. *)
      printf "An exception was raised during generation!\n";
      raise e

  | _, Error (ReferenceFailure { e = PleaseBackOff; _ }) ->
      (* The reference implementation does not allow the operation that was
         chosen, or some particular use of this operation. Abandon this
         attempt and try some other operation within the current scenario. The
         reference implementation runs first and is not allowed to perform a
         side effect before raising [PleaseBackOff], so this is safe. *)
      (* We do not decrease any parameter in the recursive call: although this
         could cause nontermination, I don't think it can be a problem, as
         afl-fuzz will abort every run at some point anyway. *)
      test fuel past env

  | _, Error (CandidateFailure { e = Unimplemented; _ }) ->
      (* The reference implementation does not allow the operation that was
         chosen, or some particular use of this operation. Abandon this
         attempt entirely and start a new scenario. *)
      ()

  | i, Error failure ->
      let past = i :: past in
      raise_abort env past failure

  | I (pat, expr), Ok v ->
      assert (pat = PatWildcard);

      (* Both the reference implementation and the candidate implementation
         have run successfully. An instruction [i] has just been constructed
         and executed, and a value [v] has been obtained as a result. *)

      (* Out of [v], we extract a reference value [rv] and a candidate value
         [cv], described by [spec]. *)

      let Value (spec, rv, cv) = v in

      (* We now deconstruct these values. While doing so, we check that they
         are in agreement; if so, we construct a pattern and extend the
         environment; if not, we also construct a pattern (one that explains
         the disagreement) and stop. *)

      match deconstruct env rv cv spec with

      | exception Deconstruct failure ->
          (* We do not have an exact context, so we use a wildcard pattern.
             The scenario that we print will not quite explain the problem,
             but it cannot explain the problem anyway, as the scenario is
             phrased in terms of the candidate implementation, and the error
             here lies in the reference implementation, which has a different
             type and takes one more argument, as [nondet] is used. *)
          let pat = PatWildcard in
          let past = I (pat, expr) :: past in
          raise_abort env past failure

      | ok, pat ->

      (* Record this instruction. *)
      let past = I (pat, expr) :: past in

      if not ok then begin

        (* The values [rv] and [cv] disagree in a concrete way, e.g., at
           a concrete type, or at a sum type. The pattern [pat] exhibits
           the problem; it is a pattern that matches [rv] but does not
           match [cv]. *)

        (* Report the problem. *)
        raise_abort env past ObservationFailure

      end
      else begin

        (* [pat] is a pattern that matches both [rv] and [cv]. *)

        (* Consume one unit of fuel. *)
        let fuel = fuel - 1 in

        (* Make sure that every data structure is well-formed. *)
        perform_checks env past;

        (* Continue. *)
        test fuel past env

      end

(* -------------------------------------------------------------------------- *)

(* In order to save the cost of allocating a fresh (empty) environment for
   every run, we re-use the same environment over and over. The operation
   [Env.clear] is extremely cheap. *)

let stored : env option ref =
  ref None

let env fuel : env =
  match !stored with
  | None ->
      (* Compute a bound on the size of the environment. This should ideally
         be computed by multiplying [fuel] by the maximum number of variables
         that a single operation can bind, that is, the maximum number of
         results of abstract type that an operation returns. For the moment,
         let's estimate this maximum number to be 5. *)
      let bound = 5 * fuel in
      (* Create an empty initial environment. *)
      let dummy_value = Value (SpecUnit, (), ()) in
      let env = Env.empty bound dummy_value in
      (* Store it for later re-use. *)
      stored := Some env;
      (* Return it. *)
      env
  | Some env ->
      (* We assume that every run uses the same value of [fuel], so the
         existing environments have an appropriate maximum size. *)
      Env.clear env;
      env

(* -------------------------------------------------------------------------- *)

(* Initialization. *)

let test fuel =
  log "Beginning one test run.\n%!";
  section @@ fun () ->
  (* No past. *)
  let past = [] in
  (* Run. *)
  let env = env fuel in
  test fuel past env;
  (* Done. *)
  log "This test run is finished.\n%!"

(* -------------------------------------------------------------------------- *)

(* [run prologue fuel] performs one test run. *)

(* The function [prologue] is executed after the source channel has been
   opened, so it is allowed to call the data generation functions in the
   module [Gen]. It is also allowed to call [declare], [override_exn_eq],
   [dprintf], etc. Thus, it can modify our global state in several ways. *)

(* [prologue] is an optional argument. Its default value is [ignore],
   which has no effect. *)

let run prologue fuel =
  (* Restore a correct initial state for this iteration. *)
  GlobalState.reset();
  (* Execute [prologue()], which can declare new operations, etc. *)
  match prologue() with
  | exception Gen.OutOfInputData ->
      log "Prologue: input data exhausted; abandoning.\n"
  | exception Gen.Reject ->
      log "Prologue: generation failure; abandoning.\n"
  | exception e ->
      printf "Prologue: an exception was raised!\n";
      raise e
  | _ ->
      (* Run the test. *)
      test fuel

(* -------------------------------------------------------------------------- *)

(* [init()] performs global initialization. *)

(* It is used both in random testing mode and in AFL mode. *)

let init () =
  (* Printing the following two lines at the beginning of every scenario
     allows us to use [Monolith.Support], under the name [Sup], in our
     scenarios. *)
  DelayedOutput.dprintf "          #require \"monolith\";;\n";
  DelayedOutput.dprintf "          module Sup = Monolith.Support;;\n";
  (* We are about to perform many runs, and each run begins with a call to
     [prologue] that can modify our global state by calling functions such
     as [declare], [override_exn_eq], [dprintf], etc. Therefore, we must
     save our global state now, just once, and reset it at the beginning
     of every run, before calling [prologue]. *)
  GlobalState.save()

(* -------------------------------------------------------------------------- *)

(* Settings. *)

type prologue =
  unit -> unit

type fuel =
  int

type settings = {

  source : string option;
    (**An optional file name. If this file name is present, then the engine
       runs in AFL mode and this file is used as a source of random bits.
       If it is absent, then the engine runs in random testing mode and
       /dev/urandom is used as a source of random bits. *)

  timeout : float option;
    (**An optional time limit, expressed in seconds. *)

  max_scenarios : int;
    (**In random testing mode, if [max_scenarios] failure scenarios are
       found, then testing stops. *)

  show_scenario : bool;
    (**This Boolean flag determines whether failure scenarios should be
       printed to the standard output channel. *)

  save_scenario : bool;
    (**This Boolean flag determines whether failure scenarios should be
       saved to a file in the directory [./output/crashes]. *)

  prologue : prologue;
    (**A prologue. *)

  fuel : fuel;
    (**The desired initial amount of fuel. *)

}

(* -------------------------------------------------------------------------- *)

(* [run_afl settings] performs many test runs in AFL mode. *)

(* [settings.source] must be [Some name], where [name] is the name of the
   input file that AFL has created for us. *)

(* We use [AflPersistent.run] to perform many test runs, say 1001. Each run
   must open and close the source file, as it is recreated afresh by AFL for
   each run. *)

let run_afl settings =
  assert (settings.source <> None);
  AflPersistent.run (fun () ->
    Gen.with_source settings.source (fun () ->
      try
        run settings.prologue settings.fuel
      with Abort (scenario, _fuel) ->
        (* Print the scenario to [stdout]. This is necessary for the user
           to be able to find out what happened. *)
        output_string stdout scenario;
        flush stdout;
        abort()
    )
  );
  0

(* -------------------------------------------------------------------------- *)

(* [tick clock fuel] ticks the clock [clock] and, once in a while,
   displays an information message. *)

let[@inline] tick clock settings =
  Clock.tick clock @@ fun () ->
    printf "%s tests run so far (%s/s overall, %s/s now) (fuel = %d).\n%!"
      (summarize (Clock.ticks clock))
      (summarize (Clock.overall_ticks_per_second clock))
      (summarize (Clock.current_ticks_per_second clock))
      settings.fuel

(* [show_and_save scenario settings] logs the failure scenario [scenario] on
   [stdout] and saves it in a file in the directory ./output/crashes. *)

let[@inline] show_and_save scenario settings =
  if settings.show_scenario then begin
    (* Print the scenario to [stdout]. *)
    output_string stdout scenario;
    print_newline();
    flush stdout
  end;
  if settings.save_scenario then begin
    (* Write the scenario into a file. *)
    let temp_dir = "./output/crashes" in
    mkdirp temp_dir;
    let prefix = sprintf "scenario.%03d." settings.fuel
    and suffix = "" in
    let _, oc = Filename.open_temp_file ~temp_dir prefix suffix in
    output_string oc scenario;
    close_out_noerr oc
  end

(* -------------------------------------------------------------------------- *)

(* [run_random_loop clock settings accu] performs an unbounded number of
   test runs in random mode. *)

(* While the tests run, we print information roughly every second. We print
   how many tests have been performed so far, our overall average speed, and
   our current speed. *)

(* If a failure is discovered, the problematic scenario is printed to [stdout]
   and logged to a file in the directory ./output/crashes. Then, we start over
   with a possibly smaller value of [settings.fuel], in the hope of
   discovering a shorter failure scenario. *)

(* For each value of [settings.fuel], we use an explicit infinite loop to
   perform an unbounded number of runs. *)

(* If the clock [clock] has no time limit, then [run_random_loop] never
   terminates. If this clock has a time limit then [run_random_loop]
   terminates once the time limit has been reached, and it returns the number
   of failure scenarios that have been discovered and logged along the way.
   The accumulator [accu] records the number of failure scenarios discovered
   so far. *)

type failures =
  int

let rec run_random_loop settings clock (accu : failures) : failures =
  try
    (* An infinite loop. *)
    while true do
      (* Perform one run. *)
      run settings.prologue settings.fuel;
      (* Tick the clock and, once in a while, display statistics. *)
      tick clock settings
    done;
    (* This cannot happen. *)
    assert false
  with
  | Abort (scenario, fuel) ->
      show_and_save scenario settings;
      (* We have been able to find a problem with a certain amount of
         fuel. Try again, with this amount. This restricts our search
         space, and (with luck) we might now be able to find an even
         shorter scenario. *)
      let settings = { settings with fuel }
      and accu = accu + 1 in
      if accu = settings.max_scenarios then
        accu
      else
        run_random_loop settings clock accu
  | Clock.Timeout ->
      accu

(* [run_random settings] performs an unbounded number of test
   runs in random mode. *)

(* The source of random bits, /dev/urandom, is opened just once;
   it would be pointless to close it and reopen it many times. *)

let run_random settings : failures =
  assert (settings.source = None);
  Gen.with_source settings.source @@ fun () ->
  let granularity = 1000 in
  let timeout = settings.timeout in
  let clock = Clock.make ?timeout granularity in
  let accu = 0 in
  run_random_loop settings clock accu

(* -------------------------------------------------------------------------- *)

(* [parse prologue fuel] parses the command line and produces a settings
   record. The [fuel] parameter can be overridden by the [--fuel] setting
   that is provided on the command line. *)

let parse prologue fuel : settings =
  let source, timeout, fuel, max_scenarios, save_scenario, show_scenario =
    ref None, ref None, ref fuel, ref max_int, ref true, ref true
  in
  let set_save_scenario b = save_scenario := b in
  let set_show_scenario b = show_scenario := b in
  let set_timeout t = timeout := Some (float_of_int t) in
  let spec = Arg.align [

    "--fuel",
      Arg.Set_int fuel,
      "<int> Set a fuel limit";

    "--max-scenarios",
      Arg.Set_int max_scenarios,
      "<int> Stop if this number of failure scenarios is reached";

    "--save-scenario",
      Arg.Bool set_save_scenario,
      "<bool> Enable/disable saving scenarios on disk";

    "--show-scenario",
      Arg.Bool set_show_scenario,
      "<bool> Enable/disable showing scenarios on stdout";

    "--timeout",
      Arg.Int set_timeout,
      "<int> Set a time limit (in seconds) (random testing mode only)";

  ] in

  let usage = sprintf "Usage: %s <input file>" Sys.argv.(0) in
  Arg.parse spec (fun s -> source := Some s) usage;

  let source, timeout, fuel, max_scenarios, save_scenario, show_scenario =
    !source, !timeout, !fuel, !max_scenarios, !save_scenario, !show_scenario
  in

  { source; timeout;
    max_scenarios; save_scenario; show_scenario;
    prologue; fuel }

(* -------------------------------------------------------------------------- *)

(* [run settings] starts the engine. *)

let run settings =
  init();
  let failures =
    (* If a source file name was provided on the command line, enter AFL mode;
       otherwise, enter random testing mode. *)
    match settings.source with
    | Some _ ->
        run_afl settings
    | None ->
        run_random settings
  in
  exit (if failures > 0 then 1 else 0)

(* -------------------------------------------------------------------------- *)

(* [main ?prologue fuel] parses the command line and starts testing. *)

let main ?(prologue = ignore) fuel =
  let settings = parse prologue fuel in
  run settings