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/Expr.ml

@@ -9,6 +9,8 @@ type t = TypeDef__.expr =
   | UnOp of UnOp.t * t  (** Unary operators         *)
   | BinOp of t * BinOp.t * t  (** Binary operators        *)
   | LstSub of t * t * t  (** Sublist or (list, start, len) *)
+  | LstSwap of t * t * t
+      (** [LstSwap (list, i, j)] is the list obtained from swapping elements [i] and [j] in [list] *)
   | NOp of NOp.t * t list  (** n-ary operators         *)
   | EList of t list  (** Lists of expressions    *)
   | ESet of t list  (** Sets of expressions     *)
@@ -311,6 +313,10 @@ let rec map_opt
             match (map_e e1, map_e e2, map_e e3) with
             | Some e1', Some e2', Some e3' -> Some (LstSub (e1', e2', e3'))
             | _ -> None)
+        | LstSwap (e1, e2, e3) -> (
+            match (map_e e1, map_e e2, map_e e3) with
+            | Some e1', Some e2', Some e3' -> Some (LstSwap (e1', e2', e3'))
+            | _ -> None)
         | NOp (op, les) -> aux les (fun les -> NOp (op, les))
         | EList les -> aux les (fun les -> EList les)
         | ESet les -> aux les (fun les -> ESet les)
@@ -341,6 +347,7 @@ let rec pp fmt e =
           Fmt.pf fmt "%s(%a, %a)" (BinOp.str op) pp e1 pp e2
       | _ -> Fmt.pf fmt "(%a %s %a)" pp e1 (BinOp.str op) pp e2)
   | LstSub (e1, e2, e3) -> Fmt.pf fmt "l-sub(%a, %a, %a)" pp e1 pp e2 pp e3
+  | LstSwap (e1, e2, e3) -> Fmt.pf fmt "l-swap(%a, %a, %a)" pp e1 pp e2 pp e3
   (* (uop e) *)
   | UnOp (op, e) -> Fmt.pf fmt "(%s %a)" (UnOp.str op) pp e
   | EList ll -> Fmt.pf fmt "{{ %a }}" (Fmt.list ~sep:Fmt.comma pp) ll
@@ -422,6 +429,7 @@ let rec is_concrete (le : t) : bool =
   | UnOp (_, e) -> loop [ e ]
   | BinOp (e1, _, e2) -> loop [ e1; e2 ]
   | LstSub (e1, e2, e3) -> loop [ e1; e2; e3 ]
+  | LstSwap (e1, e2, e3) -> loop [ e1; e2; e3 ]
   | NOp (_, les) | EList les | ESet les -> loop les
 
 let is_concrete_zero_i (le : t) : bool =

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/GIL_Syntax/Gil_syntax.mli

@@ -256,6 +256,8 @@ module Expr : sig
     | UnOp of UnOp.t * t  (** Unary operators ({!type:UnOp.t}) *)
     | BinOp of t * BinOp.t * t  (** Binary operators ({!type:BinOp.t}) *)
     | LstSub of t * t * t  (** Sublist *)
+    | LstSwap of t * t * t
+        (** [LstSwap (list, i, j)] is the list obtained from swapping elements [i] and [j] in [list] *)
     | NOp of NOp.t * t list  (** n-ary operators ({!type:NOp.t}) *)
     | EList of t list  (** Lists of expressions *)
     | ESet of t list  (** Sets of expressions *)
@@ -1401,6 +1403,7 @@ module Visitors : sig
          ; visit_LstRepeat : 'c -> BinOp.t -> BinOp.t
          ; visit_LstRev : 'c -> UnOp.t -> UnOp.t
          ; visit_LstSub : 'c -> Expr.t -> Expr.t -> Expr.t -> Expr.t -> Expr.t
+         ; visit_LstSwap : 'c -> Expr.t -> Expr.t -> Expr.t -> Expr.t -> Expr.t
          ; visit_M_abs : 'c -> UnOp.t -> UnOp.t
          ; visit_M_acos : 'c -> UnOp.t -> UnOp.t
          ; visit_M_asin : 'c -> UnOp.t -> UnOp.t
@@ -1671,6 +1674,7 @@ module Visitors : sig
     method visit_LstRepeat : 'c -> BinOp.t -> BinOp.t
     method visit_LstRev : 'c -> UnOp.t -> UnOp.t
     method visit_LstSub : 'c -> Expr.t -> Expr.t -> Expr.t -> Expr.t -> Expr.t
+    method visit_LstSwap : 'c -> Expr.t -> Expr.t -> Expr.t -> Expr.t -> Expr.t
     method visit_M_abs : 'c -> UnOp.t -> UnOp.t
     method visit_M_acos : 'c -> UnOp.t -> UnOp.t
     method visit_M_asin : 'c -> UnOp.t -> UnOp.t
@@ -1941,6 +1945,7 @@ module Visitors : sig
          ; visit_LstRepeat : 'c -> 'f
          ; visit_LstRev : 'c -> 'f
          ; visit_LstSub : 'c -> Expr.t -> Expr.t -> Expr.t -> 'f
+         ; visit_LstSwap : 'c -> Expr.t -> Expr.t -> Expr.t -> 'f
          ; visit_M_abs : 'c -> 'f
          ; visit_M_acos : 'c -> 'f
          ; visit_M_asin : 'c -> 'f
@@ -2179,6 +2184,7 @@ module Visitors : sig
     method visit_LstRepeat : 'c -> 'f
     method visit_LstRev : 'c -> 'f
     method visit_LstSub : 'c -> Expr.t -> Expr.t -> Expr.t -> 'f
+    method visit_LstSwap : 'c -> Expr.t -> Expr.t -> Expr.t -> 'f
     method visit_M_abs : 'c -> 'f
     method visit_M_acos : 'c -> 'f
     method visit_M_asin : 'c -> 'f
@@ -2424,6 +2430,7 @@ module Visitors : sig
          ; visit_LstRepeat : 'c -> unit
          ; visit_LstRev : 'c -> unit
          ; visit_LstSub : 'c -> Expr.t -> Expr.t -> Expr.t -> unit
+         ; visit_LstSwap : 'c -> Expr.t -> Expr.t -> Expr.t -> unit
          ; visit_M_abs : 'c -> unit
          ; visit_M_acos : 'c -> unit
          ; visit_M_asin : 'c -> unit
@@ -2666,6 +2673,7 @@ module Visitors : sig
     method visit_LstRepeat : 'c -> unit
     method visit_LstRev : 'c -> unit
     method visit_LstSub : 'c -> Expr.t -> Expr.t -> Expr.t -> unit
+    method visit_LstSwap : 'c -> Expr.t -> Expr.t -> Expr.t -> unit
     method visit_M_abs : 'c -> unit
     method visit_M_acos : 'c -> unit
     method visit_M_asin : 'c -> unit

GillianCore/GIL_Syntax/TypeDef__.ml

@@ -138,6 +138,7 @@ and expr =
   | UnOp of unop * expr
   | BinOp of expr * binop * expr
   | LstSub of expr * expr * expr
+  | LstSwap of expr * expr * expr
   | NOp of nop * expr list
   | EList of expr list
   | ESet of expr list

GillianCore/engine/Abstraction/MP.ml

@@ -141,7 +141,7 @@ let rec missing_expr (kb : KB.t) (e : Expr.t) : KB.t list =
     | UnOp (_, e) -> f e
     | BinOp (e1, _, e2) -> join [ e1; e2 ]
     | NOp (_, le) | EList le | ESet le -> join le
-    | LstSub (e1, e2, e3) ->
+    | LstSub (e1, e2, e3) | LstSwap (e1, e2, e3) ->
         let result = join [ e1; e2; e3 ] in
         L.verbose (fun fmt ->
             fmt "Missing for %a: %a" Expr.full_pp e
@@ -263,6 +263,11 @@ let rec learn_expr
       | true, true | false, false -> []
       | true, false -> f (BinOp (base_expr, IMinus, e1)) e2
       | false, true -> f (BinOp (base_expr, IMinus, e2)) e1)
+  | LstSwap (l, i, j) -> (
+      (* If we know i and j, we can reconstruct the l, because swapping is involutive *)
+      match (is_known_expr kb l, is_known_expr kb i, is_known_expr kb j) with
+      | false, true, true -> f (Expr.LstSwap (base_expr, i, j)) l
+      | _, _, _ -> [])
   (* Floating-point minus is invertible in two different ways *)
   | BinOp (e1, FMinus, e2) -> (
       (* If both operands are known or both are unknown, nothing can be done *)

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,37 @@ 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 }
+        | [] -> 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
-            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
+            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/Normaliser.ml

@@ -182,7 +182,8 @@ module Make (SPState : PState.S) = struct
                             expression")
                   | BinOp (_, _, _) | UnOp (_, _) -> UnOp (TypeOf, nle1)
                   | Exists _ | EForall _ -> Lit (Type BooleanType)
-                  | EList _ | LstSub _ | NOp (LstCat, _) -> Lit (Type ListType)
+                  | EList _ | LstSub _ | NOp (LstCat, _) | LstSwap _ ->
+                      Lit (Type ListType)
                   | NOp (_, _) | ESet _ -> Lit (Type SetType))
               | _ -> UnOp (uop, nle1)))
       | EList le_list ->
@@ -217,6 +218,17 @@ module Make (SPState : PState.S) = struct
           | _, Lit (Num _), Lit (Num _) ->
               raise (Failure "Sublist indexes non-integer")
           | _, _, _ -> LstSub (nle1, nle2, nle3))
+      | LstSwap (l, i, j) -> (
+          let fl, fi, fj = (f l, f i, f j) in
+          if Expr.equal fi fj then fl
+          else
+            match (fl, fl, fj) with
+            | EList les, Lit (Int i), Lit (Int j) ->
+                let new_list =
+                  List_utils.list_swap les (Z.to_int i) (Z.to_int j)
+                in
+                EList new_list
+            | _ -> LstSwap (fl, fi, fj))
       | Exists (bt, e) -> (
           let new_gamma = Type_env.copy gamma in
           List.iter

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