From de2ea63d40ce7112f1eddf21f7d3d2aeb17f3a34 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 16 Nov 2020 12:52:37 -0800 Subject: [PATCH] [sledge] Fix vocabulary handling of symbolic execution of multi-spec insts Summary: Instructions that have multiple specs sometimes have inconsistent footprints for one or more of their specifications. In such cases, the handling of the existential and universal vocabularies was sometimes incorrect before this diff. In particular, the ghosts of a spec need not appear in the pure approximation of the footprint, which the previous code incorrectly assumed. Also, the unit of disjunction is `false` with an empty vocabulary, not the precondition's vocabulary as the previous code incorrectly used. Reviewed By: ngorogiannis Differential Revision: D24989067 fbshipit-source-id: eca3bff55 --- sledge/src/exec.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index 0401d215d..71f9f99e1 100644 --- a/sledge/src/exec.ml +++ b/sledge/src/exec.ml @@ -692,13 +692,14 @@ let exec_specs pre = let rec exec_specs_ (xs, pre) = function | specm :: specs -> let gs, spec = gen_spec pre.Sh.us specm in + let pure = Sh.pure (Sh.pure_approx spec.foot) in let pre_pure = - Sh.(star (exists gs (Sh.pure (pure_approx spec.foot))) pre) + Sh.star (Sh.exists (Var.Set.inter gs pure.us) pure) pre in let* post = exec_spec_ (xs, pre_pure) (gs, spec) in let+ posts = exec_specs_ (xs, pre) specs in Sh.or_ post posts - | [] -> Some (Sh.false_ pre.us) + | [] -> Some (Sh.false_ Var.Set.empty) in exec_specs_ (xs, pre)