Something is over-approx for some reason...

Gillian-C/lib/MonadicSMemory.ml

@@ -525,7 +525,10 @@ let execute_prod_single heap params =
   ] ->
       let perm = ValueTranslation.permission_of_string perm_string in
       let chunk = ValueTranslation.chunk_of_string chunk_string in
-      let* sval = SVal.of_gil_expr_exn sval_e in
+      let* sval =
+        try SVal.of_gil_expr_exn sval_e
+        with SVal.NotACompCertValue _ -> Delayed.vanish ()
+      in
       let++ mem = Mem.prod_single heap.mem loc ofs chunk sval perm in
       { heap with mem }
   | _ -> fail_ungracefully "set_single" params

GillianCore/engine/Abstraction/Matcher.ml

@@ -139,7 +139,6 @@ end
 
 module Make (State : SState.S) :
   S with type state_t = State.t and type err_t = State.err_t = struct
-  open Literal
   open Containers
   module L = Logging
 
@@ -757,6 +756,15 @@ module Make (State : SState.S) :
     | None -> other_state_err "final state non admissible"
     | Some state -> Res_list.return { state; preds; pred_defs; wands; variants }
 
+  let production_priority (a : Asrt.t) : int =
+    match a with
+    | Emp -> 0
+    | Types _ -> 0
+    | Pure _ -> 1
+    | Pred _ | Wand _ -> 2
+    | GA _ -> 3
+    | Star _ -> failwith "unreachable"
+
   let produce (astate : t) (subst : SVal.SESubst.t) (a : Asrt.t) :
       (t, err_t) Res_list.t =
     L.verbose (fun m ->
@@ -765,6 +773,11 @@ module Make (State : SState.S) :
            -----------------@\n\
            Produce assertion: @[%a@]@]" Asrt.pp a);
     let sas = MP.collect_simple_asrts a in
+    let sas =
+      List.sort
+        (fun a1 a2 -> compare (production_priority a1) (production_priority a2))
+        sas
+    in
     produce_asrt_list astate subst sas
 
   let produce_posts (state : t) (subst : SVal.SESubst.t) (asrts : Asrt.t list) :
@@ -1548,7 +1561,6 @@ module Make (State : SState.S) :
                 L.fail "ERROR: IMPOSSIBLE! MATCHING ERRORS IN UX MODE!!!!"
             | false, [], [] ->
                 L.fail "OX MATCHING VANISHED??? MEDOOOOOOOO!!!!!!!!!"
-            | false, _ :: _ :: _, [] -> L.fail "DEATH. OX MATCHING BRANCHED"
             | true, [], _ ->
                 (* Vanished in UX *)
                 explore_next_states (rest_search_states, errs_so_far)
@@ -1569,6 +1581,30 @@ module Make (State : SState.S) :
                   ( ((state, subst, rest_mp), case_depth, false)
                     :: rest_search_states,
                     errs_so_far )
+            | false, states, [] -> (
+                L.verbose (fun m ->
+                    m
+                      "!!!CONSUMER YIELDED MULTIPLE BRANCHES IN OX MODE: %d \
+                       branches!!!"
+                      (List.length states));
+                (* We have obtained several branches. So there is a disjunction in the PFS.
+                   All branches need to successfuly unify against this *)
+                let all_next =
+                  List.map
+                    (fun state ->
+                      let state = copy_astate state in
+                      let subst = SVal.SESubst.copy subst in
+                      explore_next_states
+                        ( [ ((state, subst, rest_mp), case_depth, false) ],
+                          errs_so_far ))
+                    states
+                in
+                let res = List_res.flat all_next in
+                match res with
+                | Ok res -> Ok res
+                | Error errs ->
+                    explore_next_states (rest_search_states, errs @ errs_so_far)
+                )
             | true, first :: rem, [] ->
                 let rem =
                   List.map
@@ -1727,7 +1763,7 @@ module Make (State : SState.S) :
 
     let is_unfoldable_lit lit =
       match lit with
-      | Loc _ | LList _ -> false
+      | Literal.Loc _ | LList _ -> false
       | _ -> true
     in
 
@@ -2105,6 +2141,8 @@ module Make (State : SState.S) :
         in
         [ { lhs_state = new_lhs_state; current_state; subst } ]
       in
+      (* Importantly, we must *never* unfold anything on the lhs
+         without checking that it yields a unique state, as to avoid unsoundness. *)
       (* If it fails, we try splitting the step and we try again *)
       let- split_errs =
         let split_option =
@@ -2245,36 +2283,17 @@ module Make (State : SState.S) :
         let in_bindings = Pred.in_args rpred.pred all_bindings in
         SVal.SESubst.init in_bindings
       in
-      let start_states =
+      let start_state =
         match lhs_states with
-        | [] -> failwith "wand lhs is False!"
-        | first :: rest ->
-            let rest_pack_states =
-              List.map
-                (fun lhs_state ->
-                  {
-                    lhs_state;
-                    current_state = copy_astate astate;
-                    subst = SVal.SESubst.copy subst;
-                  })
-                rest
-            in
-            let first_pack_state =
-              { lhs_state = first; current_state = astate; subst }
-            in
-            first_pack_state :: rest_pack_states
-      in
-      L.verbose (fun m ->
-          m "About to start consuming rhs of wand. Currently %d search states"
-            (List.length start_states));
-      let final_states =
-        List.fold_left
-          (fun acc state ->
-            let* acc = acc in
-            let+ case = package_mp rhs_mp state in
-            case @ acc)
-          (Ok []) start_states
+        | [] -> Fmt.kstr L.fail "wand lhs is False!"
+        | [ lhs_state ] -> { lhs_state; current_state = astate; subst }
+        | _ :: _ ->
+            Fmt.kstr L.fail "Wand lhs produced %d states!@\n%a"
+              (List.length lhs_states)
+              (Fmt.list ~sep:(Fmt.any "@\n@\n@\nNEXT STATE@\n@\n@\n") pp_astate)
+              lhs_states
       in
+      let final_states = package_mp rhs_mp start_state in
       let* states = final_states in
       let all_res =
         List.map

GillianCore/engine/FOLogic/FOSolver.ml

@@ -150,8 +150,7 @@ let check_entailment
   in
   let gamma_right = Type_env.filter gamma (fun v -> SS.mem v existentials) in
 
-  (* If left side is false, return false *)
-  if List.mem Formula.False (left_fs @ right_fs) then false
+  if List.mem Formula.False left_fs then true
   else
     (* Check satisfiability of left side *)
     let left_sat =
@@ -266,6 +265,4 @@ let num_is_less_or_equal ~pfs ~gamma e1 e2 =
 
 let resolve_loc_name ~pfs ~gamma loc =
   Logging.tmi (fun fmt -> fmt "get_loc_name: %a" Expr.pp loc);
-  match Reduction.reduce_lexpr ~pfs ~gamma loc with
-  | Lit (Loc loc) | ALoc loc -> Some loc
-  | loc' -> Reduction.resolve_expr_to_location pfs gamma loc'
+  Reduction.resolve_expr_to_location pfs gamma loc

GillianCore/engine/FOLogic/Reduction.ml

@@ -2325,9 +2325,11 @@ and substitute_in_int_expr (le_to_find : Expr.t) (le_to_subst : Expr.t) le :
                       let c = Option.get c in
                       let () =
                         if not (Z.equal (c mod s) Z.zero) then
-                          failwith
-                            "Reduction.substitute_in_int_expr, scaling with \
-                             invalid number"
+                          raise
+                            (ReductionException
+                               ( le,
+                                 "Reduction.substitute_in_int_expr, scaling \
+                                  with invalid number" ))
                       in
                       c / s)
                     coeffs c_le_tf_symb
@@ -2412,76 +2414,78 @@ and substitute_for_list_length (pfs : PFS.t) (le : Expr.t) : Expr.t =
 
 let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
     string option =
-  let max_fuel = 5 in
+  let max_fuel = 10 in
+
+  let loc_name = function
+    | Expr.ALoc loc | Lit (Loc loc) -> Some loc
+    | _ -> None
+  in
 
   let rec resolve_expr_to_location_aux
       (fuel : int)
       (tried : Expr.Set.t)
       (to_try : Expr.t list) : string option =
+    let open Syntaxes.Option in
+    L.tmi (fun m -> m "to_try: %a" (Fmt.Dump.list Expr.pp) to_try);
+    let* () = if fuel <= 0 then None else Some () in
     let f = resolve_expr_to_location_aux (fuel - 1) in
-    match fuel = 0 with
-    | true -> None
-    | false -> (
-        match to_try with
-        | [] -> None
-        | e :: _rest -> (
-            match e with
-            | Lit (Loc loc) | ALoc loc -> Some loc
-            | _ -> (
-                let equal_e = get_equal_expressions pfs e in
-                let equal_e =
-                  equal_e @ List.map (reduce_lexpr ~pfs ~gamma) equal_e
-                in
-                let ores =
-                  List.find_opt
-                    (fun x ->
-                      match x with
-                      | Expr.ALoc _ | Lit (Loc _) -> true
-                      | _ -> false)
-                    equal_e
-                in
-                match ores with
-                | Some (ALoc loc) | Some (Lit (Loc loc)) -> Some loc
-                | _ -> (
-                    let lvars_e =
-                      List.map
-                        (fun x -> Expr.LVar x)
-                        (Containers.SS.elements (Expr.lvars e))
-                    in
-                    let found_subst =
-                      List.map
-                        (fun e -> (e, get_equal_expressions pfs e))
-                        lvars_e
-                    in
-                    let found_subst =
-                      List.filter_map
-                        (fun (e, es) ->
-                          match es with
-                          | [] -> None
-                          | es :: _ -> Some (e, es))
-                        found_subst
-                    in
-                    let subst_e =
-                      List.fold_left
-                        (fun (e : Expr.t) (e_to, e_with) ->
-                          Expr.subst_expr_for_expr ~to_subst:e_to
-                            ~subst_with:e_with e)
-                        e found_subst
-                    in
-                    let subst_e = reduce_lexpr ~pfs ~gamma subst_e in
-                    match subst_e with
-                    | ALoc loc | Lit (Loc loc) -> Some loc
-                    | _ ->
-                        let new_tried = Expr.Set.add e tried in
-                        let new_to_try = equal_e @ [ subst_e ] in
-                        let new_to_try =
-                          List.filter
-                            (fun e -> not (Expr.Set.mem e new_tried))
-                            new_to_try
-                        in
-                        f new_tried new_to_try))))
+    let* e, rest =
+      match to_try with
+      | [] -> None
+      | e :: rest -> Some (e, rest)
+    in
+    (* If e is a loc name, we return it *)
+    let/ () = loc_name e in
+    let equal_e = get_equal_expressions pfs e in
+    let equal_e = equal_e @ List.map (reduce_lexpr ~pfs ~gamma) equal_e in
+    (* If we find a loc in there, we return it *)
+    let/ () = List.find_map loc_name equal_e in
+    (* We actually want to try all possible substs! *)
+    let all_lvars = Containers.SS.elements (Expr.lvars e) in
+    let subst_for_each_lvar =
+      List.map
+        (fun x ->
+          let e = Expr.LVar x in
+          let with_eq =
+            List.map (fun eq -> (e, eq)) (get_equal_expressions pfs e)
+          in
+          (e, e) :: with_eq)
+        all_lvars
+    in
+    L.tmi (fun m ->
+        m "subst_for_each_lvar: %a"
+          (Fmt.Dump.list (Fmt.Dump.list (Fmt.Dump.pair Expr.pp Expr.pp)))
+          subst_for_each_lvar);
+    let found_substs =
+      List.fold_left
+        (fun l1 l2 -> List_utils.cross_product l1 l2 (fun l x -> x :: l))
+        [ [] ] subst_for_each_lvar
+    in
+    L.tmi (fun m ->
+        m "found_substs: %a"
+          (Fmt.Dump.list (Fmt.Dump.list (Fmt.Dump.pair Expr.pp Expr.pp)))
+          found_substs);
+    (* lvar and substs is a list [ (ei, esi) ] where for each ei, esi is a list of equal expressions.
+       We are going to build the product of each esi to obtain *)
+    let subst_es =
+      List.map
+        (fun found_subst ->
+          List.fold_left
+            (fun (e : Expr.t) (e_to, e_with) ->
+              Expr.subst_expr_for_expr ~to_subst:e_to ~subst_with:e_with e)
+            e found_subst)
+        found_substs
+    in
+    L.tmi (fun m -> m "subst_es: %a" (Fmt.Dump.list Expr.pp) subst_es);
+    let subst_es = List.map (reduce_lexpr ~pfs ~gamma) subst_es in
+    let/ () = List.find_map loc_name subst_es in
+    let new_tried = Expr.Set.add e tried in
+    let new_to_try = rest @ equal_e @ subst_es in
+    let new_to_try =
+      List.filter (fun e -> not (Expr.Set.mem e new_tried)) new_to_try
+    in
+    f new_tried new_to_try
   in
-
   resolve_expr_to_location_aux max_fuel Expr.Set.empty [ e ]
 
 let rec reduce_formula_loop
@@ -3037,7 +3041,14 @@ let reduce_formula
     ?(pfs : PFS.t = PFS.init ())
     ?(gamma = Type_env.init ())
     (a : Formula.t) : Formula.t =
-  reduce_formula_loop ~top_level:true ~rpfs matching pfs gamma a
+  try reduce_formula_loop ~top_level:true ~rpfs matching pfs gamma a
+  with ReductionException (e, msg) ->
+    Logging.normal (fun m ->
+        m
+          "WARNING: Reduction of formula %a failed while reducing %a with \
+           message %s. Not reducing this formula."
+          Formula.pp a Expr.pp e msg);
+    a
 
 let relate_llen
     (pfs : PFS.t)

GillianCore/engine/symbolic_semantics/SState.ml

@@ -322,6 +322,7 @@ module Make (SMemory : SMemory.S) :
                (ps @ PFS.to_list pfs)
                gamma
         then (
+          let ps = List.concat_map Formula.split_conjunct_formulae ps in
           List.iter (PFS.extend pfs) ps;
           Some state)
         else (

GillianCore/monadic/FOSolver.ml

@@ -37,7 +37,6 @@ let check_entailment ~(pc : Pc.t) formula =
     in
     match f with
     | True -> true
-    | False -> false
     | _ ->
         FOSolver.check_entailment ~matching:pc.matching
           Utils.Containers.SS.empty pfs [ f ] gamma

GillianCore/monadic/delayed.ml

@@ -44,11 +44,12 @@ let branch_on
   | guard -> (
       try
         let guard_sat = FOSolver.sat ~pc:curr_pc guard in
-        if not guard_sat then (* [Not guard)] has to be sat *)
-          else_ () ~curr_pc
+        let not_guard = Formula.Infix.fnot guard in
+        if not guard_sat then
+          (* [Not guard] has to be sat *)
+          else_ () ~curr_pc:(Pc.extend curr_pc [ not_guard ])
         else
           let then_branches = then_ () ~curr_pc:(Pc.extend curr_pc [ guard ]) in
-          let not_guard = Formula.Infix.fnot guard in
           if FOSolver.sat ~pc:curr_pc not_guard then
             let else_branches =
               else_ () ~curr_pc:(Pc.extend curr_pc [ not_guard ])

GillianCore/utils/list_res.ml

@@ -9,6 +9,15 @@ let pp ~ok ~err =
 let return (v : 'a) : ('a, 'b) t = Ok [ v ]
 let vanish = Ok []
 
+let flat (l : ('a, 'b) t list) : ('a, 'b) t =
+  List.fold_left
+    (fun acc x ->
+      match (acc, x) with
+      | Ok l, Ok l' -> Ok (l @ l')
+      | Error l, Error l' -> Error (l @ l')
+      | Ok _, (Error _ as err) | (Error _ as err), Ok _ -> err)
+    (Ok []) l
+
 let bind (x : ('a, 'e) t) (f : 'a -> ('b, 'e) t) : ('b, 'e) t =
   match x with
   | Error errs -> Error errs

ppx_sat/test/out.expected

@@ -1,7 +1,7 @@
 [{pc:
    {pfs: [(! (x == 1i))];
     gamma: (x: Int);
-    learned: [(1i i<=# x); (2i i<=# x)];
+    learned: [(0i i<# x); (1i i<# x); (1i i<=# x); (2i i<=# x)];
     learned_types: []};
   value: 12},
  {pc: