(****************************************************************************)
(*                           the diy toolsuite                              *)
(*                                                                          *)
(* Jade Alglave, University College London, UK.                             *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France.                          *)
(*                                                                          *)
(* Copyright 2010-present Institut National de Recherche en Informatique et *)
(* en Automatique, ARM Ltd and the authors. All rights reserved.            *)
(*                                                                          *)
(* This software is governed by the CeCILL-B license under French law and   *)
(* abiding by the rules of distribution of free software. You can use,      *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL        *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt.            *)
(****************************************************************************)
(* Authors:                                                                 *)
(* Jade Alglave, University College London, UK.                             *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France.                          *)
(* Hadrien Renaud, University College London, UK.                           *)
(****************************************************************************)

(** Produce event structures (which include variables) + constraints,
   using instruction semantics *)

module type CommonConfig = sig
  val verbose : int
  val optace : OptAce.t
  val unroll : int option
  val speedcheck : Speed.t
  val debug : Debug_herd.t
  val observed_finals_only : bool
  val initwrites : bool
  val check_filter : bool
  val maxphantom : int option
  val variant : Variant.t -> bool
  val fault_handling : Fault.Handling.t
  val mte_precision : Precision.t
end

module type Config = sig
  include CommonConfig
  val byte : MachSize.sz
  val dirty : DirtyBit.t option
end

module type S = sig

  module S : Sem.Semantics

  type result =
     {
       event_structures : (int * S.M.VC.cnstrnts * S.event_structure) list ;
       overwritable_labels : Label.Set.t ;
     }

(** [glommed_event_structures t] performs "instruction semantics".
 *  Argument [t] is a test.
 *  The function returns a pair whose first component is a record.
 *
 *  It includes a set (list) of "abstract"  event structures. In such
 *  structures, most values (and locations) are not resolved yet. Hence the
 *  [S.M.VC.cnstrnts] second component. Those are equations to be solved
 *  once some read-from relation on memory is selected by the function
 *  [calculate_rf_with_cnstrnts] (see below). The record also includes
 *  additional processing information to pass on to calculate_rf_with_cnstrnts,
 *  which is the set of labels that are allowed to be addressed by stores.
 *
 *  Second component of the returned pair is the test itself,
 *  which can be slightly modified (noticeably in the case of
 *  `-variant self`, initial values of overwitable code locations
 *  are added.
 *
 *  This modified test *must* be used in the following. *)

  val glommed_event_structures : S.test -> result * S.test



(* A first generator,
   calculate_rf_with_cnstrnts test es constraints kont res,

   - test and es are test description and (abstract) event structure.
     By abstract, we here mean that some values and even
     memory locations in them are variables.

   - constraints is a set of constraint, which
     * Is solvable: ie resolution results
       in either an assigment of all variables in es, or
       in failure.
     * expresses the constraints generated by semantics.

   - kont : S.concrete -> VC.cnstrnts -> 'a  -> 'a
     will be called on all generated concrete event structures, resulting
     in  computation:
     kont (esN (... (kont es1 res)))
     where esK is the
        + abstract event structure with variables replaced by constants
        + [Failed] of [Warn] constraint from equations, if any
        + rfmap
        + final state (included in rfmap in fact)
 *)


  val calculate_rf_with_cnstrnts :
      S.test -> Label.Set.t -> S.event_structure -> S.M.VC.cnstrnts ->
        (S.concrete -> S.M.VC.cnstrnt option -> 'a -> 'a ) -> (* kont *)
          'a -> 'a

  val solve_regs :
      S.test -> S.E.event_structure -> S.M.VC.cnstrnt list ->
        (S.E.event_structure * S.read_from S.RFMap.t * S.M.VC.cnstrnt list) option

  val solve_mem :
      S.test ->S.E.event_structure -> S.read_from S.RFMap.t -> S.M.VC.cnstrnt list ->
        (S.E.event_structure ->
          S.read_from S.RFMap.t -> S.M.VC.cnstrnt list -> 'a -> 'a) ->
            'a -> 'a

  val check_sizes : S.test -> S.event_structure -> unit

  val check_rfmap :
      S.E.event_structure -> S.read_from S.RFMap.t -> bool

  val when_unsolved :
      S.test -> S.E.event_structure -> S.read_from S.RFMap.t -> S.M.VC.cnstrnt list -> 'a -> 'a

  val compute_final_state :
    S.test -> S.read_from S.RFMap.t -> S.E.EventSet.t -> S.A.state * S.A.FaultSet.t

  val check_filter : S.test -> S.A.state * S.A.FaultSet.t -> bool

  val get_loc :
    S.E.event -> S.E.A.location

  val make_atomic_load_store :
    S.E.event_structure -> S.E.EventRel.t

end

open Printf

module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
  struct
    module S = S

    module A = S.A
    module B = S.B
    module AM = A.Mixed(C)
    module V = A.V
    module E = S.E
    module EM = S.M
    module VC = EM.VC
    module U = MemUtils.Make(S)
    module W = Warn.Make(C)

    let dbg = C.debug.Debug_herd.mem
    let morello = C.variant Variant.Morello
    let mixed = C.variant Variant.Mixed || morello
    let unaligned = C.variant Variant.Unaligned
    let memtag = C.variant Variant.MemTag
        (* default is checking *)
    let check_mixed =  not (C.variant Variant.DontCheckMixed)
    let do_deps = C.variant Variant.Deps
    let kvm = C.variant Variant.VMSA
    let self = C.variant Variant.Ifetch
    let asl = C.variant Variant.ASL
    let oota = C.variant Variant.OOTA
    let unroll =
      match C.unroll with
      | None -> Opts.unroll_default A.arch
      | Some u -> u

(*****************************)
(* Event structure generator *)
(*****************************)

(* Relabeling (eiid) events so as to get memory events labeled by 0,1, etc *)
    module IMap =
      Map.Make
        (struct
          type t = E.eiid
          let compare = Misc.int_compare
        end)

    let count_mem evts =
      E.EventSet.fold
        (fun e k ->
          if E.is_mem e then k+1
          else k)
        evts 0

    let build_map n_mem evts =
      let build_bd e (next_mem,next_other,k) =
        let key = e.E.eiid in
        if E.is_mem e then
          (next_mem+1,next_other,IMap.add key next_mem k)
        else
          (next_mem,next_other+1,IMap.add key next_other k) in
      let _,_,r = E.EventSet.fold build_bd evts (0,n_mem,IMap.empty) in
      r

(* Note: events from mem_accesses are not relabeled, as they are not part of final events *)
    let relabel es =
      let n_mem = count_mem es.E.events in
      let map = build_map n_mem es.E.events in
      let relabel_event e =
        let id =  e.E.eiid in
        try { e with E.eiid = IMap.find id map }
        with Not_found -> assert (E.EventSet.mem e es.E.mem_accesses) ; e in
       E.map_event_structure relabel_event es


    let (|*|) = EM.(|*|)
    let (>>>) = EM.(>>>)

    let is_back_jump addr_jmp addr_tgt = Misc.int_compare addr_jmp addr_tgt >= 0

    type result =
        {
         event_structures : (int * S.M.VC.cnstrnts * S.event_structure) list ;
         overwritable_labels : Label.Set.t ;
        }

(* All (virtual) locations from init state *)

    let get_all_locs_init init =
      let locs =
        A.state_fold
          (fun loc v locs ->
            let locs =
              match loc with
              | A.Location_global _
                -> loc::locs
              | A.Location_reg _ -> locs in
            try
              match A.V.as_virtual v with
              | Some s ->
                 let sym = Constant.mk_sym_virtual s in
                 A.Location_global (A.V.Val sym)::locs
              | None -> locs
            with V.Undetermined -> locs)
          init [] in
      A.LocSet.of_list locs

(* All (virtual) memory locations reachable by a test *)

    let get_all_mem_locs test =
      let locs_final =
        A.LocSet.filter
          (function
           | A.Location_global _ -> true
           | A.Location_reg _ -> false)
          (S.observed_locations test)
      and locs_init = get_all_locs_init test.Test_herd.init_state in
      let () =
        if dbg then begin
          let pp_locs locs =
            A.LocSet.pp_str "," A.dump_location locs in
          Printf.eprintf
            "locs_init={%s}, locs_final={%s}\n%!"
            (pp_locs locs_init)
            (pp_locs locs_final)
        end in
      let locs = A.LocSet.union locs_final locs_init in
      let locs =
        List.fold_left
          (fun locs (_,code,fh_code) ->
            let code = match fh_code with
              | Some fh_code -> code@fh_code
              | None -> code in
            List.fold_left
              (fun locs (_,ins) ->
                A.fold_addrs
                  (fun x ->
                    let loc = A.maybev_to_location x in
                    match loc with
                    | A.Location_global _ -> A.LocSet.add loc
                    | _ -> fun locs -> locs)
                  locs ins)
              locs code)
          locs
          test.Test_herd.start_points in
      let env =
        A.LocSet.fold
          (fun loc env ->
            try
              let v = A.look_address_in_state test.Test_herd.init_state loc in
              (loc,v)::env
            with A.LocUndetermined -> assert false)
          locs [] in
      env

    module SM = S.Mixed(C)

    type ('a,'b,'c) fetch_r = Ok of 'a * 'b | No of 'a | Segfault of 'c

    let segfault =
      Warn.user_error
        "Segmentation fault (kidding, label %s not found)"

    let glommed_event_structures (test:S.test) =
      let prog = test.Test_herd.program in
      let starts = test.Test_herd.start_points in
      let code_segment = test.Test_herd.code_segment in
      let procs = List.map (fun (p,_,_) -> p) starts in
      let labels_of_instr = test.Test_herd.entry_points in
      let exported_labels = S.get_exported_labels test in
      let is_exported_label lbl =
        Label.Full.Set.exists
          (fun (_,lbl0) -> Misc.string_eq lbl lbl0)
           exported_labels in

(**********************************************************)
(* In mode `-variant self` test init_state is changed:    *)
(*  1. Normalize labels in values                         *)
(*  2. Add initialisation of overwritable instructions    *)
(* Labels have to be normalized because only one memory   *)
(* location holds the instruction that can be pointed to  *)
(* by several labels. Read and write events *must* use a  *)
(* canonical location (label).                            *)
(**********************************************************)

      (* lbls2i -- overwritable instructions, with labels          *)
      (* overwritable_labels -- the set of labels of instructions  *)
      (*                        that are allowed to be overwritten *)
      let lbls2i, overwritable_labels =
        if self then
          List.fold_left
            (fun (ps, ls)  (proc,code,fh_code) ->
              let code = match fh_code with
                | Some fh_code -> code@fh_code
                | None -> code in
              List.fold_left
                (fun (ps, ls) (addr,i) ->
                  let lbls = labels_of_instr addr in
                  if Label.Set.exists is_exported_label lbls
                  then
                      (lbls,(proc,i))::ps,
                      Label.Set.union lbls ls
                  else ps,ls)
                (ps,ls) code)
            ([], Label.Set.empty) starts
        else (* For Adr to work *)
          let lbl2code lbl =
            IntMap.find (Label.Map.find lbl prog) code_segment in
          let ps =
            Label.Full.Set.fold
              (fun (_,lab) ps ->
                try begin
                  match lbl2code lab with
                  | (p,(_,i)::_) ->
                      (Label.Set.singleton lab,(p,i))::ps
                  | (_,[]) -> ps
                end with Not_found -> ps)
              exported_labels [] in
          ps,Label.Set.empty in
      let norm_lbl = (* Normalize labels, useful in `-variant self` *)
        if self then
          let m =
            List.fold_left
              (fun m (lbls,_) ->
                match Label.norm lbls with
                | None -> assert false (* as lbls is non-empty *)
                | Some lbl0 ->
                    Label.Set.fold
                      (fun lbl m -> Label.Map.add lbl lbl0 m)
                      lbls m)
              Label.Map.empty lbls2i in
          fun lbl ->
            try Label.Map.find lbl m
            with
            | Not_found ->
                if Label.Map.mem lbl prog then
                  lbl
                else
                  Warn.user_error
                    "Label %s is undefined, yet it is used as constant"
                    (Label.pp lbl)
        else
          (* Normalisation reduced to label existence check *)
          fun lbl -> ignore (Label.Map.find lbl prog) ; lbl in

      let norm_val = (* Normalize labels in values *)
        if self then
          fun v ->
            match v with
            | V.Val c -> V.Val (Constant.map_label norm_lbl c)
            | _ -> v
        else fun v -> v in

      let test =
        match lbls2i with
        | [] -> test
        | _::_ ->
            let open Test_herd in
            let init_state =
              (* Change labels into their canonical representants *)
              A.map_state norm_val test.init_state in
            let init_state =
              (* Add initialisation of overwritable instructions *)
              List.fold_left
                (fun env (lbls,(proc,i)) ->
                  match Label.norm lbls with
                  | None -> assert false (* as lbls is non-empty *)
                  | Some lbl ->
                      let loc =
                        A.Location_global
                          (A.V.cstToV (Constant.Label (proc, lbl)))
                      and v = A.V.instructionToV i in
                      A.state_add env loc v)
                init_state lbls2i in
            { test with init_state; } in

(*****************************************************)
(* Build events monad, _i.e._ run code in some sense *)
(*****************************************************)

(* Manage labels *)
      let see seen lbl =
        let x = try IntMap.find lbl seen with Not_found -> 0 in
        let x = x+1 in
        let seen = IntMap.add lbl x seen in
        x,seen in

      let get_label lbl addr = match lbl with
        | Some lbl -> lbl
        | None ->
           let lbls = labels_of_instr addr in
           match Label.norm lbls with
           | Some lbl -> lbl
           | None -> sprintf "##%d" addr in

      let tgt2lbl = function
        | B.Lbl lbl -> lbl
        | B.Addr addr -> get_label None addr in

    let fetch_addr check_back seen proc_jmp addr_jmp lbl addr =
        try
          let (proc_tgt,_) as tgt = IntMap.find addr code_segment in
          if (* Limit jump threshold to non determined jumps ? *)
            Misc.int_eq proc_jmp proc_tgt
            && check_back
            && is_back_jump addr_jmp addr
          then
            let x,seen = see seen addr in
            if x > unroll then begin
                W.warn "loop unrolling limit reached: %s" (get_label lbl addr);
                No tgt
              end else
              Ok (tgt,seen)
          else
            Ok (tgt,seen)
        with Not_found ->
            Segfault addr in

      let fetch_code check_back seen proc_jmp addr_jmp = function
        | B.Lbl lbl ->
           begin try
             let addr = Label.Map.find  lbl prog in
             fetch_addr check_back seen proc_jmp addr_jmp (Some lbl) addr
           with Not_found -> segfault lbl
           end
        | B.Addr addr ->
           fetch_addr check_back seen proc_jmp addr_jmp None addr in

      (* All memory locations in a test, with initial values *)
      let env0 = get_all_mem_locs test in

        let addr2v proc s =
          try (* Look for label to overwritable instruction *)
            V.Val (Constant.Label (proc,norm_lbl s))
          with
            e -> (* No, look for data location *)
              let v =  A.V.nameToV s in
              if
                List.exists
                  (fun (a,_) ->
                    match a with
                    | A.Location_global a -> A.V.compare v a=0
                    | _ -> false)
                  env0
              then v else (* No code nor data, check error *)
                match e with
                | Not_found ->
                    Warn.user_error
                      " Symbol %s is not a code label nor a location"
                      s
                | e -> raise e in

(* Call instruction semantics proper *)
        let wrap re_exec fetch_proc proc inst addr env m poi =
        let ii =
           { A.program_order_index = poi;
             proc = proc; fetch_proc; inst = inst;
             labels = labels_of_instr addr;
             lbl2addr = prog;
             addr = addr;
             addr2v=addr2v proc;
             env = env;
             in_handler = re_exec;
           } in
        if dbg then
          Printf.eprintf "%s env=%s\n"
            (A.dump_instruction ii.A.inst)
            (A.pp_reg_state ii.A.env.A.regs) ;
        if dbg && not (Label.Set.is_empty ii.A.labels) then
          eprintf "Instruction %s has labels {%s}\n"
            (A.dump_instruction inst)
            (Label.Set.pp_str ","  Label.pp ii.A.labels) ;
        m ii in

      let  sem_instr =  SM.build_semantics test in
      let rec add_next_instr re_exec fetch_proc proc env seen addr inst nexts =
        wrap re_exec fetch_proc proc inst addr env sem_instr >>> fun branch ->
          let { A.regs=env; lx_sz=szo; fh_code } = env in
          let env = A.kill_regs (A.killed inst) env
          and szo =
            let open MachSize in
            match A.get_lx_sz inst with
            | No -> szo
            | St -> None
            | Ld sz -> Some sz in
          let env =
            match branch with
            | S.B.Next bds|S.B.Jump (_,bds)|S.B.IndirectJump (_,_,bds)
            | B.Fault bds ->
                List.fold_right
                  (fun (r,v) -> A.set_reg r v)
                  bds env
            | _ -> env in
          next_instr
            re_exec inst fetch_proc proc { A.regs=env; lx_sz=szo; fh_code}
            seen addr nexts branch

      and add_code re_exec fetch_proc proc env seen nexts = match nexts with
      | [] -> EM.unitcodeT true
      | (addr,inst)::nexts ->
          add_next_instr re_exec fetch_proc proc env seen addr inst nexts

      and add_lbl re_exec check_back proc env seen addr_jmp lbl =
        add_tgt re_exec check_back proc env seen addr_jmp (B.Lbl lbl)

      and add_tgt re_exec check_back proc env seen addr_jmp tgt =
        match fetch_code check_back seen proc addr_jmp tgt with
        | No (tgt_proc,(addr,inst)::_) ->
            let m ii =
              EM.addT
                (A.next_po_index ii.A.program_order_index)
                (EM.cutoffT (tgt2lbl tgt) ii (S.B.Next [])) in
            wrap
              re_exec tgt_proc proc inst addr env m >>> fun _ -> EM.unitcodeT true
        | No (_,[]) -> assert false (* Backward jump cannot be to end of code *)
        | Ok ((tgt_proc,code),seen) -> add_code re_exec tgt_proc proc env seen code
        | Segfault addr ->
          let msg = Printf.sprintf
            "Segmentation fault (kidding, address 0x%x does not point to code)"
            addr in
          EM.failcodeT (Misc.UserError msg) true

      and add_fault re_exec inst fetch_proc proc env seen addr nexts =
        match env.A.fh_code,re_exec with
        | Some _, true ->
           let e = "Fault inside a fault handler" in
           EM.warncodeT e true
        | Some fh_code, false ->
           add_code true fetch_proc proc env seen fh_code
        | None, true ->
           EM.unitcodeT false
        | None, false ->
           let open Fault.Handling in
           match C.fault_handling with
           | Fatal -> EM.unitcodeT true
           | Skip -> add_code false fetch_proc proc env seen nexts
           | Handled ->
              add_next_instr true fetch_proc proc env seen addr inst nexts

      and next_instr re_exec inst fetch_proc proc env seen addr nexts b =
        match b with
      | S.B.Exit -> EM.unitcodeT true
      | S.B.Next _ ->
          add_code re_exec fetch_proc proc env seen nexts
      | S.B.Jump (tgt,_) ->
          add_tgt re_exec true proc env seen addr tgt
      | S.B.Fault _ ->
          add_fault re_exec inst fetch_proc proc env seen addr nexts
      | S.B.FaultRet tgt ->
          add_tgt false true proc env seen addr tgt
      | S.B.CondJump (v,tgt) ->
          EM.condJumpT v
            (add_tgt re_exec (not (V.is_var_determined v))
               proc env seen addr tgt)
            (add_code re_exec fetch_proc proc env seen nexts)
      | S.B.IndirectJump (v,lbls,_) ->
         EM.indirectJumpT v lbls
           (add_lbl re_exec true proc env seen addr)
      in

(* Code monad returns a boolean. When false the code must be discarded.
   See also add_instr in eventsMonad.ml *)
      let jump_start proc env code =
        add_code false proc proc env IntMap.empty code in

(* As name suggests, add events of one thread *)
      let add_events_for_a_processor env (proc,code,fh_code) evts =
        let env =
          if A.opt_env then A.build_reg_state proc A.reg_defaults env
          else A.reg_state_empty in
        let () =
          if dbg then
            Printf.eprintf  "Init reg state for proc %s: %s\n%!"
              (Proc.pp proc) (A.pp_reg_state env) in
        let evts_proc =
          jump_start proc { A.regs=env; lx_sz=None; fh_code } code in
        evts_proc |*| evts
      in

(* Initial events, some additional events from caller in madd *)
      let make_inits madd env size_env =
        let module MI = EM.Mixed(C) in
        if C.initwrites then
          MI.initwrites madd env size_env
        else
          EM.zerocodeT
      in

(* Build code monad for one given set of events to add *)
      let set_of_all_instr_events madd =
        List.fold_right
          (add_events_for_a_processor test.Test_herd.init_state)
          starts
          (make_inits madd env0 test.Test_herd.size_env) in

      let transitive_po es =
        let r,e = es.E.po in
        (r,E.EventRel.transitive_closure e) in

      let af0 = (* locations with initial spurious update *)
        if
          match C.dirty with
          | None -> false
          | Some t -> t.DirtyBit.some_ha || t.DirtyBit.some_hd
        then begin (* One spurious update per observed pte (final load) *)
            if C.variant Variant.PhantomOnLoad then
              let look_pt rloc k = match rloc with
                | ConstrGen.Loc (A.Location_global (V.Val c as vloc))
                when Constant.is_pt c -> vloc::k
                | _ -> k in
              A.RLocSet.fold look_pt test.Test_herd.observed []
            else (* One spurious update per variable not accessed initially *)
              let add_setaf0 k (loc,v) =
                match loc with
                | A.Location_global (V.Val c as vloc) ->
                   if Constant.is_pt c then
                     match v with
                     | V.Val (Constant.PteVal p)
                           when not (V.Cst.PteVal.is_af p) ->
                        vloc::k
                     | _ -> k
                   else k
                | _ -> k in
              List.fold_left add_setaf0 [] env0
        end else [] in

      let rec index xs i = match xs with
      | [] ->
          W.warn "%i abstract event structures\n%!" i ;
          []
      | (vcl,es)::xs ->
          let es = if C.debug.Debug_herd.monad then es else relabel es in
          let es =
            { es with E.procs = procs; E.po = if do_deps then transitive_po es else es.E.po } in
          (i,vcl,es)::index xs (i+1) in
      let r =
        Misc.fold_subsets_gen
          (fun vloc -> EM.(|||) (SM.spurious_setaf vloc))
          (EM.unitT ()) af0
          (fun maf0 ->
            EM.get_output (set_of_all_instr_events (EM.(|||) maf0)))
          [] in
      let r = match C.maxphantom with
        | None -> r
        | Some max ->
           let count_spurious es =
             E.EventSet.fold
               (fun e k ->
                 if E.is_load e && E.is_spurious e then k+1 else k)
               es 0 in
           List.filter
             (fun (_,es) -> count_spurious es.E.events <= max)
             r in
      { event_structures=index r 0; overwritable_labels; },test


(*******************)
(* Rfmap generator *)
(*******************)


(* Step 1. make rfmap for registers and reservations *)


let get_loc e = match E.location_of e with
| Some loc -> loc
| None -> assert false

and get_read e = match E.read_of e  with
| Some v -> v
| None -> assert false

and get_written e = match E.written_of e with
| Some v -> v
| None -> assert false




(* Add (local) final edges in rfm, ie for all (register) location, find the last (po+iico) store to it *)

let add_finals es =
    U.LocEnv.fold
      (fun loc stores k ->
        let stores =
          List.filter
            (fun x -> not (E.EventSet.mem x (es.E.speculated))) stores in
      match stores with
      | [] -> k
      | ew::stores ->
          let last =
            List.fold_right
              (fun ew0 ew ->
                if U.is_before_strict es ew0 ew then ew
                else begin
                  (* If writes to a given register by a given thread
                     are not totally ordered, it gets weird to define
                     the last or 'final'register write *)
                  if not (U.is_before_strict es ew ew0) then
                    Warn.fatal
                      "Ambiguous po for register %s" (A.pp_location loc) ;
                  ew0
                end)
              stores ew in
          S.RFMap.add (S.Final loc) (S.Store last) k)

(*******************************)
(* Compute rfmap for registers *)
(*******************************)

let map_loc_find loc m =
  try U.LocEnv.find loc m
  with Not_found -> []

let match_reg_events es =
  let loc_loads = U.collect_reg_loads es
  and loc_stores = U.collect_reg_stores es
  (* Share computation of the iico relation *)
  and is_before_strict =  U.is_before_strict es in

(* For all loads find the right store, the one "just before" the load *)
  let rfm =
    U.LocEnv.fold
      (fun loc loads k ->
        let stores = map_loc_find loc loc_stores in
        List.fold_right
          (fun er k ->
            let rf =
              List.fold_left
                (fun rf ew ->
                  if is_before_strict ew er then
                    match rf with
                    | S.Init -> S.Store ew
                    | S.Store ew0 ->
                        if U.is_before_strict es ew0 ew then
                          S.Store ew
                        else begin
                          (* store order is total *)
                            if not (is_before_strict ew ew0) then begin
                              Printf.eprintf "Not ordered stores %a and %a\n"
                                E.debug_event ew0
                                E.debug_event ew ;
                              assert false
                            end ;
                          rf
                        end
                  else rf)
                S.Init stores in
            S.RFMap.add (S.Load er) rf k)
          loads k)
      loc_loads S.RFMap.empty in
(* Complete with stores to final state *)
  add_finals es loc_stores rfm



    let get_rf_value test read rf = match rf with
    | S.Init ->
        let loc = get_loc read in
        let look_address =
          A.look_address_in_state test.Test_herd.init_state in
        begin
          try look_address loc with A.LocUndetermined -> assert false
        end
    | S.Store e -> get_written e

(* Add a constraint for two values *)

(* Optimization: adding constraint v1 := v2 should always work *)

    exception Contradiction

    let add_eq v1 v2 eqs =
      if V.is_var_determined v1 then
        if V.is_var_determined v2 then
          if V.equal v1 v2 then eqs
          else raise Contradiction
        else (* Here, v1 and v2 necessarily differ *)
          VC.Assign (v2, VC.Atom v1)::eqs
      else if V.equal v1 v2 then eqs
      else VC.Assign (v1, VC.Atom v2)::eqs

    let pp_nosol lvl test es rfm =
      let module PP = Pretty.Make(S) in
      eprintf "No solution at %s level\n%!" lvl;
      PP.show_es_rfm test es rfm ;
      ()

    let solve_regs test es csn =
      let rfm = match_reg_events es in
      let csn =
        S.RFMap.fold
          (fun wt rf csn -> match wt with
          | S.Final _ -> csn
          | S.Load load ->
              let v_loaded = get_read load in
              let v_stored = get_rf_value test load rf in
              try add_eq v_loaded v_stored csn
              with Contradiction ->
                let loc = Misc.as_some (E.location_of load) in
                Printf.eprintf
                  "Contradiction on reg %s: loaded %s vs. stored %s\n"
                  (A.pp_location loc)
                  (A.V.pp_v v_loaded)
                  (A.V.pp_v v_stored) ;
                assert false)
          rfm csn in
      if  C.debug.Debug_herd.solver then
        prerr_endline "++ Solve  registers" ;
      match VC.solve csn with
      | VC.NoSolns ->
         if C.debug.Debug_herd.solver then
           pp_nosol "register" test es rfm ;
         None
      | VC.Maybe (sol,csn) ->
          Some
            (E.simplify_vars_in_event_structure sol es,
             S.simplify_vars_in_rfmap sol rfm,
             csn)

(**************************************)
(* Step 2. Generate rfmap for memory  *)
(**************************************)

    let get_loc_as_value e = match  E.global_loc_of e with
    | None -> eprintf "%a\n" E.debug_event e ; assert false
    | Some v -> v

(* Compatible location are:
   - either both determined and equal,
   - or at least one location is undetermined. *)
    let compatible_locs_mem e1 e2 =
      E.event_compare e1 e2 <> 0 && (* C RMWs cannot feed themselves *)
      E.compatible_accesses e1 e2 &&
      begin
        let loc1 = get_loc e1
        and loc2 = get_loc e2 in
        let ov1 =  A.undetermined_vars_in_loc_opt loc1
        and ov2 =  A.undetermined_vars_in_loc_opt loc2 in
        match ov1,ov2 with
        | None,None -> E.same_location e1 e2
        | (Some _,None)|(None,Some _)
        | (Some _,Some _) -> true
      end

(* Add a constraint for a store/load match *)
    let pp_init load =
      if dbg then
        eprintf "Add eq load=%a, store=Init\n%!"
          E.debug_event load

    let pp_add load store =
      if dbg then
        eprintf "Add eq load=%a, store=%a\n%!"
          E.debug_event load
          E.debug_event store

    let add_mem_eqs test rf load eqs =
      let v_loaded = get_read load in
      match rf with
      | S.Init -> (* Tricky, if location (of load) is
                     not know yet, emit a specific constraint *)
          let state = test.Test_herd.init_state
          and loc_load = get_loc load in
          pp_init load  ;
          begin try
            let v_stored = A.look_address_in_state state loc_load in
            add_eq v_stored  v_loaded eqs
          with A.LocUndetermined ->
            VC.Assign
              (v_loaded, VC.ReadInit (loc_load,state))::eqs
          end
      | S.Store store ->
          pp_add load store ;
          add_eq v_loaded (get_written store)
            (add_eq
               (get_loc_as_value store)
               (get_loc_as_value load) eqs)

(* Our rather loose rfmaps can induce a cycle in
   causality. Check this. *)
    let rfmap_is_cyclic es rfm =
      let iico = E.iico es in
      let causality =
        S.RFMap.fold
          (fun load store k -> match load,store with
          | S.Load er,S.Store ew -> E.EventRel.add (ew,er) k
          | _,_ -> k)
          rfm iico in
      match E.EventRel.get_cycle causality with
      | None -> prerr_endline "no cycle"; false
      | Some cy ->
          if C.debug.Debug_herd.rfm then begin
            let debug_event chan e = fprintf chan "%i" e.E.eiid in
            eprintf "cycle = %a\n" debug_event
              (match cy with e::_ -> e | [] -> assert false)
          end; true

(* solve_mem proper *)


(* refrain from being subtle: match a load with all compatible
   stores, and there may be many *)

(* First consider loads from init, in the initwrite case
   nothing to consider, as the initial stores should present
   as events *)
    let init = if C.initwrites then [] else [S.Init]
    let map_load_init loads =
      E.EventSet.fold
        (fun load k -> (load,init)::k)
        loads []

(*condition:
  soit le load est specule, auquel cas il peut lire de partout;
  soit le load n'est pas specule, auquel cas il ne peut pas lire de stores specules*)

    let check_speculation es store load =
      let spec = es.E.speculated in
      E.EventSet.mem load spec ||
      not (E.EventSet.mem store spec)

    let is_spec es e = E.EventSet.mem e es.E.speculated

(* Consider all stores that may feed a load
   - Compatible location.
   - Not after in program order
    (suppressed when uniproc is not optmised early) *)

    let map_load_possible_stores test es rfm loads stores compat_locs =
      let ok = match C.optace with
        | OptAce.False -> fun _ _ -> true
        | OptAce.True ->
           let pred = U.is_before_strict es
           and iico = U.iico es in
           fun er ew ->
           not
             (E.is_explicit er && E.is_explicit ew && pred er ew
              || E.EventRel.mem (er,ew) iico)
        | OptAce.Iico ->
           let iico = U.iico es in
           fun load store -> not (E.EventRel.mem (load,store) iico) in
      let m =
        E.EventSet.fold
          (fun store map_load ->
            List.map
              (fun ((load,stores) as c) ->
                if
                  compat_locs store load &&
                  check_speculation es store load &&
                  ok load store
                then
                  load,S.Store store::stores
                else c)
              map_load)
          stores (map_load_init loads) in
      if dbg then begin
        let pp_read_froms chan rfs =
          List.iter
            (fun rf -> match rf with
            | S.Init -> fprintf chan "Init"
            | S.Store e -> E.debug_event chan e ; fprintf chan ",")
            rfs in
        List.iter
          (fun (load,stores) ->
            eprintf "Pairing {%a} with {%a}\n"
              E.debug_event load
              pp_read_froms stores)
          m
      end ;
(* Check for loads that cannot feed on some write *)
      if not do_deps && not asl then begin
        List.iter
          (fun (load,stores) ->
            match stores with
            | [] ->
                begin match E.location_of load with
                | Some loc ->
                    begin match A.symbol loc with
                    | Some sym ->
                        if S.is_non_mixed_symbol test sym then
                          Warn.fatal
                            "read on location %s does not match any write"
                        (A.pp_location loc)
                        else if check_mixed then
                          Warn.user_error
                            "mixed-size test rejected (symbol %s), consider option -variant mixed"
                            (A.pp_location loc)
                    | None ->
                       if dbg then begin
                        let module PP = Pretty.Make(S) in
                        eprintf
                          "Failed to find at least one write for load %a\n%!"
                          E.debug_event load ;
                        PP.show_es_rfm test es rfm
                       end ;
                       Warn.fatal
                         "Non symbolic location with no initial write: '%s'\n"
                         (A.pp_location loc)
                    end
                | _ -> assert false
                end
            | _::_ -> ())
          m
        end ;
      m

(* Add memory events to rfmap *)
    let add_mem =
      List.fold_right2
        (fun er rf -> S.RFMap.add (S.Load er) rf)

    let add_some_mem =
      List.fold_right2
        (fun er rf ->  match rf with
        | None -> fun rfm -> rfm
        | Some rf -> S.RFMap.add (S.Load er) rf)


    let add_mems =
      List.fold_right2
        (List.fold_right2 (fun r w ->  S.RFMap.add (S.Load r) (S.Store w)))

    let solve_mem_or_res test es rfm cns kont res loads stores compat_locs add_eqs =
      let possible =
        map_load_possible_stores test es rfm loads stores compat_locs in
      let possible =
        List.map
          (fun (er,ws) ->
            let ws = List.map (fun w -> Some w) ws in
            (* Add reading from nowhere for speculated reads *)
            let ws = if is_spec es er then None::ws else ws in
            er,ws)
          possible in
      let loads,possible_stores =  List.split possible in
      (* Cross product fold. Probably an overkill here *)
      Misc.fold_cross possible_stores
        (fun stores res ->
          (* stores is a list of stores that may match the loads list.
             Both lists in same order [by List.split above]. *)
          try
            (* Add constraints now *)
            if dbg then eprintf "Add equations\n" ;
            let cns =
              List.fold_right2
                (fun load rf k -> match rf with
                | None -> k (* No write, no equation *)
                | Some rf -> add_eqs test rf load k)
                loads stores cns in
            if dbg then eprintf "\n%!" ;
            (* And solve *)
            if C.debug.Debug_herd.solver then
              prerr_endline "++ Solve memory" ;
            match VC.solve cns with
            | VC.NoSolns ->
               if C.debug.Debug_herd.solver then begin
                 let rfm = add_some_mem loads stores rfm in
                 pp_nosol "memory" test es rfm
               end ;
               res
            | VC.Maybe (sol,cs) ->
                (* Time to complete rfmap *)
                let rfm = add_some_mem loads stores rfm in
                (* And to make everything concrete *)
                let es = E.simplify_vars_in_event_structure sol es
                and rfm = S.simplify_vars_in_rfmap sol rfm in
                kont es rfm cs res
          with
          | Contradiction ->  (* May  be raised by add_mem_eqs *)
             if C.debug.Debug_herd.solver then
               begin
                 let rfm = add_some_mem loads stores rfm in
                 pp_nosol "memory" test es rfm
               end ;
             res
          | e ->
              if C.debug.Debug_herd.top then begin
                eprintf "Exception: %s\n%!" (Printexc.to_string e) ;
                let module PP = Pretty.Make(S) in
                let rfm = add_some_mem loads stores rfm in
                PP.show_es_rfm test es rfm
              end ;
              raise e
        )
        res

    let when_unsolved test es rfm _cs res =
      (* This system in fact has no solution.
         In other words, it is not possible to make
         such event structures concrete.
         This occurs with cyclic rfmaps *)
      if C.debug.Debug_herd.solver then begin
          let module PP = Pretty.Make(S) in
          prerr_endline "Unsolvable system" ;
          PP.show_es_rfm test es rfm ;
        end ;
      assert (true || rfmap_is_cyclic es rfm);
      res

    let solve_mem_non_mixed test es rfm cns kont res =
      let compat_locs = compatible_locs_mem in
      if self then
        let code_store e =
        E.is_store e &&
        match
          Misc.seq_opt A.global (E.location_of e)
        with
        | Some (V.Val (Constant.Label _)|V.Var _) -> true
        | Some _|None -> false in
        (* Select code accesses *)
        let code_loads =
          E.EventSet.filter E.is_ifetch es.E.events
        and code_stores =
          E.EventSet.filter code_store es.E.events in
        let kont es rfm cns res =
          (* We get here once code accesses are solved *)
          let loads =  E.EventSet.filter E.is_mem_load es.E.events
          and stores = E.EventSet.filter E.is_mem_store es.E.events in
          let loads =
            (* Remove code loads that are now solved *)
            E.EventSet.diff loads code_loads in
          if dbg then begin
            eprintf "Left loads : %a\n"E.debug_events loads ;
            eprintf "All stores: %a\n"E.debug_events stores
          end ;
          solve_mem_or_res test es rfm cns kont res
            loads stores compat_locs add_mem_eqs in
        if dbg then begin
            eprintf "Code loads : %a\n"E.debug_events code_loads ;
            eprintf "Code stores: %a\n"E.debug_events code_stores
          end ;
        solve_mem_or_res test es rfm cns kont res
          code_loads code_stores compat_locs add_mem_eqs
      else
        let loads = E.EventSet.filter E.is_mem_load es.E.events
        and stores = E.EventSet.filter E.is_mem_store es.E.events in
        if dbg then begin
          eprintf "Loads : %a\n"E.debug_events loads ;
          eprintf "Stores: %a\n"E.debug_events stores
          end ;
        solve_mem_or_res test es rfm cns kont res
          loads stores compat_locs add_mem_eqs

(*************************************)
(* Mixed-size write-to-load matching *)
(*************************************)

    exception CannotSca

(* Various utilities on symbolic addresses as locations *)
    (* Absolute base of indexed symbol (i.e. array address) *)
    let get_base a =
      let open Constant in
      match A.symbolic_data a with
      | Some ({name=s;_} as sym) ->
          let s = if Misc.check_ctag s then Misc.tr_ctag s else s in
          A.of_symbolic_data {sym with name=s; offset=0;}
      | _ -> raise CannotSca

(* Sort same_base *)
    let compare_index e1 e2 =
      let open Constant in
      let loc1 = E.location_of e1 and loc2 = E.location_of e2 in
      match Misc.seq_opt A.symbolic_data loc1,
            Misc.seq_opt A.symbolic_data loc2
      with
      | Some {name=s1;offset=i1;_},Some {name=s2;offset=i2;_}
            when  Misc.string_eq s1 s2 ->
          Misc.int_compare i1 i2
      | Some {name=s1;_},Some {name=s2;_} when morello ->
          if Misc.check_ctag s1 && Misc.string_eq (Misc.tr_ctag s1) s2 then 1
          else if Misc.check_ctag s2 && Misc.string_eq s1 (Misc.tr_ctag s2) then -1
          else if Misc.check_ctag s1 && Misc.check_ctag s2 && Misc.string_eq s1 s2 then 0
          else raise CannotSca
      | _,_ -> raise CannotSca

    let sort_same_base es = List.sort compare_index es

    let debug_events out es = Misc.pp_list out " " E.debug_event es

    module Match
        (R:sig
          type read
          val compare_index : read -> S.event -> int
          val debug_read : out_channel -> read -> unit
        end) = struct

          let debug_reads out es = Misc.pp_list out " " R.debug_read es

          let rec inter rs0 ws0 = match rs0 with
          | [] -> [],[]
          | r::rs -> begin match ws0 with
            | [] -> rs0,[]
            | w::ws ->
                let c = R.compare_index r w in
                if c < 0 then
                  let rs,ws = inter rs ws0 in
                  r::rs,ws
                else if c > 0 then
                  let rs,ws = inter rs0 ws in
                  rs,ws
                else
                  let rs,ws = inter rs ws in
                  rs,w::ws
          end

          let rec all_ws rs ws wss =
            if dbg then
              eprintf "Trying [%a] on [%a]\n"
                debug_reads rs debug_events ws ;
            let rs_diff,ws_inter = inter rs ws in
            if dbg then
              eprintf "Found [%a] (remains [%a])\n"
                debug_events ws_inter debug_reads rs_diff ;
            match ws_inter with
            | [] -> next_all_ws rs wss
            | _  ->
                List.fold_right
                  (fun ws k -> (ws_inter@ws)::k)
                  (next_all_ws rs_diff wss)
                  (next_all_ws rs wss)

          and next_all_ws rs wss = match rs with
          | [] -> [[]]
          | _  ->
              begin match wss with
              | [] -> []
              | ws::wss ->  all_ws rs ws wss
              end

          let find_rfs_sca s rs wss = match next_all_ws rs wss with
          | _::_ as wss -> List.map sort_same_base wss
          | [] -> begin match rs with
            | [] -> assert false
            | _::_ -> Warn.user_error "out-of-bound access on %s" s
          end
        end

    module MatchRf =
      Match
        (struct
          type read = S.event
          let compare_index = compare_index
          let debug_read = E.debug_event
        end)

    let byte_sz = MachSize.nbytes C.byte

    let expose_sca es sca =
      let open Constant in
      let sca = E.EventSet.elements sca in
      let sca = sort_same_base sca in
      let fst = match sca with
      | e::_ -> e
      | [] -> assert false in
      let s,idx= match  E.global_loc_of fst with
      |  Some (V.Val (Symbolic (Virtual {name=s; offset=i;_})))
         ->
           (if morello && Misc.check_ctag s then Misc.tr_ctag s else s),i
      | _ -> raise CannotSca in
      let sz = List.length sca*byte_sz in
      is_spec es fst,E.get_mem_dir fst,s,idx,sz,sca

    let expose_scas es =
      let scas = es.E.sca in
      let ms =
        E.EventSetSet.fold
          (fun sca k -> expose_sca es sca::k)
          scas [] in
      let rs,ws =
        List.fold_left
          (fun (rs,ws) (g,d,x,idx,sz,es) -> match d with
          | Dir.W ->
              let old = StringMap.safe_find [] x ws in
              rs,StringMap.add x ((g,idx,sz,es)::old) ws
          | Dir.R -> (g,x,idx,sz,es)::rs,ws)
          ([],StringMap.empty) ms in
      let ws =
        StringMap.map
          (List.sort (fun (_,_,sz1,_) (_,_,sz2,_) -> Misc.int_compare sz1 sz2))
          ws in
      let ms =
        List.map
          (fun (gr,x,i,sz,rs) ->
            let ws = try StringMap.find x ws with Not_found -> assert false in (* Because of init writes *)
            let ws =
              List.filter
                (fun (gw,i_w,sz_w,_) ->
                  not (not gr && gw) &&
                  (* non-ghost reads cannot read from ghost writes *)
                  i+sz >= i_w && i < i_w+sz_w
                    (* write and read intersects *))
                ws in
            x,rs,List.map (fun (_,_,_,ws) -> ws) ws)
          rs in
      let ms =
        List.map
          (fun (x,rs,wss) -> rs,MatchRf.find_rfs_sca x rs wss)
          ms in
      if C.debug.Debug_herd.solver || C.debug.Debug_herd.mem then begin
        eprintf "+++++++++++++++++++++++\n" ;
        List.iter
          (fun (rs,wss) -> eprintf "[%a] ->\n" debug_events rs ;
            List.iter
              (fun ws ->  eprintf "    [%a]\n" debug_events ws)
              wss)
          ms ;
        flush stderr
      end ;
      ms

(* Non-mixed pairing for tags, if any *)
    let pair_tags test es rfm =
      let tags = E.EventSet.filter E.is_tag es.E.events in
      let loads = E.EventSet.filter E.is_load tags
      and stores = E.EventSet.filter E.is_store tags in
      let m =
        map_load_possible_stores test es rfm loads stores compatible_locs_mem in
      m

    let solve_mem_mixed test es rfm cns kont res =
      let match_tags = if morello then []
        else pair_tags test es rfm in
      let tag_loads,tag_possible_stores = List.split match_tags in
      let ms = expose_scas es in
      let rss,wsss = List.split ms in
      (* Cross product fold. Probably an overkill here *)
      Misc.fold_cross wsss
        (fun wss res ->
          (* Add memory constraints now *)
          try
            let cns =
              List.fold_right2
                (fun rs ws eqs ->
                  List.fold_right2
                    (fun r w eqs ->
                      assert (E.same_location r w) ;
                      add_eq (get_read r) (get_written w) eqs)
                    rs ws eqs)
                rss wss cns in
            Misc.fold_cross tag_possible_stores
              (fun tag_stores res ->
                (* Add tag memory constraints *)
                try
                  let cns =
                    List.fold_right2
                      (fun load store k -> add_mem_eqs test store load k)
                      tag_loads tag_stores cns in
                  (* And solve *)
                  match VC.solve cns with
                  | VC.NoSolns -> res
                  | VC.Maybe (sol,cs) ->
                      (* Time to complete rfmap *)
                      let rfm = add_mems rss wss rfm in
                      let rfm = add_mem tag_loads tag_stores rfm in
                      (* And to make everything concrete *)
                      let es = E.simplify_vars_in_event_structure sol es
                      and rfm = S.simplify_vars_in_rfmap sol rfm in
                      kont es rfm cs res
                with
                | Contradiction -> res  (* can be raised by add_mem_eqs *)
                | e ->
                    if C.debug.Debug_herd.top then begin
                      eprintf "Exception: %s\n%!" (Printexc.to_string e) ;
                      let module PP = Pretty.Make(S) in
                      let rfm = add_mems rss wss rfm in
                      PP.show_es_rfm test es rfm
                    end ;
                    raise e)
              res
          with Contradiction -> res)   (* can be raised by add_eq *)
        res

    let solve_mem test es rfm cns kont res =
      try
        if mixed && not C.debug.Debug_herd.mixed then solve_mem_mixed test es rfm cns kont res
        else solve_mem_non_mixed  test es rfm cns kont res
      with
      | CannotSca ->
         solve_mem_non_mixed test es rfm cns kont res


(*************************************)
(* Final condition invalidation mode *)
(*************************************)

    module CM = S.Cons.Mixed(C)

(* Internal filter *)
    let check_filter test fsc = match test.Test_herd.filter with
    | None -> true
    | Some p ->
        not C.check_filter ||
          CM.check_prop p (S.type_env test) (S.size_env test) fsc

(*************************************)
(* Final condition invalidation mode *)
(*************************************)

(*
  A little optimisation: we check whether the existence/non-existence
  of some vo would help in validation/invalidating the constraint
  of the test.

  If no, not need to go on
 *)

    module T = Test_herd.Make(S.A)

    let final_is_relevant test fsc =
      let open ConstrGen in
      let cnstr = T.find_our_constraint test in
      let senv = S.size_env test
      and tenv = S.type_env test in
      let check_prop p = CM.check_prop p tenv senv fsc in
      match cnstr with
        (* Looking for 'Allow' witness *)
      | NotExistsState p | ExistsState p -> check_prop p
            (* Looking for witness that invalidates 'Require' *)
      | ForallStates p -> not (check_prop p)
            (* Looking for witness that invalidates 'Forbid' *)


    let worth_going test fsc = match C.speedcheck with
    | Speed.True|Speed.Fast -> final_is_relevant test fsc
    | Speed.False -> true

(***************************)
(* Rfmap full exploitation *)
(***************************)

(* final state *)
    let tr_physical =
      let open Constant in
      if kvm then
        (function
         | A.Location_global (V.Val (Symbolic (Physical (s,idx)))) ->
             let sym = { default_symbolic_data with name=s; offset=idx; } in
             A.of_symbolic_data sym
         | A.Location_global (V.Val (Symbolic (TagAddr (PHY,s,o)))) ->
             A.Location_global (V.Val (Symbolic (TagAddr (VIR,s,o))))
         | loc -> loc)
      else
        Misc.identity

    let compute_final_state test rfm es =
      let st =
        S.RFMap.fold
          (fun wt rf k -> match wt,rf with
          | S.Final loc,S.Store ew ->
              A.state_add k (tr_physical loc) (get_written ew)
          | _,_ -> k)
          rfm test.Test_herd.init_state in
      st,
      if A.FaultAtomSet.is_empty test.Test_herd.ffaults && not !Opts.dumpallfaults then
        A.FaultSet.empty
      else
        E.EventSet.fold
          (fun e k ->
            match E.to_fault e with
            | Some f -> A.FaultSet.add f k
            | None -> k)
          es A.FaultSet.empty


(* View before relations easily available, from po_iico and rfmap *)


(* Preserved Program Order, per memory location - same processor *)
    let make_ppoloc po_iico_data es =
      let mem_evts = E.mem_of es in
      E.EventRel.of_pred mem_evts mem_evts
        (fun e1 e2 ->
          E.same_location e1 e2 &&
          E.EventRel.mem (e1,e2) po_iico_data)

(* Store is before rfm load successor *)
    let store_load rfm =
      S.RFMap.fold
        (fun wt rf k -> match wt,rf with
        | S.Load er,S.Store ew -> E.EventRel.add (ew,er) k
        | _,_ -> k)
        rfm E.EventRel.empty

(* Load from init is before all stores *)
    let init_load es rfm =
      let loc_stores = U.collect_stores es in
      S.RFMap.fold
        (fun wt rf k -> match wt,rf with
        | S.Load er,S.Init ->
            List.fold_left
              (fun k ew ->
                E.EventRel.add (er,ew) k)
              k (map_loc_find (get_loc er) loc_stores)
        | _,_ -> k)
        rfm E.EventRel.empty

(* Reconstruct load/store atomic pairs *)

    let make_atomic_load_store es =
      let all = E.atomics_of es.E.events in
      let atms = U.collect_atomics es in
      U.LocEnv.fold
        (fun _loc atms k ->
          let atms =
            List.filter
              (fun e -> not (E.is_load e && E.is_store e))
              atms in (* get rid of C RMW *)
          let rs,ws = List.partition E.is_load atms in
          List.fold_left
            (fun k r ->
              let exp = E.is_explicit r in
              List.fold_left
                (fun k w ->
                  if
                    S.atomic_pair_allowed r w &&
                    U.is_before_strict es r w &&
                    E.is_explicit w = exp &&
                    not
                      (E.EventSet.exists
                         (fun e ->
                           E.is_explicit e = exp &&
                           U.is_before_strict es r e &&
                           U.is_before_strict es e w)
                         all)
                  then E.EventRel.add (r,w) k
                  else k)
                k ws)
            k rs)
        atms E.EventRel.empty


(* Retrieve last store from rfmap *)
    let get_max_store _test _es rfm loc =
      try match S.RFMap.find (S.Final loc) rfm with
      | S.Store ew -> Some ew
      | S.Init -> None       (* means no store to loc *)
      with Not_found -> None
(*
  let module PP = Pretty.Make(S) in
  eprintf "Uncomplete rfmap: %s\n%!" (A.pp_location loc) ;
  PP.show_es_rfm test es rfm ;
  assert false
 *)
(* Store to final state comes last *)
    let last_store test es rfm =
      let loc_stores = U.collect_stores_non_spec es
      and loc_loads = U.collect_loads_non_spec es in
      U.LocEnv.fold
        (fun loc ws k ->
          match get_max_store test es rfm loc with
          | None -> k
          | Some max ->
              let loads = map_loc_find loc loc_loads in
              let k =
                List.fold_left
                  (fun k er ->
                    if E.event_equal er max then k (* possible with RMW *)
                    else match S.RFMap.find (S.Load er) rfm with
                    | S.Init -> E.EventRel.add (er,max) k
                    | S.Store my_ew ->
                        if E.event_equal my_ew max then k
                        else E.EventRel.add (er,max) k)
                  k loads in
              List.fold_left
                (fun k ew ->
                  if E.event_equal ew max then k
                  else E.EventRel.add (ew,max) k)
                k ws)
        loc_stores E.EventRel.empty

    let keep_observed_loc =
      if kvm then
        let open Constant in
        fun loc -> match loc with
        | A.Location_global (V.Val (Symbolic (Physical _|TagAddr (PHY, _, _) as sym1))) ->
            let p oloc = match oloc with
            | A.Location_global (V.Val (Symbolic sym2)) ->
                Constant.virt_match_phy sym2 sym1
            | _ -> false in
            A.LocSet.exists p
        | _ -> A.LocSet.mem loc
      else A.LocSet.mem

    let pp_locations = A.LocSet.pp_str " " A.pp_location

    let all_finals_non_mixed test es =
      let loc_stores = U.remove_spec_from_map es (U.collect_mem_stores es) in
      let loc_stores =
        if C.observed_finals_only then
          let observed_locs =
            let locs = S.observed_locations test in
            if mixed then
              let senv = S.size_env test in
              A.LocSet.map_union
                (fun loc ->
                  let open Constant in
                  match loc with
                  | A.Location_global
                    (V.Val (Symbolic (Virtual {name=s;_})) as a)
                    ->
                      let eas = AM.byte_eas (A.look_size senv s) a in
                      A.LocSet.of_list
                        (List.map (fun a -> A.Location_global a) eas)
                  | _ -> A.LocSet.singleton loc)
                locs
            else if morello then
              A.LocSet.map_union
                (fun loc ->
                  let open Constant in
                  match loc with
                  | A.Location_global
                    (A.V.Val
                       (Symbolic
                          (Virtual ({name=s; offset=0; _} as sym))))
                        ->
                        A.LocSet.add
                          (A.of_symbolic_data {sym with name=Misc.add_ctag s})
                          (A.LocSet.singleton loc)
                    | _ -> A.LocSet.singleton loc)
                locs
            else locs in
          if C.debug.Debug_herd.mem then begin
            eprintf "Observed locs: {%s}\n" (pp_locations observed_locs)
          end ;
          U.LocEnv.fold
            (fun loc ws k ->
              if keep_observed_loc loc observed_locs then
                U.LocEnv.add loc ws k
              else k)
            loc_stores U.LocEnv.empty
        else loc_stores in

      let possible_finals =
        match C.optace with
        | OptAce.True ->
           U.LocEnv.fold
             (fun _loc ws k ->
               List.filter
                 (fun w ->
                   not (E.is_explicit w) ||
                   not
                     (List.exists
                        (fun w' ->
                          E.is_explicit w' && U.is_before_strict es w w') ws))
                 ws::k)
             loc_stores []
        | OptAce.False|OptAce.Iico ->
           U.LocEnv.fold (fun _loc ws k -> ws::k) loc_stores [] in
      if C.debug.Debug_herd.solver && Misc.consp possible_finals then begin
        eprintf "+++++++++ possible finals ++++++++++++++\n" ;
        List.iter
          (fun ws ->  eprintf "[%a]\n" debug_events ws)
          possible_finals ;
        flush stderr
      end ;
      List.map (fun ws -> List.map (fun w -> [w]) ws) (possible_finals)


    let rec compare_len xs ys = match xs,ys with
    | [],[] -> 0
    | [],_::_ -> -1
    | _::_,[] -> 1
    | _::xs,_::ys -> compare_len xs ys

    module MatchFinal =
      Match
        (struct

          type read = int

          let compare_index idx e =
            let open Constant in
            match Misc.seq_opt A.symbolic_data (E.location_of e) with
            | Some {name=s; offset=i; _} ->
                if Misc.check_ctag s then  Misc.int_compare idx max_int (* always -1 ??? *)
                else  Misc.int_compare idx i
            | _ -> assert false

          let debug_read out = fprintf out "%i"
        end)


    let all_finals_mixed test es =
      assert  C.observed_finals_only ;
      let locs = S.observed_locations test in
      let locs =  A.LocSet.filter A.is_global locs in
      let loc_wss =
        E.EventSetSet.fold
          (fun sca k ->
            let e = E.EventSet.choose sca in
            if E.is_store e && not (E.EventSet.mem e es.E.speculated) then match E.location_of e with
            | Some a ->
                let a0 = get_base a in
                let t = A.look_type (S.type_env test) a0 in
                let a =
                  match t with
                  | TestType.TyArray _ -> raise CannotSca
                  | _ -> a0 in
                if keep_observed_loc a locs then
                  let old = A.LocMap.safe_find [] a k in
                  A.LocMap.add a (sort_same_base (E.EventSet.elements sca)::old) k
                else k
            | _ -> assert false (* Only globals in sca *)
            else k)
          es.E.sca A.LocMap.empty in
      let wsss =
        A.LocMap.fold
          (fun loc wss k ->
            let wss = List.sort compare_len (List.map sort_same_base wss)
            and rs =
              let senv = S.size_env test
              and o = Misc.as_some (A.offset loc) in
              AM.byte_indices o (A.look_size_location senv loc) in
            let rs = if morello then rs@[max_int] else rs in
            MatchFinal.find_rfs_sca (A.pp_location loc) rs wss::k)
          loc_wss [] in

      if C.debug.Debug_herd.solver && Misc.consp wsss then begin
        eprintf "+++++++++ possible finals ++++++++++++++\n" ;
        List.iter
          (fun wss ->
            List.iter
              (fun ws ->  eprintf "[%a]\n" debug_events ws)
              wss ;
            eprintf "--------------\n")
          wsss ;
        flush stderr
      end ;
      wsss

    let fold_left_left f = List.fold_left (List.fold_left f)

    let all_finals test es =
      try
        if mixed && not C.debug.Debug_herd.mixed then
          all_finals_mixed test es
        else
          all_finals_non_mixed test es
      with CannotSca ->
        all_finals_non_mixed test es

    let some_same_rf_rmw rfm rmw =
      let loads = U.partition_events (E.EventRel.domain rmw) in
      List.exists
        (fun ers ->
          let rfs =
            E.EventSet.fold
              (fun er k ->
                try S.RFMap.find (S.Load er) rfm::k
                with Not_found -> assert false)
            ers [] in
          Misc.exists_pair S.read_from_equal rfs)
        loads

    let fold_mem_finals test es rfm ofail atomic_load_store kont res =
      (* We can build those now *)
      let evts = es.E.events in
      let po_iico = U.po_iico es in
      let partial_po = E.EventTransRel.to_implicitely_transitive_rel es.E.partial_po in
      let ppoloc = make_ppoloc po_iico evts in
      let store_load_vbf = store_load rfm
      and init_load_vbf = init_load es rfm in
(* Now generate final stores *)
      let possible_finals = all_finals test es in
      if C.debug.Debug_herd.mem then begin
        eprintf "Possible finals:\n" ;
        List.iter
          (fun wss ->
            (List.iter
               (fun ws ->
                 List.iter (eprintf " %a" E.debug_event) ws)
               wss ;
             eprintf "\n"))
          possible_finals
      end ;
(* Add final loads from init for all locations, cleaner *)
      let loc_stores = U.collect_stores es
      and loc_loads = U.collect_loads es in
      let rfm =
        U.LocEnv.fold
          (fun loc _rs k ->
            try
              ignore (U.LocEnv.find loc loc_stores) ;
              k
            with Not_found -> S.RFMap.add (S.Final loc) S.Init k)
          loc_loads rfm in
      try
        let pco0 =
          if C.initwrites then U.compute_pco_init es
          else E.EventRel.empty in
        (*jade: looks ok even in specul case: writes from init are before all
          other writes, including speculated writes*)
        let pco =
          match C.optace with
          | OptAce.False|OptAce.Iico -> pco0
          | OptAce.True ->
            (*jade: looks compatible with speculation, but there might be some
              unforeseen subtlety here so flagging it to be sure*)
             let ppoloc =
               E.EventRel.restrict_rel
                 (fun e1 e2 -> E.is_explicit e1 && E.is_explicit e2)
                 ppoloc in
               match U.compute_pco rfm ppoloc with
               | None -> raise Exit
               | Some pco -> E.EventRel.union pco0 pco in
(* Cross product *)
        Misc.fold_cross
          possible_finals
          (fun ws res ->
            if C.debug.Debug_herd.mem then begin
              eprintf "Finals:" ;
              List.iter
                (fun ws ->
                  List.iter
                    (fun e -> eprintf " %a"  E.debug_event e) ws)
                ws ;
              eprintf "\n";
            end ;

            let rfm =
              fold_left_left
                (fun k w ->
                  S.RFMap.add (S.Final (get_loc w)) (S.Store w) k)
                rfm ws in
            let fsc = compute_final_state test rfm es.E.events in
            if check_filter test fsc && worth_going test fsc then begin
              if C.debug.Debug_herd.solver then begin
                let module PP = Pretty.Make(S) in
                let fsc,_ = fsc in eprintf "Final rfmap, final state=%s\n%!" (S.A.dump_state fsc);
                PP.show_es_rfm test es rfm ;
              end ;
              let last_store_vbf = last_store test es rfm in
              let pco =
                E.EventRel.union pco
                  (U.restrict_to_mem_stores last_store_vbf) in
              if E.EventRel.is_acyclic pco then
                let conc =
                  {
                   S.str = es ;
                   rfmap = rfm ;
                   fs = fsc ;
                   po = po_iico ;
                   partial_po = partial_po;
                   pos = ppoloc ;
                   pco = pco ;

                   store_load_vbf = store_load_vbf ;
                   init_load_vbf = init_load_vbf ;
                   last_store_vbf = last_store_vbf ;
                   atomic_load_store = atomic_load_store ;
                 } in
                kont conc ofail res
              else begin
                if C.debug.Debug_herd.solver then begin
                  let conc =
                    {
                     S.str = es ;
                     rfmap = rfm ;
                     fs = fsc ;
                     po = po_iico ;
                     partial_po = partial_po ;
                     pos = ppoloc ;
                     pco = pco ;

                     store_load_vbf = store_load_vbf ;
                     init_load_vbf = init_load_vbf ;
                     last_store_vbf = last_store_vbf ;
                     atomic_load_store = atomic_load_store ;
                   } in
                  let module PP = Pretty.Make(S) in
                  eprintf "PCO is cyclic, discarding candidate\n%!" ;
                  PP.show_legend test "PCO is cyclic" conc [("last_store_vbf",last_store_vbf); ("pco",pco);];
                end ;
                res
              end
            end else res)
          res
      with Exit -> res


(* Initial check of rfmap validity: no intervening writes.
   Limited to memory, since  generated rfmaps are correct for registers *)
(* NOTE: this is more like an optimization,
   models should rule out those anyway *)

    let check_rfmap es rfm =
      let po_iico = U.is_before_strict es in
      S.for_all_in_rfmap
        (fun wt rf -> match wt with
        | S.Load er when E.is_mem_load er && E.is_explicit er ->
            begin match rf with
            | S.Store ew ->
                not (E.is_explicit ew) ||
                begin
                  assert (not (po_iico er ew)) ;
                (* ok by construction, in theory *)
                  not
                    (E.EventSet.exists
                       (fun e ->
                         E.is_store e && E.same_location e ew &&
                         E.is_explicit e && po_iico ew e &&
                         po_iico e er)
                       es.E.events)
                end
            | S.Init ->
                not
                  (E.EventSet.exists
                     (fun e ->
                       E.is_store e && E.same_location e er &&
                       E.is_explicit e && po_iico e er)
                     es.E.events)
            end
        | _ -> true)
        rfm

    let check_sizes test es =
      if check_mixed then begin
        (* No need to check initial writes, correct by construction. *)
        let loc_mems = U.collect_mem_non_init es in
        U.LocEnv.iter
          (fun loc evts ->
            let open Constant in
            begin match loc with
            | A.Location_global (V.Val (Symbolic sym))
                  when not (S.is_non_mixed_symbol test sym) ->
                Warn.user_error "mixed-size test rejected (symbol %s), consider option -variant mixed"
                  (A.pp_location loc)
            | _ -> ()
            end ;
            begin match evts with
            | [] -> ()
            | e0::es ->
                let sz0 = E.get_mem_size e0 in
                List.iter
                  (fun e ->
                    let sz =  E.get_mem_size e in
                    if sz0 <> sz then begin
                      Printf.eprintf
                        "Size mismatch %a vs. %a, ie %s vs. %s\n"
                        E.debug_event e0
                        E.debug_event e
                        (MachSize.pp sz0) (MachSize.pp sz);
                      Warn.user_error "Illegal mixed-size test"
                    end)
                  es
            end)
          loc_mems
        end

     let check_event_aligned test e =
       let a = Misc.as_some (E.global_loc_of e) in
       if not (U.is_aligned (S.type_env test) (S.size_env test) e) then begin
         if dbg then eprintf "UNALIGNED: %s\n" (E.pp_action e);
         Warn.user_error "Unaligned or out-of-bound access: %s, %d bytes"
           (A.V.pp_v a) (E.get_mem_size e |> MachSize.nbytes)
       end

(* Check alignement in the mixed-size case.
   Check is performed on original memory accesses,
   not on splitted sub-events. Checking sub-events would
   be too permissive, as easily shown by splitting accesses
   into byte accesses. *)
    let check_aligned test es =
      E.EventSet.iter
        (fun e -> check_event_aligned test e)
        es.E.mem_accesses

    let check_symbolic_locations _test es =
      E.EventSet.iter
        (fun e -> match E.location_of e with
        | Some (A.Location_global (V.Val cst)) when
            Constant.is_symbol cst ||
            Constant.is_label cst
            -> ()
        | Some (A.Location_global (V.Var _))
            -> ()
        | Some loc ->
            Warn.user_error "Non-symbolic memory access found on '%s'"
              (A.pp_location loc)
        | None -> assert false)
        (E.mem_of es.E.events)

      let check_noifetch_limitations es =
        let non_init_stores = E.EventSet.filter
          (fun e -> E.is_mem_store e && not (E.is_mem_store_init e))
          es.E.events in
        E.EventSet.iter (fun e ->
          match E.location_of e with
          | Some (A.Location_global (V.Val(Constant.Label(p, lbl)))) ->
             Warn.user_error
               "Store to %s:%s requires instruction fetch functionality.\n\
Please use `-variant self` as an argument to herd7 to enable it."
              (Proc.pp p) (Label.pp lbl)
          | _ -> ()
        ) non_init_stores

    let check_ifetch_limitations test es owls =
      let stores = E.EventSet.filter E.is_mem_store es.E.events in
      let program = test.Test_herd.program
      and code_segment = test.Test_herd.code_segment in
      E.EventSet.iter (fun e ->
        match E.location_of e with
        | Some (A.Location_global (V.Val(Constant.Label(p, lbl))) as loc) ->
          if Label.Set.mem lbl owls then begin
            if false then (* insert a proper test here *)
              Warn.user_error "Illegal store to '%s'; overwrite with the given argument not supported"
              (A.pp_location loc)
          end else begin
            if not (E.is_mem_store_init e) then begin
              try
                match IntMap.find (Label.Map.find lbl program) code_segment with
                | (_,[]) ->
                   Warn.user_error
                     "Final label %s cannot be overwritten"
                     (Label.pp lbl)
                | (_,(_,i)::_) ->
                   Warn.user_error
                     "Instruction %s:%s cannot be overwritten"
                     (Label.pp lbl)
                     (A.dump_instruction i)
              with
              | Not_found ->
                 Warn.user_error
                   "Label %s not found on %s, yet it is used as constant"
                   (Label.pp lbl) (Proc.pp p)
              end
            end
        | _ ->
          ()
      ) stores

    let calculate_rf_with_cnstrnts test owls es cs kont res =
      match solve_regs test es cs with
      | None -> res
      | Some (es,rfm,cs) ->
          if C.debug.Debug_herd.solver && C.verbose > 0 then begin
            let module PP = Pretty.Make(S) in
            prerr_endline "Reg solved" ;
            PP.show_es_rfm test es rfm ;
          end ;
          solve_mem test es rfm cs
            (fun es rfm cs res ->
              let ofail = VC.get_failed cs in
              match cs with
              | _::_
                   when
                     (not oota)
                     && (not C.initwrites || not do_deps)
                     && not asl
                     && Misc.is_none ofail
                ->
(*
 Jade:
  on tolere qu'il reste des equations dans le cas d'evts specules -
  mais il faudrait sans doute le preciser dans la clause when ci-dessus.
 Luc:
   Done, or at least avoid accepting such candidates in non-deps mode.
   Namely, having  non-sensical candidates rejected later by model
   entails a tremendous runtime penalty. *)
                  when_unsolved test es rfm cs res
              | _ ->
                  check_symbolic_locations test es ;
                  if self then check_ifetch_limitations test es owls
                  else check_noifetch_limitations es;
                  if (mixed && not unaligned) then check_aligned test es ;
                  if A.reject_mixed
                     && not (mixed || memtag || morello)
                  then
                    check_sizes test es ;
                  if C.debug.Debug_herd.solver && C.verbose > 0 then begin
                    let module PP = Pretty.Make(S) in
                    prerr_endline "Mem solved" ;
                    PP.show_es_rfm test es rfm
                  end ;
                  if
                    match C.optace with
                    | OptAce.False|OptAce.Iico -> true
                    | OptAce.True -> check_rfmap es rfm
                  then
                    (* Atomic load/store pairs *)
                    let atomic_load_store = make_atomic_load_store es in
                    if
                      C.variant Variant.OptRfRMW
                      && some_same_rf_rmw rfm atomic_load_store
                    then begin
                      if C.debug.Debug_herd.mem then begin
                        let module PP = Pretty.Make(S) in
                        eprintf
                          "Atomicity violation anticipated from rf map%!" ;
                        PP.show_es_rfm test es rfm
                      end ;
                      res
                      end else
                      fold_mem_finals test es
                        rfm ofail atomic_load_store kont res
                  else  res)
            res
  end