diff --git a/Gillian-C/lib/MonadicSMemory.ml b/Gillian-C/lib/MonadicSMemory.ml index 8dea96a4..bf26ae5d 100644 --- a/Gillian-C/lib/MonadicSMemory.ml +++ b/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 diff --git a/GillianCore/GIL_Syntax/Formula.ml b/GillianCore/GIL_Syntax/Formula.ml index ae52b295..901ba876 100644 --- a/GillianCore/GIL_Syntax/Formula.ml +++ b/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) *) diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml index 17d6edec..688d7449 100644 --- a/GillianCore/engine/Abstraction/Matcher.ml +++ b/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 diff --git a/GillianCore/engine/Abstraction/Verifier.ml b/GillianCore/engine/Abstraction/Verifier.ml index 0f2a1114..667eb6a2 100644 --- a/GillianCore/engine/Abstraction/Verifier.ml +++ b/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)) diff --git a/GillianCore/engine/FOLogic/FOSolver.ml b/GillianCore/engine/FOLogic/FOSolver.ml index 7220a73e..94bd8962 100644 --- a/GillianCore/engine/FOLogic/FOSolver.ml +++ b/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 diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml index 31a205c0..bbb87288 100644 --- a/GillianCore/engine/FOLogic/Reduction.ml +++ b/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) diff --git a/GillianCore/engine/FOLogic/Simplifications.ml b/GillianCore/engine/FOLogic/Simplifications.ml index 3603cfec..c3433640 100644 --- a/GillianCore/engine/FOLogic/Simplifications.ml +++ b/GillianCore/engine/FOLogic/Simplifications.ml @@ -549,9 +549,9 @@ let simplify_pfs_and_gamma | ALoc alocl, ALoc alocr when matching -> L.verbose (fun fmt -> fmt "Two equal alocs: %s and %s" alocl alocr); - SESubst.put result (ALoc alocr) (ALoc alocl); + SESubst.put result (ALoc alocl) (ALoc alocr); let temp_subst = - SESubst.init [ (ALoc alocr, ALoc alocl) ] + SESubst.init [ (ALoc alocl, ALoc alocr) ] in PFS.substitution temp_subst lpfs; let substituted = diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml index 50b85033..19e9930c 100644 --- a/GillianCore/engine/symbolic_semantics/SState.ml +++ b/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 ( diff --git a/GillianCore/monadic/FOSolver.ml b/GillianCore/monadic/FOSolver.ml index 9e8c10c1..ed2e1004 100644 --- a/GillianCore/monadic/FOSolver.ml +++ b/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 diff --git a/GillianCore/monadic/delayed.ml b/GillianCore/monadic/delayed.ml index 2f7c929a..6dfc9f2e 100644 --- a/GillianCore/monadic/delayed.ml +++ b/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 ]) diff --git a/GillianCore/utils/list_res.ml b/GillianCore/utils/list_res.ml index c6e7abdb..ee0fe68f 100644 --- a/GillianCore/utils/list_res.ml +++ b/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 diff --git a/ppx_sat/test/out.expected b/ppx_sat/test/out.expected index b77944da..9d8b627e 100644 --- a/ppx_sat/test/out.expected +++ b/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: