From 6a5eae0952e16b9a66b480717577cec6f3e0bdc7 Mon Sep 17 00:00:00 2001 From: Tristan Ravitch Date: Mon, 16 Dec 2019 11:10:17 -0800 Subject: [PATCH] Improve the SMT generated for array lookups with symbolic indices What4 attempts to simplify array lookups of values with concrete indices. In cases where the index to look up in symbolic, that fails and it instead generates a huge mux over all possible indexes, which is very expensive and counterproductive. This commit removes the special handling of symbolic indices, allowing the generated SMT to fall back on just issuing an SMT array lookup. Fixes #371 --- what4/src/What4/Expr/Builder.hs | 33 +++++---------------------------- 1 file changed, 5 insertions(+), 28 deletions(-) diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs index 775596e22..8f5f5f521 100644 --- a/what4/src/What4/Expr/Builder.hs +++ b/what4/src/What4/Expr/Builder.hs @@ -3473,22 +3473,6 @@ evalBoundVars sym e vars exprs = do } evalBoundVars' tbls sym e --- | Return true if corresponding expressions in contexts are equivalent. -allEq :: forall sym ctx - . IsExprBuilder sym - => sym - -> Ctx.Assignment (SymExpr sym) ctx - -> Ctx.Assignment (SymExpr sym) ctx - -> IO (Pred sym) -allEq sym x y = Ctx.forIndex (Ctx.size x) joinEq (pure (truePred sym)) - where joinEq :: IO (Pred sym) -> Ctx.Index ctx tp -> IO (Pred sym) - joinEq mp i = do - q <- isEq sym (x Ctx.! i) (y Ctx.! i) - case asConstantPred q of - Just True -> mp - Just False -> return (falsePred sym) - Nothing -> andPred sym q =<< mp - -- | This attempts to lookup an entry in a symbolic array. -- -- It patterns maps on the array constructor. @@ -3505,18 +3489,11 @@ sbConcreteLookup :: forall t st fs d tp range -> IO (Expr t range) sbConcreteLookup sym arr0 mcidx idx -- Try looking up a write to a concrete address. - | Just (ArrayMap _ _ entry_map def) <- asApp arr0 = do - case mcidx of - Just cidx -> do - case Hash.mapLookup cidx entry_map of - Just v -> return v - Nothing -> sbConcreteLookup sym def mcidx idx - Nothing -> Map.foldrWithKey f (sbConcreteLookup sym def mcidx idx) (Hash.hashedMap entry_map) - where f updated_cidx c m = do - updated_idx <- traverseFC (indexLit sym) updated_cidx - p <- allEq sym updated_idx idx - iteM baseTypeIte sym p (pure c) m - + | Just (ArrayMap _ _ entry_map def) <- asApp arr0 + , Just cidx <- mcidx = + case Hash.mapLookup cidx entry_map of + Just v -> return v + Nothing -> sbConcreteLookup sym def mcidx idx -- Evaluate function arrays on ground values. | Just (ArrayFromFn f) <- asNonceApp arr0 = do betaReduce sym f idx