crucible-llvm-0.7: src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs
------------------------------------------------------------------------
-- |
-- Module : Lang.Crucible.LLVM.SimpleLoopFixpointCHC
-- Description : Execution feature to compute loop fixpoint in
-- conjunction with CHC
-- Copyright : (c) Galois, Inc 2021
-- License : BSD3
-- Stability : provisional
--
-- This offers a similar API to what is offered in
-- "Lang.Crucible.LLVM.SimpleLoopFixpoint", but this generates proof obligations
-- involving a predicate function (named @inv@). The intent is that a user will
-- leverage Z3's constrained horn-clause (CHC) functionality to synthesize an
-- implementation of @inv@ and then substitute it back into the proof
-- obligations.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TupleSections #-}
module Lang.Crucible.LLVM.SimpleLoopFixpointCHC
( FixpointEntry(..)
, FixpointState(..)
, CallFrameContext(..)
, SomeCallFrameContext(..)
, ExecutionFeatureContext(..)
, simpleLoopFixpoint
) where
import Control.Lens
import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Maybe
import Data.Foldable
import qualified Data.IntMap as IntMap
import Data.IORef
import Data.Kind
import qualified Data.List as List
import Data.Maybe
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import Data.Set (Set)
import GHC.TypeLits (KnownNat)
import Numeric.Natural (Natural)
import qualified System.IO
import qualified Data.BitVector.Sized as BV
import Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.Map (MapF)
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import Data.Parameterized.TraversableF
import Data.Parameterized.TraversableFC
import qualified What4.Config as W4
import qualified What4.Expr.Builder as W4
import qualified What4.Interface as W4
import qualified What4.Solver as W4
import qualified Lang.Crucible.Analysis.Fixpoint.Components as C
import qualified Lang.Crucible.Backend as C
import qualified Lang.Crucible.CFG.Core as C
import qualified Lang.Crucible.FunctionHandle as C
import qualified Lang.Crucible.Panic as C
import qualified Lang.Crucible.Simulator.CallFrame as C
import qualified Lang.Crucible.Simulator.EvalStmt as C
import qualified Lang.Crucible.Simulator.ExecutionTree as C
import qualified Lang.Crucible.Simulator.GlobalState as C
import qualified Lang.Crucible.Simulator.Operations as C
import qualified Lang.Crucible.Simulator.RegMap as C
import qualified Lang.Crucible.Simulator as C
import qualified Lang.Crucible.LLVM.Bytes as C
import qualified Lang.Crucible.LLVM.DataLayout as C
import qualified Lang.Crucible.LLVM.MemModel as C
import qualified Lang.Crucible.LLVM.MemModel.MemLog as C hiding (Mem)
import qualified Lang.Crucible.LLVM.MemModel.Pointer as C
import qualified Lang.Crucible.LLVM.MemModel.Type as C
-- import qualified Lang.Crucible.LLVM.MemModel.Generic as C (writeArrayMem)
-- | When live loop-carried dependencies are discovered as we traverse
-- a loop body, new "widening" variables are introduced to stand in
-- for those locations. When we introduce such a variable, we
-- capture what value the variable had when we entered the loop (the
-- \"header\" value); this is essentially the initial value of the
-- variable. We also compute what value the variable should take on
-- its next iteration assuming the loop doesn't exit and executes
-- along its backedge. This \"body\" value will be computed in
-- terms of the the set of all discovered live variables so far.
-- We know we have reached fixpoint when we don't need to introduce
-- and more fresh widening variables, and the body values for each
-- variable are stable across iterations.
data FixpointEntry sym tp = FixpointEntry
{ headerValue :: W4.SymExpr sym tp
, bodyValue :: W4.SymExpr sym tp
}
instance OrdF (W4.SymExpr sym) => OrdF (FixpointEntry sym) where
compareF x y = joinOrderingF
(compareF (headerValue x) (headerValue y))
(compareF (bodyValue x) (bodyValue y))
instance OrdF (FixpointEntry sym) => W4.TestEquality (FixpointEntry sym) where
testEquality x y = orderingF_refl $ compareF x y
data MemLocation sym w = MemLocation
{ memLocationBlock :: Natural
, memLocationOffset :: W4.SymBV sym w
, memLocationSize :: W4.SymBV sym w
}
instance OrdF (W4.SymExpr sym) => Ord (MemLocation sym w) where
compare x y =
compare (memLocationBlock x) (memLocationBlock y)
<> toOrdering (compareF (memLocationOffset x) (memLocationOffset y))
<> toOrdering (compareF (memLocationSize x) (memLocationSize y))
instance OrdF (W4.SymExpr sym) => Eq (MemLocation sym w) where
x == y = EQ == compare x y
data MemFixpointEntry sym wptr where
MemStoreFixpointEntry ::
(1 <= w) =>
W4.SymBV sym w {- ^ bitvector join variable -} ->
C.StorageType ->
MemFixpointEntry sym wptr
MemArrayFixpointEntry ::
W4.SymArray sym (C.SingleCtx (W4.BaseBVType wptr)) (W4.BaseBVType 8) {- ^ array join variable -} ->
W4.SymBV sym wptr {- ^ length of the allocation -} ->
MemFixpointEntry sym wptr
-- | This datatype captures the state machine that progresses as we
-- attempt to compute a loop invariant for a simple structured loop.
data FixpointState sym wptr blocks args
-- | We have not yet encoundered the loop head
= BeforeFixpoint
-- | We have encountered the loop head at least once, and are in the process
-- of converging to an inductive representation of the live variables
-- in the loop.
| ComputeFixpoint (FixpointRecord sym wptr blocks args)
-- | We have found an inductively-strong representation of the live variables
-- of the loop, and have discovered the loop index structure controling the
-- execution of the loop. We are now executing the loop once more to compute
-- verification conditions for executions that reamain in the loop.
| CheckFixpoint
(FixpointRecord sym wptr blocks args)
(W4.SomeSymFn sym) -- ^ function that represents the loop invariant
(Some (Ctx.Assignment (W4.SymExpr sym))) -- ^ arguments to the loop invariant
(W4.Pred sym) -- ^ predicate that represents the loop condition
-- | Finally, we stitch everything we have found together into the rest of the program.
-- Starting from the loop header one final time, we now force execution to exit the loop
-- and continue into the rest of the program.
| AfterFixpoint
(FixpointRecord sym wptr blocks args)
-- | Data about the loop that we incrementally compute as we approach fixpoint.
data FixpointRecord sym wptr blocks args = FixpointRecord
{
-- | Block identifier of the head of the loop
fixpointBlockId :: C.BlockID blocks args
-- | identifier for the currently-active assumption frame related to this fixpoint computation
, fixpointAssumptionFrameIdentifier :: C.FrameIdentifier
-- | Map from introduced widening variables to prestate value before the loop starts,
-- and to the value computed in a single loop iteration, assuming we return to the
-- loop header. These variables may appear only in either registers or memory.
, fixpointSubstitution :: MapF (W4.SymExpr sym) (FixpointEntry sym)
-- | Prestate values of the Crucible registers when the loop header is first encountered.
, fixpointRegMap :: C.RegMap sym args
-- | Triples are (blockId, offset, size) to bitvector-typed entries ( bitvector only/not pointers )
, fixpointMemSubstitution :: Map (MemLocation sym wptr) (MemFixpointEntry sym wptr)
, fixpointEqualitySubstitution :: MapF (W4.SymExpr sym) (W4.SymExpr sym)
-- | The loop index variable
, fixpointIndex :: W4.SymBV sym wptr
}
data CallFrameContext sym wptr ext init ret blocks = CallFrameContext
{ callFrameContextFixpointStates :: MapF (C.BlockID blocks) (FixpointState sym wptr blocks)
, callFrameContextLoopHeaders :: [C.Some (C.BlockID blocks)]
, callFrameContextCFG :: C.CFG ext blocks init ret
, callFrameContextParentLoop :: Map (C.Some (C.BlockID blocks)) (C.Some (C.BlockID blocks))
, callFrameContextLoopHeaderBlockIds :: Set (C.Some (C.BlockID blocks))
}
data CallFrameHandle init ret blocks = CallFrameHandle (C.FnHandle init ret) (Ctx.Assignment (Ctx.Assignment C.TypeRepr) blocks)
deriving (Eq, Ord, Show)
data SomeCallFrameContext sym wptr ext init ret =
forall blocks . SomeCallFrameContext (CallFrameContext sym wptr ext init ret blocks)
unwrapSomeCallFrameContext ::
Ctx.Assignment (Ctx.Assignment C.TypeRepr) blocks ->
SomeCallFrameContext sym wptr ext init ret ->
CallFrameContext sym wptr ext init ret blocks
unwrapSomeCallFrameContext blocks_repr (SomeCallFrameContext ctx) =
case W4.testEquality blocks_repr (fmapFC C.blockInputs $ C.cfgBlockMap $ callFrameContextCFG ctx) of
Just Refl -> ctx
Nothing -> C.panic "SimpleLoopFixpoint.unwrapSomeCallFrameContext" ["type mismatch"]
data ExecutionFeatureContext sym wptr ext = ExecutionFeatureContext
{ executionFeatureContextFixpointStates :: C.FnHandleMap (SomeCallFrameContext sym wptr ext)
, executionFeatureContextInvPreds :: [W4.SomeSymFn sym]
, executionFeatureContextLoopFunEquivConds :: [W4.Pred sym]
}
callFrameContextLookup ::
CallFrameHandle init ret blocks ->
ExecutionFeatureContext sym wptr ext ->
CallFrameContext sym wptr ext init ret blocks
callFrameContextLookup (CallFrameHandle hdl blocks_repr) ctx =
unwrapSomeCallFrameContext blocks_repr $
fromMaybe (C.panic "SimpleLoopFixpoint.callFrameContextLookup" ["missing call frame context", show hdl]) $
C.lookupHandleMap hdl (executionFeatureContextFixpointStates ctx)
callFrameContextUpdate ::
CallFrameHandle init ret blocks ->
(CallFrameContext sym wptr ext init ret blocks -> CallFrameContext sym wptr ext init ret blocks) ->
ExecutionFeatureContext sym wptr ext ->
ExecutionFeatureContext sym wptr ext
callFrameContextUpdate (CallFrameHandle hdl blocks_repr) f ctx =
ctx
{ executionFeatureContextFixpointStates = C.updateHandleMap
(SomeCallFrameContext . f . unwrapSomeCallFrameContext blocks_repr)
hdl
(executionFeatureContextFixpointStates ctx)
}
callFrameContextLookup' ::
CallFrameHandle init ret blocks ->
C.BlockID blocks args ->
ExecutionFeatureContext sym wptr ext ->
Maybe (FixpointState sym wptr blocks args)
callFrameContextLookup' hdl bid ctx =
MapF.lookup bid $ callFrameContextFixpointStates $ callFrameContextLookup hdl ctx
callFrameContextInsert ::
CallFrameHandle init ret blocks ->
C.BlockID blocks args ->
FixpointState sym wptr blocks args ->
ExecutionFeatureContext sym wptr ext ->
ExecutionFeatureContext sym wptr ext
callFrameContextInsert hdl bid fs =
callFrameContextUpdate hdl $
\ctx -> ctx { callFrameContextFixpointStates = MapF.insert bid fs (callFrameContextFixpointStates ctx) }
callFrameContextPush ::
CallFrameHandle init ret blocks ->
C.Some (C.BlockID blocks) ->
ExecutionFeatureContext sym wptr ext ->
ExecutionFeatureContext sym wptr ext
callFrameContextPush hdl bid =
callFrameContextUpdate hdl $
\ctx -> ctx { callFrameContextLoopHeaders = bid : callFrameContextLoopHeaders ctx }
-- | Precondition: the context's 'callFrameContextLoopHeaders' should be
-- non-empty.
callFrameContextPop ::
CallFrameHandle init ret blocks ->
ExecutionFeatureContext sym wptr ext ->
ExecutionFeatureContext sym wptr ext
callFrameContextPop hdl =
callFrameContextUpdate hdl $
\ctx -> ctx { callFrameContextLoopHeaders =
case callFrameContextLoopHeaders ctx of
_:hdrs -> hdrs
[] -> C.panic "callFrameContextPop"
["Empty callFrameContextLoopHeaders"] }
callFrameContextPeek ::
CallFrameHandle init ret blocks ->
ExecutionFeatureContext sym wptr ext ->
Maybe (C.Some (C.BlockID blocks))
callFrameContextPeek hdl ctx =
listToMaybe $ callFrameContextLoopHeaders $ callFrameContextLookup hdl ctx
callFrameContextLoopHeaderBlockIds' ::
CallFrameHandle init ret blocks ->
ExecutionFeatureContext sym wptr ext ->
Set (C.Some (C.BlockID blocks))
callFrameContextLoopHeaderBlockIds' hdl =
callFrameContextLoopHeaderBlockIds . callFrameContextLookup hdl
callFrameContextParentLoop' ::
CallFrameHandle init ret blocks ->
ExecutionFeatureContext sym wptr ext ->
Map (C.Some (C.BlockID blocks)) (C.Some (C.BlockID blocks))
callFrameContextParentLoop' hdl =
callFrameContextParentLoop . callFrameContextLookup hdl
executionFeatureContextAddCallFrameContext ::
CallFrameHandle init ret blocks ->
CallFrameContext sym wptr ext init ret blocks ->
ExecutionFeatureContext sym wptr ext ->
ExecutionFeatureContext sym wptr ext
executionFeatureContextAddCallFrameContext (CallFrameHandle hdl _blocks_repr) ctx context =
context
{ executionFeatureContextFixpointStates =
C.insertHandleMap hdl (SomeCallFrameContext ctx) (executionFeatureContextFixpointStates context)
}
executionFeatureContextAddInvPred ::
W4.SomeSymFn sym ->
ExecutionFeatureContext sym wptr ext ->
ExecutionFeatureContext sym wptr ext
executionFeatureContextAddInvPred inv_pred context =
context { executionFeatureContextInvPreds = inv_pred : executionFeatureContextInvPreds context }
executionFeatureContextAddLoopFunEquivCond ::
W4.Pred sym ->
ExecutionFeatureContext sym wptr ext ->
ExecutionFeatureContext sym wptr ext
executionFeatureContextAddLoopFunEquivCond cond context =
context { executionFeatureContextLoopFunEquivConds = cond : executionFeatureContextLoopFunEquivConds context }
newtype FixpointMonad sym a =
FixpointMonad (StateT (MapF (W4.SymExpr sym) (FixpointEntry sym)) IO a)
deriving (Functor, Applicative, Monad, MonadIO, MonadFail)
deriving instance s ~ MapF (W4.SymExpr sym) (FixpointEntry sym) => MonadState s (FixpointMonad sym)
runFixpointMonad ::
FixpointMonad sym a ->
MapF (W4.SymExpr sym) (FixpointEntry sym) ->
IO (a, MapF (W4.SymExpr sym) (FixpointEntry sym))
runFixpointMonad (FixpointMonad m) = runStateT m
joinRegEntries ::
(?logMessage :: String -> IO (), C.IsSymInterface sym) =>
sym ->
Ctx.Assignment (C.RegEntry sym) ctx ->
Ctx.Assignment (C.RegEntry sym) ctx ->
FixpointMonad sym (Ctx.Assignment (C.RegEntry sym) ctx)
joinRegEntries sym = Ctx.zipWithM (joinRegEntry sym)
joinRegEntry ::
(?logMessage :: String -> IO (), C.IsSymInterface sym) =>
sym ->
C.RegEntry sym tp ->
C.RegEntry sym tp ->
FixpointMonad sym (C.RegEntry sym tp)
joinRegEntry sym left right = case C.regType left of
C.LLVMPointerRepr w
-- special handling for "don't care" registers coming from Macaw
| List.isPrefixOf "cmacaw_reg" (show $ W4.printSymNat $ C.llvmPointerBlock (C.regValue left))
, List.isPrefixOf "cmacaw_reg" (show $ W4.printSymExpr $ C.llvmPointerOffset (C.regValue left)) -> do
liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: cmacaw_reg"
return left
| C.llvmPointerBlock (C.regValue left) == C.llvmPointerBlock (C.regValue right) -> do
liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr"
subst <- get
if isJust (W4.testEquality (C.llvmPointerOffset (C.regValue left)) (C.llvmPointerOffset (C.regValue right)))
then do
liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: left == right"
return left
else case MapF.lookup (C.llvmPointerOffset (C.regValue left)) subst of
Just join_entry -> do
liftIO $ ?logMessage $
"SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: Just: "
++ show (W4.printSymExpr $ bodyValue join_entry)
++ " -> "
++ show (W4.printSymExpr $ C.llvmPointerOffset (C.regValue right))
put $ MapF.insert
(C.llvmPointerOffset (C.regValue left))
(join_entry { bodyValue = C.llvmPointerOffset (C.regValue right) })
subst
return left
Nothing -> do
liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: Nothing"
join_variable <- liftIO $ W4.freshConstant sym (W4.safeSymbol "reg_join_var") (W4.BaseBVRepr w)
let join_entry = FixpointEntry
{ headerValue = C.llvmPointerOffset (C.regValue left)
, bodyValue = C.llvmPointerOffset (C.regValue right)
}
put $ MapF.insert join_variable join_entry subst
return $ C.RegEntry (C.LLVMPointerRepr w) $ C.LLVMPointer (C.llvmPointerBlock (C.regValue left)) join_variable
| Just{} <- W4.asConcrete (C.llvmPointerOffset (C.regValue left)) -> do
return $ C.RegEntry (C.LLVMPointerRepr w) $ C.LLVMPointer (C.llvmPointerBlock (C.regValue left)) (C.llvmPointerOffset (C.regValue left))
| otherwise ->
fail $
"SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: unsupported pointer base join: "
++ show (C.ppPtr $ C.regValue left)
++ " \\/ "
++ show (C.ppPtr $ C.regValue right)
C.BoolRepr
| List.isPrefixOf "cmacaw" (show $ W4.printSymExpr $ C.regValue left) -> do
liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: cmacaw_reg"
return left
| otherwise -> do
liftIO $ ?logMessage $
"SimpleLoopFixpoint.joinRegEntry: BoolRepr:"
++ show (W4.printSymExpr $ C.regValue left)
++ " \\/ "
++ show (W4.printSymExpr $ C.regValue right)
join_varaible <- liftIO $ W4.freshConstant sym (W4.safeSymbol "macaw_reg") W4.BaseBoolRepr
return $ C.RegEntry C.BoolRepr join_varaible
C.StructRepr field_types -> do
liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: StructRepr"
C.RegEntry (C.regType left) <$> fmapFC (C.RV . C.regValue) <$> joinRegEntries sym
(Ctx.generate (Ctx.size field_types) $ \i ->
C.RegEntry (field_types Ctx.! i) $ C.unRV $ (C.regValue left) Ctx.! i)
(Ctx.generate (Ctx.size field_types) $ \i ->
C.RegEntry (field_types Ctx.! i) $ C.unRV $ (C.regValue right) Ctx.! i)
_ -> fail $ "SimpleLoopFixpoint.joinRegEntry: unsupported type: " ++ show (C.regType left)
applySubstitutionRegEntries ::
C.IsSymInterface sym =>
sym ->
MapF (W4.SymExpr sym) (W4.SymExpr sym) ->
Ctx.Assignment (C.RegEntry sym) ctx ->
Ctx.Assignment (C.RegEntry sym) ctx
applySubstitutionRegEntries sym substitution = fmapFC (applySubstitutionRegEntry sym substitution)
applySubstitutionRegEntry ::
C.IsSymInterface sym =>
sym ->
MapF (W4.SymExpr sym) (W4.SymExpr sym) ->
C.RegEntry sym tp ->
C.RegEntry sym tp
applySubstitutionRegEntry sym substitution entry = case C.regType entry of
C.LLVMPointerRepr{} ->
entry
{ C.regValue = C.LLVMPointer
(C.llvmPointerBlock (C.regValue entry))
(MapF.findWithDefault
(C.llvmPointerOffset (C.regValue entry))
(C.llvmPointerOffset (C.regValue entry))
substitution)
}
C.BoolRepr ->
entry
C.StructRepr field_types ->
entry
{ C.regValue = fmapFC (C.RV . C.regValue) $
applySubstitutionRegEntries sym substitution $
Ctx.generate (Ctx.size field_types) $
\i -> C.RegEntry (field_types Ctx.! i) $ C.unRV $ (C.regValue entry) Ctx.! i
}
_ -> C.panic "SimpleLoopFixpoint.applySubstitutionRegEntry" ["unsupported type: " ++ show (C.regType entry)]
joinMem ::
forall sym wptr .
(C.IsSymInterface sym, C.HasPtrWidth wptr) =>
sym ->
C.MemImpl sym ->
C.MemWrites sym ->
IO (Map (MemLocation sym wptr) (MemFixpointEntry sym wptr))
joinMem sym mem_impl mem_writes = do
ranges <- maybe (fail "SimpleLoopFixpoint: unsupported symbolic pointers") return =<<
runMaybeT (C.writeRangesMem @_ @wptr sym $ C.memImplHeap mem_impl)
mem_subst <- case mem_writes of
C.MemWrites [C.MemWritesChunkIndexed indexed_writes] -> Map.fromList . catMaybes <$> mapM
(\case
C.MemWrite ptr mem_source
| Just Refl <- W4.testEquality ?ptrWidth (C.ptrWidth ptr)
, Just blk <- W4.asNat (C.llvmPointerBlock ptr) -> do
sz <- maybe (fail "SimpleLoopFixpoint: unsupported MemSource") return =<<
runMaybeT (C.writeSourceSize sym (C.ptrWidth ptr) mem_source)
let mem_loc = MemLocation
{ memLocationBlock = blk
, memLocationOffset = C.llvmPointerOffset ptr
, memLocationSize = sz
}
is_loop_local <- and <$> mapM
(\(prev_off, prev_sz) -> do
disjoint_pred <- C.buildDisjointRegionsAssertionWithSub
sym
ptr
sz
(C.LLVMPointer (C.llvmPointerBlock ptr) prev_off)
prev_sz
return $ W4.asConstantPred disjoint_pred == Just True)
(Map.findWithDefault [] blk ranges)
if not is_loop_local then do
mem_entry <- case mem_source of
C.MemStore _ storage_type _ ->
case W4.mkNatRepr $ C.bytesToBits (C.typeEnd 0 storage_type) of
C.Some bv_width
| Just C.LeqProof <- W4.testLeq (W4.knownNat @1) bv_width -> do
join_variable <- W4.freshConstant sym (W4.safeSymbol "mem_join_var") (W4.BaseBVRepr bv_width)
return $ MemStoreFixpointEntry join_variable storage_type
| otherwise ->
C.panic
"SimpleLoopFixpoint.simpleLoopFixpoint"
["unexpected storage type " ++ show storage_type]
C.MemArrayStore arr _ -> do
join_variable <- W4.freshConstant sym (W4.safeSymbol "mem_join_var") (W4.exprType arr)
return $ MemArrayFixpointEntry join_variable sz
_ -> fail "SimpleLoopFixpoint.joinMem: unsupported MemSource"
return $ Just (mem_loc, mem_entry)
else
return Nothing
_ -> fail $ "SimpleLoopFixpoint: not MemWrite: " ++ show (C.ppMemWrites mem_writes))
(List.concat $ IntMap.elems indexed_writes)
C.MemWrites [] -> return Map.empty
_ -> fail $ "SimpleLoopFixpoint: not MemWritesChunkIndexed: " ++ show (C.ppMemWrites mem_writes)
checkDisjointRegions sym $ Map.keys mem_subst
return mem_subst
checkDisjointRegions ::
(C.IsSymInterface sym, C.HasPtrWidth wptr) =>
sym ->
[MemLocation sym wptr] ->
IO ()
checkDisjointRegions sym = \case
hd_mem_loc : tail_mem_locs -> do
mapM_ (checkDisjointRegions' sym hd_mem_loc) tail_mem_locs
checkDisjointRegions sym tail_mem_locs
[] -> return ()
checkDisjointRegions' ::
(C.IsSymInterface sym, C.HasPtrWidth wptr) =>
sym ->
MemLocation sym wptr ->
MemLocation sym wptr ->
IO ()
checkDisjointRegions' sym mem_loc1 mem_loc2 = do
ptr1 <- memLocationPtr sym mem_loc1
ptr2 <- memLocationPtr sym mem_loc2
disjoint_pred <- C.buildDisjointRegionsAssertionWithSub
sym
ptr1
(memLocationSize mem_loc1)
ptr2
(memLocationSize mem_loc2)
when (W4.asConstantPred disjoint_pred /= Just True) $
fail $
"SimpleLoopFixpoint: non-disjoint ranges: off1="
++ show (W4.printSymExpr $ C.llvmPointerOffset ptr1)
++ ", sz1="
++ show (W4.printSymExpr $ memLocationSize mem_loc1)
++ ", off2="
++ show (W4.printSymExpr $ C.llvmPointerOffset ptr2)
++ ", sz2="
++ show (W4.printSymExpr $ memLocationSize mem_loc2)
loadMemJoinVariables ::
(C.IsSymBackend sym bak, C.HasPtrWidth wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) =>
bak ->
C.MemImpl sym ->
Map (MemLocation sym wptr) (MemFixpointEntry sym wptr) ->
IO (MapF (W4.SymExpr sym) (W4.SymExpr sym))
loadMemJoinVariables bak mem subst =
let sym = C.backendGetSym bak in
MapF.fromList . catMaybes <$> mapM
(\(mem_loc, mem_entry) -> do
ptr <- memLocationPtr sym mem_loc
case mem_entry of
MemStoreFixpointEntry join_variable storage_type -> do
val <- C.doLoad bak mem ptr storage_type (C.LLVMPointerRepr $ W4.bvWidth join_variable) C.noAlignment
case W4.asNat (C.llvmPointerBlock val) of
Just 0 -> return $ Just $ MapF.Pair join_variable $ C.llvmPointerOffset val
_ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables: unexpected val:" ++ show (C.ppPtr val)
-- foo <- C.loadRaw sym mem ptr storage_type C.noAlignment
-- case foo of
-- C.NoErr _p val' -> do
-- val <- C.unpackMemValue sym (C.LLVMPointerRepr $ W4.bvWidth join_variable) val'
-- case W4.asNat (C.llvmPointerBlock val) of
-- Just 0 -> return $ Just $ MapF.Pair join_variable $ C.llvmPointerOffset val
-- _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables: unexpected val:" ++ show (C.ppPtr val)
-- C.Err{} -> -- return Nothing
-- fail $ "SimpleLoopFixpoint.loadMemJoinVariables: loadRaw failed"
MemArrayFixpointEntry join_variable _size -> do
-- TODO: handle arrays
maybe_allocation_array <- C.asMemAllocationArrayStore sym ?ptrWidth ptr (C.memImplHeap mem)
case maybe_allocation_array of
Just (ok, arr, _arr_sz) | Just True <- W4.asConstantPred ok -> do
return $ Just $ MapF.Pair join_variable arr
_ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables")
(Map.toAscList subst)
storeMemJoinVariables ::
(C.IsSymBackend sym bak, C.HasPtrWidth wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) =>
bak ->
C.MemImpl sym ->
Map (MemLocation sym wptr) (MemFixpointEntry sym wptr) ->
MapF (W4.SymExpr sym) (W4.SymExpr sym) ->
IO (C.MemImpl sym)
storeMemJoinVariables bak mem mem_subst eq_subst = do
let sym = C.backendGetSym bak
foldlM
(\mem_acc (mem_loc, mem_entry) -> do
ptr <- memLocationPtr sym mem_loc
case mem_entry of
MemStoreFixpointEntry join_variable storage_type -> do
C.doStore bak mem_acc ptr (C.LLVMPointerRepr $ W4.bvWidth join_variable) storage_type C.noAlignment =<<
C.llvmPointer_bv sym (findWithDefaultKey eq_subst join_variable)
MemArrayFixpointEntry join_variable size -> do
C.doArrayStore bak mem_acc ptr C.noAlignment (findWithDefaultKey eq_subst join_variable) size)
-- (heap, p1, p2) <- C.writeArrayMem
-- sym
-- ?ptrWidth
-- ptr
-- C.noAlignment
-- (findWithDefaultKey eq_subst join_variable)
-- (Just size)
-- (C.memImplHeap mem_acc)
-- return $ mem_acc { C.memImplHeap = heap })
mem
(Map.toAscList mem_subst)
memLocationPtr ::
C.IsSymInterface sym =>
sym ->
MemLocation sym wptr ->
IO (C.LLVMPtr sym wptr)
memLocationPtr sym (MemLocation { memLocationBlock = blk, memLocationOffset = off }) =
C.LLVMPointer <$> W4.natLit sym blk <*> return off
dropMemStackFrame :: C.IsSymInterface sym => C.MemImpl sym -> (C.MemImpl sym, C.MemAllocs sym, C.MemWrites sym)
dropMemStackFrame mem = case (C.memImplHeap mem) ^. C.memState of
(C.StackFrame _ _ _ (a, w) s) -> ((mem { C.memImplHeap = (C.memImplHeap mem) & C.memState .~ s }), a, w)
_ -> C.panic "SimpleLoopFixpoint.dropMemStackFrame" ["not a stack frame:", show (C.ppMem $ C.memImplHeap mem)]
filterSubstitution ::
C.IsSymInterface sym =>
sym ->
MapF (W4.SymExpr sym) (FixpointEntry sym) ->
MapF (W4.SymExpr sym) (FixpointEntry sym)
filterSubstitution sym substitution =
-- TODO: fixpoint
let uninterp_constants = foldMapF
(Set.map (C.mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym . bodyValue)
substitution
in
MapF.filterWithKey (\variable _entry -> Set.member (C.Some variable) uninterp_constants) substitution
loopIndexLinearSubstitution ::
(C.IsSymInterface sym, C.HasPtrWidth wptr, MonadIO m) =>
sym ->
W4.SymBV sym wptr ->
MapF (W4.SymExpr sym) (FixpointEntry sym) ->
m (MapF (W4.SymExpr sym) (W4.SymExpr sym))
loopIndexLinearSubstitution sym index_variable =
MapF.traverseMaybeWithKey
(\variable entry -> case W4.testEquality (W4.exprType variable) (W4.exprType index_variable) of
Just Refl -> do
diff <- liftIO $ W4.bvSub sym (bodyValue entry) variable
case W4.asBV diff of
Just{} -> liftIO $ Just <$> (W4.bvAdd sym (headerValue entry) =<< W4.bvMul sym index_variable diff)
Nothing -> return Nothing
Nothing -> return Nothing)
-- find widening variables that are actually the same (up to syntactic equality)
-- and can be substituted for each other
uninterpretedConstantEqualitySubstitution ::
(C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, MonadIO m, MonadFail m, ?logMessage :: String -> IO ()) =>
sym ->
MapF (W4.SymExpr sym) (FixpointEntry sym) ->
m (MapF (W4.SymExpr sym) (FixpointEntry sym), MapF (W4.SymExpr sym) (W4.SymExpr sym))
uninterpretedConstantEqualitySubstitution sym substitution = do
let reverse_substitution = MapF.foldlWithKey'
(\accumulator variable entry -> MapF.insert entry variable accumulator)
MapF.empty
substitution
let uninterpreted_constant_substitution =
MapF.filterWithKey (\variable entry -> isNothing $ W4.testEquality variable entry) $
fmapF (\entry -> fromJust $ MapF.lookup entry reverse_substitution)
substitution
let normal_substitution = MapF.filterWithKey
(\variable _entry -> isNothing $ MapF.lookup variable uninterpreted_constant_substitution)
substitution
liftIO $ ?logMessage "vars:"
mapM_
(\(MapF.Pair variable entry) -> do
let body_vars = Set.map (C.mapSome $ W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry
liftIO $ ?logMessage $ show (W4.printSymExpr variable) ++ " :: "++ show (W4.exprType variable) ++ " -> " ++ (show $ Set.map (C.viewSome $ show . W4.printSymExpr) $ body_vars))
(MapF.toList normal_substitution)
foo <- MapF.fromList <$> filterM
(\(MapF.Pair variable entry) -> do
let body_vars = Set.map (C.mapSome $ W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry
if Set.notMember (C.Some variable) body_vars then do
let lalala = runIdentity $ MapF.fromKeysM (return . W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry
let foobar = fmapF headerValue $ MapF.mapMaybe (\v -> MapF.lookup v normal_substitution) lalala
bar <- liftIO $ W4.isEq sym (headerValue entry) =<< W4.substituteBoundVars sym foobar (bodyValue entry)
liftIO $ ?logMessage $ "la: " ++ (show $ W4.printSymExpr variable)
liftIO $ ?logMessage $ "headerValue entry: " ++ (show $ W4.printSymExpr $ headerValue entry)
liftIO $ ?logMessage $ "bodyValue entry:" ++ (show $ W4.printSymExpr $ bodyValue entry)
liftIO $ ?logMessage $ "bar: " ++ (show $ W4.printSymExpr $ bar)
if Just True == W4.asConstantPred bar then do
liftIO $ ?logMessage "lala"
return True
else do
notbar <- liftIO $ W4.notPred sym bar
lala <- liftIO $ W4.runZ3InOverride sym (W4.defaultLogData { W4.logVerbosity = 2 }) [notbar] $ return . W4.isUnsat
when lala $ do
liftIO $ ?logMessage "lalala"
return lala
else
return False)
(MapF.toList normal_substitution)
unless (Set.disjoint (Set.fromList $ MapF.keys foo) (foldMapF (Set.map (C.mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym) $ fmapF bodyValue foo)) $
fail "SimpleLoopFixpoint: uninterpretedConstantEqualitySubstitution: not disjoint"
return
( MapF.mergeWithKey (\_ _ _ -> Nothing) id (const MapF.empty) normal_substitution foo -- difference
, MapF.mergeWithKey (\_ _ -> Just) id id uninterpreted_constant_substitution $ fmapF bodyValue foo -- union
)
-- -- | Given the WTO analysis results, find the nth loop.
-- -- Return the identifier of the loop header, and a list of all the blocks
-- -- that are part of the loop body. It is at this point that we check
-- -- that the loop has the necessary properties; there must be a single
-- -- entry point to the loop, and it must have a single back-edge. Otherwise,
-- -- the analysis will not work correctly.
-- computeLoopBlocks :: forall ext blocks init ret k .
-- (k ~ C.Some (C.BlockID blocks)) =>
-- C.CFG ext blocks init ret ->
-- Integer ->
-- IO (k, [k])
-- computeLoopBlocks cfg loopNum =
-- case List.genericDrop loopNum (Map.toList loop_map) of
-- [] -> fail ("Did not find " ++ show loopNum ++ " loop headers")
-- (p:_) -> do checkSingleEntry p
-- checkSingleBackedge p
-- return p
-- where
-- -- There should be exactly one block which is not part of the loop body that
-- -- can jump to @hd@.
-- checkSingleEntry :: (k,[k]) -> IO ()
-- checkSingleEntry (hd, body) =
-- case filter (\x -> not (elem x body) && elem hd (C.cfgSuccessors cfg x)) allReachable of
-- [_] -> return ()
-- _ -> fail "SimpleLoopInvariant feature requires a single-entry loop!"
-- -- There should be exactly on block in the loop body which can jump to @hd@.
-- checkSingleBackedge :: (k,[k]) -> IO ()
-- checkSingleBackedge (hd, body) =
-- case filter (\x -> elem hd (C.cfgSuccessors cfg x)) body of
-- [_] -> return ()
-- _ -> fail "SimpleLoopInvariant feature requires a loop with a single backedge!"
-- flattenWTOComponent = \case
-- C.SCC C.SCCData{..} -> wtoHead : concatMap flattenWTOComponent wtoComps
-- C.Vertex v -> [v]
-- loop_map = Map.fromList $ mapMaybe
-- (\case
-- C.SCC C.SCCData{..} -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps)
-- C.Vertex{} -> Nothing)
-- wto
-- allReachable = concatMap flattenWTOComponent wto
-- wto = C.cfgWeakTopologicalOrdering cfg
-- | This execution feature is designed to allow a limited form of
-- verification for programs with unbounded looping structures.
--
-- It is currently highly experimental and has many limitations.
-- Most notably, it only really works properly for functions
-- consisting of a single, non-nested loop with a single exit point.
-- Moreover, the loop must have an indexing variable that counts up
-- from a starting point by a fixed stride amount.
--
-- Currently, these assumptions about the loop structure are not
-- checked.
--
-- The basic use case here is for verifying functions that loop
-- through an array of data of symbolic length. This is done by
-- providing a \""fixpoint function\" which describes how the live
-- values in the loop at an arbitrary iteration are used to compute
-- the final values of those variables before execution leaves the
-- loop. The number and order of these variables depends on
-- internal details of the representation, so is relatively fragile.
simpleLoopFixpoint ::
(C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) =>
sym ->
C.CFG ext blocks init ret {- ^ The function we want to verify -} ->
C.GlobalVar C.Mem {- ^ global variable representing memory -} ->
Maybe (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), Maybe (W4.Pred sym))) ->
IO (C.ExecutionFeature p sym ext rtp, IORef (ExecutionFeatureContext sym wptr ext))
simpleLoopFixpoint sym _cfg mem_var maybe_fixpoint_func = do
verbSetting <- W4.getOptionSetting W4.verbosity $ W4.getConfiguration sym
_verb <- fromInteger @Natural <$> W4.getOpt verbSetting
-- let loop_map = Map.fromList $ mapMaybe
-- (\case
-- scc@(C.SCC _) -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps)
-- C.Vertex{} -> Nothing)
-- (C.cfgWeakTopologicalOrdering cfg)
-- Doesn't really work if there are nested loops: looop datastructures will
-- overwrite each other. Currently no error message.
-- Really only works for single-exit loops; need a message for that too.
-- let flattenWTOComponent = \case
-- C.SCC C.SCCData{..} -> wtoHead : concatMap flattenWTOComponent wtoComps
-- C.Vertex v -> [v]
-- let loop_map = Map.fromList $ mapMaybe
-- (\case
-- C.SCC C.SCCData{..} -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps)
-- C.Vertex{} -> Nothing)
-- (C.cfgWeakTopologicalOrdering cfg)
-- let parent_wto_component = C.parentWTOComponent $ C.cfgWeakTopologicalOrdering cfg
-- fixpoint_state_ref <- newIORef $
-- FrameContext
-- { frameContextFixpointStates = MapF.empty
-- , frameContextLoopHeaders = []
-- , frameContextCFG = cfg
-- , frameContextParentLoop = parent_wto_component
-- , frameContextLoopHeaderBlockIds = Set.fromList $ Map.elems parent_wto_component
-- }
fixpoint_state_ref <- newIORef $
ExecutionFeatureContext
{ executionFeatureContextFixpointStates = C.emptyHandleMap
, executionFeatureContextInvPreds = []
, executionFeatureContextLoopFunEquivConds = []
}
-- initializeCallFrameContext cfg fixpoint_state_ref
return $ (, fixpoint_state_ref) $ C.ExecutionFeature $ \exec_state -> do
-- let ?logMessage = \msg -> when (_verb >= 3) $ do
let ?logMessage = \msg -> do
let h = C.printHandle $ C.execStateContext exec_state
System.IO.hPutStrLn h msg
System.IO.hFlush h
-- cfg_handle <- C.cfgHandle . callFrameContextCFG <$> readIORef fixpoint_state_ref
-- cfg_block_map <- C.cfgBlockMap . callFrameContextCFG <$> readIORef fixpoint_state_ref
-- parent_loop_map <- callFrameContextParentLoop <$> readIORef fixpoint_state_ref
-- loop_header_block_ids <- callFrameContextLoopHeaderBlockIds <$> readIORef fixpoint_state_ref
-- maybe_some_loop_block_id <- callFrameContextPeek <$> readIORef fixpoint_state_ref
C.withBackend (C.execStateContext exec_state) $ \bak -> case exec_state of
C.RunningState (C.RunBlockStart block_id) sim_state
| SomeCallFrameHandle call_frame_handle <- callFrameHandle (sim_state ^. C.stateCrucibleFrame) -> do
loop_header_block_ids <- callFrameContextLoopHeaderBlockIds' call_frame_handle <$> readIORef fixpoint_state_ref
if Set.member (C.Some block_id) loop_header_block_ids then do
?logMessage $ "!!!SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id
advanceFixpointState bak mem_var maybe_fixpoint_func call_frame_handle block_id sim_state fixpoint_state_ref
else do
?logMessage $ "SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id
return C.ExecutionFeatureNoChange
-- | C.SomeHandle cfg_handle == C.frameHandle (sim_state ^. C.stateCrucibleFrame)
-- -- make sure the types match
-- , Just Refl <- W4.testEquality
-- (fmapFC C.blockInputs cfg_block_map)
-- (fmapFC C.blockInputs $ C.frameBlockMap $ sim_state ^. C.stateCrucibleFrame)
-- -- loop map is what we computed above, is this state at a loop header
-- , Set.member (C.Some block_id) loop_header_block_ids ->
-- advanceFixpointState bak mem_var maybe_fixpoint_func cfg_handle block_id sim_state fixpoint_state_ref
-- | otherwise -> do
-- ?logMessage $ "SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id
-- return C.ExecutionFeatureNoChange
-- TODO: maybe need to rework this, so that we are sure to capture even concrete exits from the loop.
C.SymbolicBranchState branch_condition true_frame false_frame _target sim_state
| JustPausedFrameTgtId true_frame_some_block_id <- pausedFrameTgtId true_frame
, JustPausedFrameTgtId false_frame_some_block_id <- pausedFrameTgtId false_frame
, SomeCallFrameHandle call_frame_handle <- callFrameHandle (sim_state ^. C.stateCrucibleFrame) -> do
maybe_some_loop_block_id <- callFrameContextPeek call_frame_handle <$> readIORef fixpoint_state_ref
parent_loop_map <- callFrameContextParentLoop' call_frame_handle <$> readIORef fixpoint_state_ref
-- , C.SomeHandle cfg_handle == C.frameHandle (sim_state ^. C.stateCrucibleFrame)
-- , Just Refl <- W4.testEquality
-- (fmapFC C.blockInputs cfg_block_map)
-- (fmapFC C.blockInputs $ C.frameBlockMap $ sim_state ^. C.stateCrucibleFrame)
-- , Just (Some loop_block_id) <- maybe_some_loop_block_id
-- , true_frame_parent_loop_id <- Map.lookup true_frame_some_block_id parent_loop_map
-- , false_frame_parent_loop_id <- Map.lookup false_frame_some_block_id parent_loop_map
-- , true_frame_parent_loop_id /= maybe_some_loop_block_id || false_frame_parent_loop_id /= maybe_some_loop_block_id -> do
if| Just (Some loop_block_id) <- maybe_some_loop_block_id
, true_frame_parent_loop_id <- if true_frame_some_block_id /= C.Some loop_block_id then Map.lookup true_frame_some_block_id parent_loop_map else maybe_some_loop_block_id
, false_frame_parent_loop_id <- if false_frame_some_block_id /= C.Some loop_block_id then Map.lookup false_frame_some_block_id parent_loop_map else maybe_some_loop_block_id
, true_frame_parent_loop_id /= maybe_some_loop_block_id || false_frame_parent_loop_id /= maybe_some_loop_block_id -> do
?logMessage $ "!!!SimpleLoopFixpoint: SymbolicBranchState: " ++ show (true_frame_some_block_id, false_frame_some_block_id)
handleSymbolicBranch
bak
call_frame_handle
loop_block_id
branch_condition
true_frame
false_frame
true_frame_parent_loop_id
false_frame_parent_loop_id
sim_state
fixpoint_state_ref
| otherwise -> do
?logMessage $ "SimpleLoopFixpoint: SymbolicBranchState: " ++ show (W4.printSymExpr branch_condition, true_frame_some_block_id, false_frame_some_block_id)
return C.ExecutionFeatureNoChange
C.CallState _return_handler (C.CrucibleCall _block_id call_frame) _sim_state
| C.CallFrame { C._frameCFG = callee_cfg } <- call_frame -> do
initializeCallFrameContext callee_cfg fixpoint_state_ref
return C.ExecutionFeatureNoChange
C.TailCallState _value_from_value (C.CrucibleCall _block_id call_frame) _sim_state
| C.CallFrame { C._frameCFG = callee_cfg } <- call_frame -> do
initializeCallFrameContext callee_cfg fixpoint_state_ref
return C.ExecutionFeatureNoChange
_ -> return C.ExecutionFeatureNoChange
initializeCallFrameContext ::
(?logMessage :: String -> IO ()) =>
C.CFG ext blocks init ret ->
IORef (ExecutionFeatureContext sym wptr ext) ->
IO ()
initializeCallFrameContext cfg context_ref = do
?logMessage $ "SimpleLoopFixpoint: cfgHandle: " ++ show (C.cfgHandle cfg)
?logMessage $ "SimpleLoopFixpoint: cfg: " ++ show (toListFC (\b -> (C.Some (C.blockID b), C.nextBlocks b)) $ C.cfgBlockMap cfg)
?logMessage $ "SimpleLoopFixpoint: cfgWeakTopologicalOrdering: " ++ show (C.cfgWeakTopologicalOrdering cfg)
let parent_wto_component = C.parentWTOComponent $ C.cfgWeakTopologicalOrdering cfg
let call_frame_handle = CallFrameHandle (C.cfgHandle cfg) $ fmapFC C.blockInputs $ C.cfgBlockMap cfg
modifyIORef' context_ref $ executionFeatureContextAddCallFrameContext call_frame_handle $
CallFrameContext
{ callFrameContextFixpointStates = MapF.empty
, callFrameContextLoopHeaders = []
, callFrameContextCFG = cfg
, callFrameContextParentLoop = parent_wto_component
, callFrameContextLoopHeaderBlockIds = Set.fromList $ Map.elems parent_wto_component
}
initializeFixpointState ::
(C.IsSymBackend sym bak, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) =>
bak ->
C.GlobalVar C.Mem ->
CallFrameHandle init ret blocks ->
C.BlockID blocks args ->
C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) ->
IORef (ExecutionFeatureContext sym wptr ext) ->
IO (C.ExecutionFeatureResult p sym ext rtp)
initializeFixpointState bak mem_var call_frame_handle block_id sim_state fixpoint_state_ref = do
let sym = C.backendGetSym bak
assumption_frame_identifier <- C.pushAssumptionFrame bak
?logMessage $ "!!!SimpleLoopFixpoint: initializeFixpointState: block_id=" ++ show block_id ++ ", assumption_frame_identifier=" ++ show assumption_frame_identifier
index_var <- W4.freshConstant sym (W4.safeSymbol "index_var") W4.knownRepr
let mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals)
let res_mem_impl = mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" $ C.memImplHeap mem_impl }
modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $ ComputeFixpoint $
FixpointRecord
{ fixpointBlockId = block_id
, fixpointAssumptionFrameIdentifier = assumption_frame_identifier
, fixpointSubstitution = MapF.empty
, fixpointRegMap = sim_state ^. (C.stateCrucibleFrame . C.frameRegs)
, fixpointMemSubstitution = Map.empty
, fixpointEqualitySubstitution = MapF.empty
, fixpointIndex = index_var
}
modifyIORef' fixpoint_state_ref $ callFrameContextPush call_frame_handle $ Some block_id
return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $
sim_state & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl
advanceFixpointState ::
(C.IsSymBackend sym bak, sym ~ W4.ExprBuilder t st fs, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) =>
bak ->
C.GlobalVar C.Mem ->
Maybe (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), Maybe (W4.Pred sym))) ->
CallFrameHandle init ret blocks ->
C.BlockID blocks args ->
C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) ->
IORef (ExecutionFeatureContext sym wptr ext) ->
IO (C.ExecutionFeatureResult p sym ext rtp)
advanceFixpointState bak mem_var maybe_fixpoint_func call_frame_handle block_id sim_state fixpoint_state_ref = do
let sym = C.backendGetSym bak
fixpoint_state <- fromMaybe BeforeFixpoint <$> callFrameContextLookup' call_frame_handle block_id <$> readIORef fixpoint_state_ref
case fixpoint_state of
BeforeFixpoint -> do
?logMessage $ "SimpleLoopFixpoint: RunningState: BeforeFixpoint -> ComputeFixpoint"
mapM_ (\g -> print =<< C.ppProofObligation sym g) =<< (maybe [] C.goalsToList <$> C.getProofObligations bak)
initializeFixpointState bak mem_var call_frame_handle block_id sim_state fixpoint_state_ref
ComputeFixpoint fixpoint_record -> do
?logMessage $ "SimpleLoopFixpoint: RunningState: ComputeFixpoint: " ++ show block_id
proof_goals_and_assumptions_vars <- Set.map (mapSome $ W4.varExpr sym) <$>
(Set.union <$> C.proofObligationsUninterpConstants bak <*> C.pathConditionUninterpConstants bak)
(frame_assumptions, _) <- C.popAssumptionFrameAndObligations bak $ fixpointAssumptionFrameIdentifier fixpoint_record
loop_condition <- C.assumptionsPred sym frame_assumptions
-- widen the inductive condition
(join_reg_map, join_substitution) <- runFixpointMonad
(joinRegEntries sym
(C.regMap $ fixpointRegMap fixpoint_record)
(C.regMap $ sim_state ^. (C.stateCrucibleFrame . C.frameRegs))) $
fixpointSubstitution fixpoint_record
let body_mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals)
let (header_mem_impl, mem_allocs, mem_writes) = dropMemStackFrame body_mem_impl
when (C.sizeMemAllocs mem_allocs /= 0) $
fail "SimpleLoopFixpoint: unsupported memory allocation in loop body."
-- widen the memory
mem_substitution_candidate <- joinMem sym header_mem_impl mem_writes
-- check that the mem substitution always computes the same footprint on every iteration (!?!)
mem_substitution <- if Map.null (fixpointMemSubstitution fixpoint_record)
then return mem_substitution_candidate
else if Map.keys mem_substitution_candidate == Map.keys (fixpointMemSubstitution fixpoint_record)
then return $ fixpointMemSubstitution fixpoint_record
else fail "SimpleLoopFixpoint: unsupported memory writes change"
assumption_frame_identifier <- C.pushAssumptionFrame bak
-- check if we are done; if we did not introduce any new variables, we don't have to widen any more
if MapF.keys join_substitution == MapF.keys (fixpointSubstitution fixpoint_record) && Map.keys mem_substitution == Map.keys (fixpointMemSubstitution fixpoint_record)
-- we found the fixpoint, get ready to wrap up
then do
?logMessage $
"SimpleLoopFixpoint: RunningState: ComputeFixpoint -> CheckFixpoint"
-- we have delayed populating the main substitution map with
-- memory variables, so we have to do that now
header_mem_substitution <- loadMemJoinVariables bak header_mem_impl $
fixpointMemSubstitution fixpoint_record
body_mem_substitution <- loadMemJoinVariables bak body_mem_impl $
fixpointMemSubstitution fixpoint_record
-- drop variables that don't appear along some back edge
let union_substitution' = filterSubstitution sym $
MapF.union join_substitution $
-- this implements zip, because the two maps have the same keys
MapF.intersectWithKeyMaybe
(\_k x y -> Just $ FixpointEntry{ headerValue = x, bodyValue = y })
header_mem_substitution
body_mem_substitution
loop_index_linear_substitution <- loopIndexLinearSubstitution sym (fixpointIndex fixpoint_record) union_substitution'
let union_substitution = MapF.filterWithKey
(\variable _entry -> MapF.notMember variable loop_index_linear_substitution)
union_substitution'
-- try to unify widening variables that have the same values
(normal_substitution', equality_substitution') <- uninterpretedConstantEqualitySubstitution sym union_substitution
zero_bv <- W4.bvZero sym knownNat
one_bv <- W4.bvOne sym knownNat
add_index_one <- W4.bvAdd sym (fixpointIndex fixpoint_record) one_bv
let normal_substitution = MapF.insert
(fixpointIndex fixpoint_record)
FixpointEntry
{ headerValue = zero_bv
, bodyValue = add_index_one
}
normal_substitution'
let equality_substitution = MapF.union equality_substitution' loop_index_linear_substitution
?logMessage $ "loop_index_linear_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList loop_index_linear_substitution)
?logMessage $ "normal_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList normal_substitution)
?logMessage $ "equality_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList equality_substitution)
-- unify widening variables in the register subst
let res_reg_map = applySubstitutionRegEntries sym equality_substitution join_reg_map
-- unify widening varialbes in the memory subst
res_mem_impl <- storeMemJoinVariables
bak
(header_mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" (C.memImplHeap header_mem_impl) })
mem_substitution
equality_substitution
let body_values_vars = foldMap (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym . bodyValue) $
MapF.elems normal_substitution
let header_values_vars = foldMap (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym . headerValue) $
MapF.elems normal_substitution
-- let all_vars = Set.union proof_goals_and_assumptions_vars $ Set.union body_values_vars header_values_vars
let all_vars' = Set.insert (Some $ fixpointIndex fixpoint_record) proof_goals_and_assumptions_vars
let all_vars = Set.filter
(\(Some variable) -> MapF.notMember variable equality_substitution)
all_vars'
-- let some_uninterpreted_constants = Ctx.fromList $ Set.toList all_vars
let filtered_vars = Set.filter
(\(Some variable) ->
not (List.isPrefixOf "cundefined_" $ show $ W4.printSymExpr variable)
&& not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable)
&& not (List.isPrefixOf "cnoSatisfyingWrite" $ show $ W4.printSymExpr variable))
all_vars
let some_uninterpreted_constants = Ctx.fromList $ Set.toList filtered_vars
-- let implicit_vars = Set.filter
-- (\(Some variable) ->
-- not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable)
-- && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable)
-- && not (List.isPrefixOf "cundefined_" $ show $ W4.printSymExpr variable)
-- && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable)
-- && not (List.isPrefixOf "cnoSatisfyingWrite" $ show $ W4.printSymExpr variable))
-- all_vars
some_inv_pred <- case some_uninterpreted_constants of
Some uninterpreted_constants -> do
inv_pred <- W4.freshTotalUninterpFn
sym
(W4.safeSymbol "inv")
(fmapFC W4.exprType uninterpreted_constants)
W4.BaseBoolRepr
loc <- W4.getCurrentProgramLoc sym
header_inv <- W4.applySymFn sym inv_pred $
applySubstitutionFC (fmapF headerValue normal_substitution) uninterpreted_constants
C.addProofObligation bak $ C.LabeledPred header_inv $ C.SimError loc ""
inv <- W4.applySymFn sym inv_pred uninterpreted_constants
C.addAssumption bak $ C.GenericAssumption loc "inv" inv
return $ W4.SomeSymFn inv_pred
modifyIORef' fixpoint_state_ref $ executionFeatureContextAddInvPred some_inv_pred
?logMessage $
"proof_goals_and_assumptions_vars: "
++ show (map (viewSome W4.printSymExpr) $ Set.toList proof_goals_and_assumptions_vars)
?logMessage $
"body_values_vars: " ++ show (map (viewSome W4.printSymExpr) $ Set.toList body_values_vars)
?logMessage $
"header_values_vars: " ++ show (map (viewSome W4.printSymExpr) $ Set.toList header_values_vars)
?logMessage $
"uninterpreted_constants: " ++ show (map (viewSome W4.printSymExpr) $ Set.toList filtered_vars)
modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $
CheckFixpoint
FixpointRecord
{ fixpointBlockId = block_id
, fixpointAssumptionFrameIdentifier = assumption_frame_identifier
, fixpointSubstitution = normal_substitution
, fixpointRegMap = fixpointRegMap fixpoint_record
, fixpointMemSubstitution = mem_substitution
, fixpointEqualitySubstitution = equality_substitution
, fixpointIndex = fixpointIndex fixpoint_record
}
some_inv_pred
-- implicit_vars
some_uninterpreted_constants
loop_condition
return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $
sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ C.RegMap res_reg_map
& C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl
else do
?logMessage $
"SimpleLoopFixpoint: RunningState: ComputeFixpoint: -> ComputeFixpoint"
-- write any new widening variables into memory state
res_mem_impl <- storeMemJoinVariables bak
(header_mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" (C.memImplHeap header_mem_impl) })
mem_substitution
MapF.empty
modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $ ComputeFixpoint
FixpointRecord
{ fixpointBlockId = block_id
, fixpointAssumptionFrameIdentifier = assumption_frame_identifier
, fixpointSubstitution = join_substitution
, fixpointRegMap = C.RegMap join_reg_map
, fixpointMemSubstitution = mem_substitution
, fixpointEqualitySubstitution = MapF.empty
, fixpointIndex = fixpointIndex fixpoint_record
}
return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $
sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ C.RegMap join_reg_map
& C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl
CheckFixpoint fixpoint_record some_inv_pred some_uninterpreted_constants loop_condition -> do
?logMessage $
"SimpleLoopFixpoint: RunningState: "
++ "CheckFixpoint"
++ " -> "
++ "AfterFixpoint"
++ ": "
++ show block_id
loc <- W4.getCurrentProgramLoc sym
-- assert that the hypothesis we made about the loop termination condition is true
(_ :: ()) <- case (some_inv_pred, some_uninterpreted_constants) of
(W4.SomeSymFn inv_pred, Some uninterpreted_constants)
| Just Refl <- testEquality (W4.fnArgTypes inv_pred) (fmapFC W4.exprType uninterpreted_constants)
, Just Refl <- testEquality (W4.fnReturnType inv_pred) W4.BaseBoolRepr -> do
inv <- W4.applySymFn sym inv_pred $ applySubstitutionFC
(fmapF bodyValue $ fixpointSubstitution fixpoint_record)
uninterpreted_constants
C.addProofObligation bak $ C.LabeledPred inv $ C.SimError loc ""
| otherwise -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["type mismatch: CheckFixpoint"]
frame_assumptions <- C.popAssumptionFrame bak $ fixpointAssumptionFrameIdentifier fixpoint_record
-- body_mem_substitution <- loadMemJoinVariables bak body_mem_impl $ fixpointMemSubstitution fixpoint_record
-- let res_substitution = MapF.mapWithKey
-- (\variable fixpoint_entry ->
-- fixpoint_entry
-- { bodyValue = MapF.findWithDefault (bodyValue fixpoint_entry) variable body_mem_substitution
-- })
-- (fixpointSubstitution fixpoint_record)
-- ?logMessage $ "res_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList res_substitution)
-- match things up with the input function that describes the loop body behavior
fixpoint_substitution <- case maybe_fixpoint_func of
Just fixpoint_func -> do
-- (fixpoint_func_substitution, maybe_fixpoint_func_condition) <- fixpoint_func res_substitution loop_condition
correct_substitution <- traverseF
(\fixpoint_entry -> do
correct_body_value <- W4.substituteBoundVars sym (asBoundVarSubstitution sym $ fixpointEqualitySubstitution fixpoint_record) $ bodyValue fixpoint_entry
return $ fixpoint_entry
{ bodyValue = correct_body_value
})
(fixpointSubstitution fixpoint_record)
(fixpoint_func_substitution, maybe_fixpoint_func_condition) <- fixpoint_func correct_substitution loop_condition
-- (fixpoint_func_substitution, maybe_fixpoint_func_condition) <- fixpoint_func (fixpointSubstitution fixpoint_record) loop_condition
_ <- case maybe_fixpoint_func_condition of
Just fixpoint_func_condition -> do
bak_assumptions <- liftIO $ C.assumptionsPred sym =<< C.collectAssumptions bak
inv_assumption <- C.assumptionPred <$> headAssumption sym frame_assumptions
all_assumptions <- liftIO $ W4.andPred sym bak_assumptions inv_assumption
implication <- liftIO $ W4.impliesPred sym all_assumptions fixpoint_func_condition
modifyIORef' fixpoint_state_ref $ executionFeatureContextAddLoopFunEquivCond implication
-- tmp_frame_id <- C.pushAssumptionFrame bak
-- C.addProofObligation bak $ C.LabeledPred fixpoint_func_condition $ C.SimError loc ""
-- (_, obligations) <- C.popAssumptionFrameAndObligations bak tmp_frame_id
-- ?logMessage "before convertProofObligationsAsImplications"
-- implications <- C.convertProofObligationsAsImplications sym obligations
-- ?logMessage "after convertProofObligationsAsImplications"
-- forM_ implications $ \implication ->
-- modifyIORef' fixpoint_state_ref $ executionFeatureContextAddLoopFunEquivCond implication
Nothing -> return ()
?logMessage $ "fixpoint_func_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList fixpoint_func_substitution)
return fixpoint_func_substitution
Nothing -> return MapF.empty
let body_mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals)
let (header_mem_impl, _mem_allocs, _mem_writes) = dropMemStackFrame body_mem_impl
fixpoint_equality_substitution <- traverseF
(W4.substituteBoundVars sym $ asBoundVarSubstitution sym fixpoint_substitution) $
fixpointEqualitySubstitution fixpoint_record
let fixpoint_equality_substitution' = MapF.union fixpoint_substitution fixpoint_equality_substitution
let res_reg_map = C.RegMap $ applySubstitutionRegEntries sym fixpoint_equality_substitution' (C.regMap $ fixpointRegMap fixpoint_record)
res_mem_impl <- storeMemJoinVariables bak header_mem_impl (fixpointMemSubstitution fixpoint_record) fixpoint_equality_substitution'
(_ :: ()) <- case (some_inv_pred, some_uninterpreted_constants) of
(W4.SomeSymFn inv_pred, Some uninterpreted_constants)
| Just Refl <- testEquality (W4.fnArgTypes inv_pred) (fmapFC W4.exprType uninterpreted_constants)
, Just Refl <- testEquality (W4.fnReturnType inv_pred) W4.BaseBoolRepr -> do
inv <- W4.applySymFn sym inv_pred $ applySubstitutionFC fixpoint_substitution uninterpreted_constants
C.addAssumption bak $ C.GenericAssumption loc "" inv
| otherwise -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["type mismatch: CheckFixpoint"]
modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $
AfterFixpoint
-- fixpoint_record{ fixpointSubstitution = res_substitution }
fixpoint_record
return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $
sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ res_reg_map
& C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl
AfterFixpoint{} -> do
?logMessage $ "SimpleLoopFixpoint: RunningState: AfterFixpoint -> ComputeFixpoint"
initializeFixpointState bak mem_var call_frame_handle block_id sim_state fixpoint_state_ref
handleSymbolicBranch ::
(C.IsSymBackend sym bak, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) =>
bak ->
CallFrameHandle init ret blocks ->
C.BlockID blocks tp ->
W4.Pred sym ->
C.PausedFrame p sym ext rtp (C.CrucibleLang blocks r) ->
C.PausedFrame p sym ext rtp (C.CrucibleLang blocks r) ->
Maybe (C.Some (C.BlockID blocks)) ->
Maybe (C.Some (C.BlockID blocks)) ->
C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) ->
IORef (ExecutionFeatureContext sym wptr ext) ->
IO (C.ExecutionFeatureResult p sym ext rtp)
handleSymbolicBranch bak call_frame_handle loop_block_id branch_condition true_frame false_frame true_frame_parent_loop_id false_frame_parent_loop_id sim_state fixpoint_state_ref = do
let sym = C.backendGetSym bak
(loop_condition, inside_loop_frame, outside_loop_frame) <-
if true_frame_parent_loop_id == Just (C.Some loop_block_id)
then
return (branch_condition, true_frame, false_frame)
else if false_frame_parent_loop_id == Just (C.Some loop_block_id)
then do
not_branch_condition <- W4.notPred sym branch_condition
return (not_branch_condition, false_frame, true_frame)
else
fail $ "unsupported loop: loop header block id " ++ show loop_block_id ++ " true frame parent loop id " ++ show true_frame_parent_loop_id ++ " false frame parent loop id " ++ show false_frame_parent_loop_id
Just fixpoint_state <- callFrameContextLookup' call_frame_handle loop_block_id <$> readIORef fixpoint_state_ref
(condition, frame) <- case fixpoint_state of
BeforeFixpoint -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint:" ["BeforeFixpoint"]
ComputeFixpoint{} -> do
-- continue in the loop
?logMessage "SimpleLoopFixpoint: SymbolicBranchState: ComputeFixpoint"
return (loop_condition, inside_loop_frame)
CheckFixpoint fixpoint_record some_inv_pred some_uninterpreted_constants _ -> do
-- continue in the loop
?logMessage "SimpleLoopFixpoint: SymbolicBranchState: CheckFixpoint"
modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle loop_block_id $
CheckFixpoint fixpoint_record some_inv_pred some_uninterpreted_constants loop_condition
return (loop_condition, inside_loop_frame)
AfterFixpoint{} -> do
-- break out of the loop
?logMessage "SimpleLoopFixpoint: SymbolicBranchState: AfterFixpoint"
modifyIORef' fixpoint_state_ref $ callFrameContextPop call_frame_handle
not_loop_condition <- W4.notPred sym loop_condition
return (not_loop_condition, outside_loop_frame)
loc <- W4.getCurrentProgramLoc sym
C.addAssumption bak $ C.BranchCondition loc (C.pausedLoc frame) condition
C.ExecutionFeatureNewState <$>
runReaderT
(C.resumeFrame (C.forgetPostdomFrame frame) $ sim_state ^. (C.stateTree . C.actContext))
sim_state
data SomeCallFrameHandle ret blocks = forall init . SomeCallFrameHandle (CallFrameHandle init ret blocks)
callFrameHandle :: C.CallFrame sym ext blocks ret ctx -> SomeCallFrameHandle ret blocks
callFrameHandle C.CallFrame { _frameCFG = g } =
SomeCallFrameHandle $ CallFrameHandle (C.cfgHandle g) $ fmapFC C.blockInputs $ C.cfgBlockMap g
data MaybePausedFrameTgtId f where
JustPausedFrameTgtId :: C.Some (C.BlockID b) -> MaybePausedFrameTgtId (C.CrucibleLang b r)
NothingPausedFrameTgtId :: MaybePausedFrameTgtId f
pausedFrameTgtId :: C.PausedFrame p sym ext rtp f -> MaybePausedFrameTgtId f
pausedFrameTgtId C.PausedFrame{ resume = resume } = case resume of
C.ContinueResumption (C.ResolvedJump tgt_id _) -> JustPausedFrameTgtId $ C.Some tgt_id
C.CheckMergeResumption (C.ResolvedJump tgt_id _) -> JustPausedFrameTgtId $ C.Some tgt_id
_ -> NothingPausedFrameTgtId
applySubstitutionFC :: (OrdF k, FunctorFC f) => MapF k k -> f k l -> f k l
applySubstitutionFC substitution = fmapFC $ findWithDefaultKey substitution
findWithDefaultKey :: forall a (k :: a -> Type) tp . OrdF k => MapF k k -> k tp -> k tp
findWithDefaultKey substitution key = MapF.findWithDefault key key substitution
asBoundVarSubstitution :: W4.IsSymExprBuilder sym => sym -> MapF (W4.SymExpr sym) a -> MapF (W4.BoundVar sym) a
asBoundVarSubstitution sym =
MapF.fromList . mapMaybe (\(MapF.Pair k_expr v) -> fmap (\k_var -> MapF.Pair k_var v) $ asBoundVar sym k_expr) . MapF.toList
asBoundVar :: W4.IsSymExprBuilder sym => sym -> W4.SymExpr sym tp -> Maybe (W4.BoundVar sym tp)
asBoundVar sym expr = case Set.toList (W4.exprUninterpConstants sym expr) of
[Some var]
| Just Refl <- testEquality expr (W4.varExpr sym var) ->
Just var
_ -> Nothing
headAssumption :: sym -> C.Assumptions sym -> IO (C.CrucibleAssumption (W4.SymExpr sym))
headAssumption sym = \case
C.SingleAssumption a -> return a
C.ManyAssumptions (x Seq.:<| _) -> headAssumption sym x
_ -> fail "SimpleLoopFixpoint.headAssumption: empty assumptions"