Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use map indexed by TermIndex instead of Map Term. #581

Merged
merged 1 commit into from
Nov 14, 2020
Merged

Use map indexed by TermIndex instead of Map Term. #581

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Use map indexed by TermIndex instead of Map Term. 
This avoids relying heavily on the slow Ord instance for type Term,
which can become a significant slowdown when `bindSAWTerm` is called
many times.
  • Loading branch information
Brian Huffman committed Nov 13, 2020
commit 250602ba126465efeb63d5de5f0fca727fe28ea7
20 changes: 14 additions & 6 deletions crucible-saw/src/Lang/Crucible/Backend/SAWCore.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,8 @@ import qualified Data.BitVector.Sized as BV
import Data.IORef
import Data.List (elemIndex)
import Data.Foldable (toList)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.List.NonEmpty (NonEmpty(..))
import Data.Map ( Map )
import qualified Data.Map as Map
Expand Down Expand Up @@ -86,8 +88,8 @@ data SAWCoreState solver fs n
, saw_elt_cache :: B.IdxCache n SAWExpr
-- ^ cache mapping a What4 variable nonce to its corresponding SAWCore term.

, saw_elt_cache_r :: IORef (Map SC.Term (Some (B.SymExpr (SAWCoreBackend n solver fs))))
-- ^ reverse cache mapping a SAWCore term to its corresponding What4 variable.
, saw_elt_cache_r :: IORef (IntMap (Some (B.SymExpr (SAWCoreBackend n solver fs))))
-- ^ reverse cache mapping a SAWCore TermIndex to its corresponding What4 variable.
-- 'saw_elt_cache' and 'saw_elt_cache_r' implement a bidirectional map between
-- SAWCore terms and What4 variables.

Expand Down Expand Up @@ -129,7 +131,7 @@ inFreshNamingContext sym f =

mkNew _gen old =
do ch <- B.newIdxCache
ch_r <- newIORef Map.empty
ch_r <- newIORef IntMap.empty
iref <- newIORef mempty
let new = SAWCoreState
{ saw_ctx = saw_ctx old
Expand Down Expand Up @@ -204,14 +206,20 @@ bindSAWTerm :: SAWCoreBackend n solver fs
bindSAWTerm sym bt t = do
st <- readIORef $ B.sbStateManager sym
ch_r <- readIORef $ saw_elt_cache_r st
case Map.lookup t ch_r of
let midx =
case t of
SC.STApp { SC.stAppIndex = idx } -> Just idx
SC.Unshared _ -> Nothing
case midx >>= flip IntMap.lookup ch_r of
Just (Some var) -> do
Just Refl <- return $ testEquality bt (B.exprType var)
return var
Nothing -> do
sbVar@(B.BoundVarExpr bv) <- freshConstant sym emptySymbol bt
B.insertIdxValue (saw_elt_cache st) (B.bvarId bv) (SAWExpr t)
modifyIORef' (saw_elt_cache_r st) $ Map.insert t (Some sbVar)
case midx of
Just i -> modifyIORef' (saw_elt_cache_r st) $ IntMap.insert i (Some sbVar)
Nothing -> pure ()
return sbVar

newSAWCoreBackend ::
Expand All @@ -222,7 +230,7 @@ newSAWCoreBackend ::
newSAWCoreBackend fm sc gen = do
inpr <- newIORef Seq.empty
ch <- B.newIdxCache
ch_r <- newIORef Map.empty
ch_r <- newIORef IntMap.empty
let feats = Yices.yicesDefaultFeatures
ob_st0 <- initialOnlineBackendState gen feats
let st0 = SAWCoreState
Expand Down