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/GIL_Syntax/Formula.ml

@@ -153,7 +153,7 @@ let alocs (f : t) : SS.t = Visitors.Collectors.aloc_collector#visit_formula () f
 let clocs (f : t) : SS.t = Visitors.Collectors.cloc_collector#visit_formula () f
 
 (* Get all the locations in [a] *)
-let locs (f : t) : SS.t = Visitors.Collectors.cloc_collector#visit_formula () f
+let locs (f : t) : SS.t = Visitors.Collectors.loc_collector#visit_formula () f
 let get_print_info (a : t) = (pvars a, lvars a, locs a)
 
 (* Get all the logical expressions of --a-- of the form (Lit (LList lst)) and (EList lst)  *)

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
 
@@ -1888,7 +1924,7 @@ module Make (State : SState.S) :
       match produced with
       | Error _ -> []
       | Ok state ->
-          let _, simplified = simplify_astate ~matching:true state in
+          let _, simplified = simplify_astate ~save:true ~matching:true state in
           simplified
 
     let match_assertion astate subst step =
@@ -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,30 @@ 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 ] -> (
+          (* We add (persistent) knowledge from lhs state to current state *)
+          let lhs_pfs = State.get_pfs lhs_state.state |> PFS.to_list in
+          let lhs_alocs =
+            List.fold_left
+              (fun acc pf -> SS.union acc (Formula.alocs pf))
+              SS.empty lhs_pfs
+          in
+          let current_sstate =  State.add_spec_vars astate.state lhs_alocs in 
+          match State.assume_a ~matching:true ~production:true current_sstate lhs_pfs with
+          | Some current_sstate ->
+            { lhs_state; current_state = { astate with state = current_sstate }; subst }
+          | None ->
+            Fmt.kstr L.fail "Wand lhs pure contradicts with current state!")
+        | _ :: _ ->
+            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/Abstraction/Verifier.ml

@@ -607,7 +607,11 @@ struct
             let successes, errors = Res_list.split lemma_evaluation_results in
             match errors with
             | [] -> analyse_lemma_results test successes
-            | _ ->
+            | errors ->
+                L.normal (fun m ->
+                    m "Failed to verify lemma, terminated with errors:\n%a"
+                      (Fmt.Dump.list SPState.pp_err)
+                      errors);
                 print_success_or_failure false;
                 false))
 

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
@@ -2563,6 +2567,10 @@ let rec reduce_formula_loop
           Eq (e, Lit (Num 0.))
       | Eq (BinOp (Lit (Int x), ITimes, e), Lit (Int z))
         when Z.equal z Z.zero && not (Z.equal x Z.zero) -> Eq (e, Expr.zero_i)
+      | Eq (lst, NOp (LstCat, [Expr.EList [ head ]; Expr.UnOp (Cdr, lst')])) when Expr.equal lst lst' ->
+        (* lst == ([head] @ (cdr lst)) *)
+          let open Formula.Infix in
+          head #== (Expr.list_nth lst 0)
       | Eq (Lit (LList ll), Lit (LList lr)) -> if ll = lr then True else False
       | Eq (EList le, Lit (LList ll)) | Eq (Lit (LList ll), EList le) ->
           if List.length ll <> List.length le then False
@@ -3037,7 +3045,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)