From 455ea495fb808877a60e9b03cb589fae48746b38 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 19 Mar 2019 09:26:15 -0700 Subject: [PATCH] [sledge] Strengthen Sh re null cannot be allocated MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Summary: Strengthen the Sh.seg constructor and Sh.is_false test to account for the axiom that `null -[_;_)-> ⟨_,_⟩` is inconsistent. Reviewed By: ngorogiannis Differential Revision: D14481986 fbshipit-source-id: 7016e7451 --- sledge/src/symbheap/sh.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 8a8cd75c0..9c09abeb2 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -370,7 +370,11 @@ let rec pure (e : Exp.t) = [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q] let and_ e q = star (pure e) q -let seg pt = {emp with us= fv_seg pt; heap= [pt]} |> check invariant + +let seg pt = + let us = fv_seg pt in + if Exp.equal Exp.null pt.loc then false_ us + else {emp with us; heap= [pt]} |> check invariant (** Update *) @@ -387,8 +391,10 @@ let is_emp = function let is_false = function | {djns= [[]]; _} -> true - | {cong; pure; _} -> + | {cong; pure; heap; _} -> List.exists pure ~f:(fun b -> Exp.is_false (Equality.normalize cong b)) + || List.exists heap ~f:(fun seg -> + Equality.entails_eq cong seg.loc Exp.null ) let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) = let heap = emp.heap in