------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.SimpleLoopFixpoint
-- Description      : Execution feature to compute loop fixpoint
-- Copyright        : (c) Galois, Inc 2021
-- License          : BSD3
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}


module Lang.Crucible.LLVM.SimpleLoopFixpoint
  ( FixpointEntry(..)
  , simpleLoopFixpoint
  ) where

import           Control.Lens
import           Control.Monad (when)
import           Control.Monad.IO.Class (MonadIO(..))
import           Control.Monad.Reader (ReaderT(..))
import           Control.Monad.State (MonadState(..), StateT(..))
import           Control.Monad.Trans.Maybe
import           Data.Either
import           Data.Foldable
import qualified Data.IntMap as IntMap
import           Data.IORef
import qualified Data.List as List
import           Data.Maybe
import qualified Data.Map as Map
import           Data.Map (Map)
import qualified Data.Set as Set
import qualified System.IO
import           Numeric.Natural

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.TraversableF
import           Data.Parameterized.TraversableFC

import qualified What4.Config as W4
import qualified What4.Interface 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.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


-- | 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 varible, 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
  { forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
headerValue :: W4.SymExpr sym tp
  , forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
bodyValue :: W4.SymExpr sym tp
  }

instance OrdF (W4.SymExpr sym) => OrdF (FixpointEntry sym) where
  compareF :: forall (x :: BaseType) (y :: BaseType).
FixpointEntry sym x -> FixpointEntry sym y -> OrderingF x y
compareF FixpointEntry sym x
x FixpointEntry sym y
y = case SymExpr sym x -> SymExpr sym y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: BaseType) (y :: BaseType).
SymExpr sym x -> SymExpr sym y -> OrderingF x y
compareF (FixpointEntry sym x -> SymExpr sym x
forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
headerValue FixpointEntry sym x
x) (FixpointEntry sym y -> SymExpr sym y
forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
headerValue FixpointEntry sym y
y) of
    OrderingF x y
LTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
    OrderingF x y
EQF -> SymExpr sym x -> SymExpr sym y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: BaseType) (y :: BaseType).
SymExpr sym x -> SymExpr sym y -> OrderingF x y
compareF (FixpointEntry sym x -> SymExpr sym x
forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
bodyValue FixpointEntry sym x
x) (FixpointEntry sym y -> SymExpr sym y
forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
bodyValue FixpointEntry sym y
y)
    OrderingF x y
GTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

instance OrdF (FixpointEntry sym) => W4.TestEquality (FixpointEntry sym) where
  testEquality :: forall (a :: BaseType) (b :: BaseType).
FixpointEntry sym a -> FixpointEntry sym b -> Maybe (a :~: b)
testEquality FixpointEntry sym a
x FixpointEntry sym b
y = case FixpointEntry sym a -> FixpointEntry sym b -> OrderingF a b
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: BaseType) (y :: BaseType).
FixpointEntry sym x -> FixpointEntry sym y -> OrderingF x y
compareF FixpointEntry sym a
x FixpointEntry sym b
y of
    OrderingF a b
EQF -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    OrderingF a b
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing

data MemFixpointEntry sym = forall w . (1 <= w) => MemFixpointEntry
  { forall sym. MemFixpointEntry sym -> sym
memFixpointEntrySym :: sym
  , ()
memFixpointEntryJoinVariable :: W4.SymBV sym w
  }

-- | This datatype captures the state machine that progresses as we
--   attempt to compute a loop invariant for a simple structured loop.
data FixpointState sym blocks
    -- | 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 blocks)

    -- | 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 blocks)
      (LoopIndexBound sym) -- ^ data about the fixed sort of loop index values we are trying to find

    -- | 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 blocks)
      (LoopIndexBound sym) -- ^ data about the fixed sort of loop index values we are trying to find

-- | Data about the loop that we incrementally compute as we approach fixpoint.
data FixpointRecord sym blocks = forall args.
  FixpointRecord
  {
    -- | Block identifier of the head of the loop
    forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> Some (BlockID blocks)
fixpointBlockId :: C.Some (C.BlockID blocks)

    -- | identifier for the currently-active assumption frame related to this fixpoint computation
  , forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> FrameIdentifier
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.
  , forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> MapF (SymExpr sym) (FixpointEntry sym)
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 )
  , forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution :: Map (Natural, Natural, Natural) (MemFixpointEntry sym, C.StorageType)

    -- | Condition which, when true, stays in the loop. This is captured when the (unique, by assumption)
    --   symbolic branch that exits the loop is encountered. This condition is updated on each iteration
    --   as we widen the invariant.
  , forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> Maybe (Pred sym)
fixpointLoopCondition :: Maybe (W4.Pred sym)
  }


fixpointRecord :: FixpointState sym blocks -> Maybe (FixpointRecord sym blocks)
fixpointRecord :: forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointState sym blocks -> Maybe (FixpointRecord sym blocks)
fixpointRecord FixpointState sym blocks
BeforeFixpoint = Maybe (FixpointRecord sym blocks)
forall a. Maybe a
Nothing
fixpointRecord (ComputeFixpoint FixpointRecord sym blocks
r) = FixpointRecord sym blocks -> Maybe (FixpointRecord sym blocks)
forall a. a -> Maybe a
Just FixpointRecord sym blocks
r
fixpointRecord (CheckFixpoint FixpointRecord sym blocks
r LoopIndexBound sym
_) = FixpointRecord sym blocks -> Maybe (FixpointRecord sym blocks)
forall a. a -> Maybe a
Just FixpointRecord sym blocks
r
fixpointRecord (AfterFixpoint FixpointRecord sym blocks
r LoopIndexBound sym
_) = FixpointRecord sym blocks -> Maybe (FixpointRecord sym blocks)
forall a. a -> Maybe a
Just FixpointRecord sym blocks
r


type FixpointMonad sym = StateT (MapF (W4.SymExpr sym) (FixpointEntry sym)) IO


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 :: forall sym (ctx :: Ctx CrucibleType).
(?logMessage::String -> IO (), IsSymInterface sym) =>
sym
-> Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx
-> FixpointMonad sym (Assignment (RegEntry sym) ctx)
joinRegEntries sym
sym = (forall (x :: CrucibleType).
 RegEntry sym x
 -> RegEntry sym x
 -> StateT
      (MapF (SymExpr sym) (FixpointEntry sym)) IO (RegEntry sym x))
-> Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx
-> StateT
     (MapF (SymExpr sym) (FixpointEntry sym))
     IO
     (Assignment (RegEntry sym) ctx)
forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
       (h :: k -> Type) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Assignment f a -> Assignment g a -> m (Assignment h a)
Ctx.zipWithM (sym
-> RegEntry sym x
-> RegEntry sym x
-> StateT
     (MapF (SymExpr sym) (FixpointEntry sym)) IO (RegEntry sym x)
forall sym (tp :: CrucibleType).
(?logMessage::String -> IO (), IsSymInterface sym) =>
sym
-> RegEntry sym tp
-> RegEntry sym tp
-> FixpointMonad sym (RegEntry sym tp)
joinRegEntry sym
sym)

joinRegEntry ::
  (?logMessage :: String -> IO (), C.IsSymInterface sym) =>
  sym ->
  C.RegEntry sym tp ->
  C.RegEntry sym tp ->
  FixpointMonad sym (C.RegEntry sym tp)
joinRegEntry :: forall sym (tp :: CrucibleType).
(?logMessage::String -> IO (), IsSymInterface sym) =>
sym
-> RegEntry sym tp
-> RegEntry sym tp
-> FixpointMonad sym (RegEntry sym tp)
joinRegEntry sym
sym RegEntry sym tp
left RegEntry sym tp
right = case RegEntry sym tp -> TypeRepr tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
C.regType RegEntry sym tp
left of
  C.LLVMPointerRepr NatRepr w
w

      -- special handling for "don't care" registers coming from Macaw
    | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf String
"cmacaw_reg" (Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ SymNat sym -> Doc Any
forall sym ann. IsExpr (SymExpr sym) => SymNat sym -> Doc ann
W4.printSymNat (SymNat sym -> Doc Any) -> SymNat sym -> Doc Any
forall a b. (a -> b) -> a -> b
$ LLVMPtr sym w -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
C.llvmPointerBlock (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left))
    , String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf String
"cmacaw_reg" (Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ SymExpr sym (BaseBVType w) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr (SymExpr sym (BaseBVType w) -> Doc Any)
-> SymExpr sym (BaseBVType w) -> Doc Any
forall a b. (a -> b) -> a -> b
$ LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left)) -> do
      IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a.
IO a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ())
-> IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage String
"SimpleLoopFixpoint.joinRegEntry: cmacaw_reg"
      RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RegEntry sym tp
left

    | LLVMPtr sym w -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
C.llvmPointerBlock (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left) SymNat sym -> SymNat sym -> Bool
forall a. Eq a => a -> a -> Bool
== LLVMPtr sym w -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
C.llvmPointerBlock (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
right) -> do
      IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a.
IO a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ())
-> IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage String
"SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr"
      MapF (SymExpr sym) (FixpointEntry sym)
subst <- StateT
  (MapF (SymExpr sym) (FixpointEntry sym))
  IO
  (MapF (SymExpr sym) (FixpointEntry sym))
forall s (m :: Type -> Type). MonadState s m => m s
get
      if Maybe (BaseBVType w :~: BaseBVType w) -> Bool
forall a. Maybe a -> Bool
isJust (SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> Maybe (BaseBVType w :~: BaseBVType w)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
SymExpr sym a -> SymExpr sym b -> Maybe (a :~: b)
W4.testEquality (LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left)) (LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
right)))
      then do
        IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a.
IO a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ())
-> IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage String
"SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: left == right"
        RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RegEntry sym tp
left
      else case SymExpr sym (BaseBVType w)
-> MapF (SymExpr sym) (FixpointEntry sym)
-> Maybe (FixpointEntry sym (BaseBVType w))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup (LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left)) MapF (SymExpr sym) (FixpointEntry sym)
subst of
        Just FixpointEntry sym (BaseBVType w)
join_entry -> do
          IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a.
IO a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ())
-> IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
            String
"SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: Just: "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseBVType w) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr (SymExpr sym (BaseBVType w) -> Doc Any)
-> SymExpr sym (BaseBVType w) -> Doc Any
forall a b. (a -> b) -> a -> b
$ FixpointEntry sym (BaseBVType w) -> SymExpr sym (BaseBVType w)
forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
bodyValue FixpointEntry sym (BaseBVType w)
join_entry)
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -> "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseBVType w) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr (SymExpr sym (BaseBVType w) -> Doc Any)
-> SymExpr sym (BaseBVType w) -> Doc Any
forall a b. (a -> b) -> a -> b
$ LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
right))
          MapF (SymExpr sym) (FixpointEntry sym)
-> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put (MapF (SymExpr sym) (FixpointEntry sym)
 -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ())
-> MapF (SymExpr sym) (FixpointEntry sym)
-> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a b. (a -> b) -> a -> b
$ SymExpr sym (BaseBVType w)
-> FixpointEntry sym (BaseBVType w)
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert
            (LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left))
            (FixpointEntry sym (BaseBVType w)
join_entry { bodyValue = C.llvmPointerOffset (C.regValue right) })
            MapF (SymExpr sym) (FixpointEntry sym)
subst
          RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RegEntry sym tp
left
        Maybe (FixpointEntry sym (BaseBVType w))
Nothing -> do
          IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a.
IO a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ())
-> IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage String
"SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: Nothing"
          SymExpr sym (BaseBVType w)
join_varaible <- IO (SymExpr sym (BaseBVType w))
-> StateT
     (MapF (SymExpr sym) (FixpointEntry sym))
     IO
     (SymExpr sym (BaseBVType w))
forall a.
IO a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType w))
 -> StateT
      (MapF (SymExpr sym) (FixpointEntry sym))
      IO
      (SymExpr sym (BaseBVType w)))
-> IO (SymExpr sym (BaseBVType w))
-> StateT
     (MapF (SymExpr sym) (FixpointEntry sym))
     IO
     (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ sym
-> SolverSymbol
-> BaseTypeRepr (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
W4.freshConstant sym
sym (String -> SolverSymbol
userSymbol' String
"reg_join_var") (NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr NatRepr w
w)
          let join_entry :: FixpointEntry sym (BaseBVType w)
join_entry = FixpointEntry
                { headerValue :: SymExpr sym (BaseBVType w)
headerValue = LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left)
                , bodyValue :: SymExpr sym (BaseBVType w)
bodyValue = LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
right)
                }
          MapF (SymExpr sym) (FixpointEntry sym)
-> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put (MapF (SymExpr sym) (FixpointEntry sym)
 -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ())
-> MapF (SymExpr sym) (FixpointEntry sym)
-> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a b. (a -> b) -> a -> b
$ SymExpr sym (BaseBVType w)
-> FixpointEntry sym (BaseBVType w)
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert SymExpr sym (BaseBVType w)
join_varaible FixpointEntry sym (BaseBVType w)
join_entry MapF (SymExpr sym) (FixpointEntry sym)
subst
          RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp))
-> RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a b. (a -> b) -> a -> b
$ TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
C.RegEntry (NatRepr w -> TypeRepr tp
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
C.LLVMPointerRepr NatRepr w
w) (RegValue sym tp -> RegEntry sym tp)
-> RegValue sym tp -> RegEntry sym tp
forall a b. (a -> b) -> a -> b
$ SymNat sym -> SymExpr sym (BaseBVType w) -> LLVMPointer sym w
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
C.LLVMPointer (LLVMPtr sym w -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
C.llvmPointerBlock (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left)) SymExpr sym (BaseBVType w)
join_varaible
    | Bool
otherwise ->
      String -> FixpointMonad sym (RegEntry sym tp)
forall a.
String -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> FixpointMonad sym (RegEntry sym tp))
-> String -> FixpointMonad sym (RegEntry sym tp)
forall a b. (a -> b) -> a -> b
$
        String
"SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: unsupported pointer base join: "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (LLVMPtr sym w -> Doc Any
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
C.ppPtr (LLVMPtr sym w -> Doc Any) -> LLVMPtr sym w -> Doc Any
forall a b. (a -> b) -> a -> b
$ RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left)
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" \\/ "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (LLVMPtr sym w -> Doc Any
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
C.ppPtr (LLVMPtr sym w -> Doc Any) -> LLVMPtr sym w -> Doc Any
forall a b. (a -> b) -> a -> b
$ RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
right)

  TypeRepr tp
C.BoolRepr
    | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf String
"cmacaw" (Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ SymExpr sym BaseBoolType -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr (SymExpr sym BaseBoolType -> Doc Any)
-> SymExpr sym BaseBoolType -> Doc Any
forall a b. (a -> b) -> a -> b
$ RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left) -> do
      IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a.
IO a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ())
-> IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage String
"SimpleLoopFixpoint.joinRegEntry: cmacaw_reg"
      RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RegEntry sym tp
left
    | Bool
otherwise -> do
      IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a.
IO a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ())
-> IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
        String
"SimpleLoopFixpoint.joinRegEntry: BoolRepr:"
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym BaseBoolType -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr (SymExpr sym BaseBoolType -> Doc Any)
-> SymExpr sym BaseBoolType -> Doc Any
forall a b. (a -> b) -> a -> b
$ RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left)
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" \\/ "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym BaseBoolType -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr (SymExpr sym BaseBoolType -> Doc Any)
-> SymExpr sym BaseBoolType -> Doc Any
forall a b. (a -> b) -> a -> b
$ RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
right)
      SymExpr sym BaseBoolType
join_varaible <- IO (SymExpr sym BaseBoolType)
-> StateT
     (MapF (SymExpr sym) (FixpointEntry sym))
     IO
     (SymExpr sym BaseBoolType)
forall a.
IO a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> StateT
      (MapF (SymExpr sym) (FixpointEntry sym))
      IO
      (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> StateT
     (MapF (SymExpr sym) (FixpointEntry sym))
     IO
     (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SolverSymbol
-> BaseTypeRepr BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
W4.freshConstant sym
sym (String -> SolverSymbol
userSymbol' String
"macaw_reg") BaseTypeRepr BaseBoolType
W4.BaseBoolRepr
      RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp))
-> RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a b. (a -> b) -> a -> b
$ TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
C.RegEntry TypeRepr tp
TypeRepr ('BaseToType BaseBoolType)
C.BoolRepr RegValue sym tp
SymExpr sym BaseBoolType
join_varaible

  C.StructRepr CtxRepr ctx
field_types -> do
    IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a.
IO a -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ())
-> IO () -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage String
"SimpleLoopFixpoint.joinRegEntry: StructRepr"
    TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
C.RegEntry (RegEntry sym tp -> TypeRepr tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
C.regType RegEntry sym tp
left) (Assignment (RegValue' sym) ctx -> RegEntry sym tp)
-> (Assignment (RegEntry sym) ctx
    -> Assignment (RegValue' sym) ctx)
-> Assignment (RegEntry sym) ctx
-> RegEntry sym tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). RegEntry sym x -> RegValue' sym x)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> Assignment (RegValue' sym) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (RegValue sym x -> RegValue' sym x
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
C.RV (RegValue sym x -> RegValue' sym x)
-> (RegEntry sym x -> RegValue sym x)
-> RegEntry sym x
-> RegValue' sym x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RegEntry sym x -> RegValue sym x
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue) (Assignment (RegEntry sym) ctx -> RegEntry sym tp)
-> StateT
     (MapF (SymExpr sym) (FixpointEntry sym))
     IO
     (Assignment (RegEntry sym) ctx)
-> FixpointMonad sym (RegEntry sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx
-> StateT
     (MapF (SymExpr sym) (FixpointEntry sym))
     IO
     (Assignment (RegEntry sym) ctx)
forall sym (ctx :: Ctx CrucibleType).
(?logMessage::String -> IO (), IsSymInterface sym) =>
sym
-> Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx
-> FixpointMonad sym (Assignment (RegEntry sym) ctx)
joinRegEntries sym
sym
      (Size ctx
-> (forall {tp :: CrucibleType}. Index ctx tp -> RegEntry sym tp)
-> Assignment (RegEntry sym) ctx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
Ctx.generate (CtxRepr ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size CtxRepr ctx
field_types) ((forall {tp :: CrucibleType}. Index ctx tp -> RegEntry sym tp)
 -> Assignment (RegEntry sym) ctx)
-> (forall {tp :: CrucibleType}. Index ctx tp -> RegEntry sym tp)
-> Assignment (RegEntry sym) ctx
forall a b. (a -> b) -> a -> b
$ \Index ctx tp
i ->
        TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
C.RegEntry (CtxRepr ctx
field_types CtxRepr ctx -> Index ctx tp -> TypeRepr tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i) (RegValue sym tp -> RegEntry sym tp)
-> RegValue sym tp -> RegEntry sym tp
forall a b. (a -> b) -> a -> b
$ RegValue' sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
C.unRV (RegValue' sym tp -> RegValue sym tp)
-> RegValue' sym tp -> RegValue sym tp
forall a b. (a -> b) -> a -> b
$ (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
left) Assignment (RegValue' sym) ctx -> Index ctx tp -> RegValue' sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i)
      (Size ctx
-> (forall {tp :: CrucibleType}. Index ctx tp -> RegEntry sym tp)
-> Assignment (RegEntry sym) ctx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
Ctx.generate (CtxRepr ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size CtxRepr ctx
field_types) ((forall {tp :: CrucibleType}. Index ctx tp -> RegEntry sym tp)
 -> Assignment (RegEntry sym) ctx)
-> (forall {tp :: CrucibleType}. Index ctx tp -> RegEntry sym tp)
-> Assignment (RegEntry sym) ctx
forall a b. (a -> b) -> a -> b
$ \Index ctx tp
i ->
        TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
C.RegEntry (CtxRepr ctx
field_types CtxRepr ctx -> Index ctx tp -> TypeRepr tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i) (RegValue sym tp -> RegEntry sym tp)
-> RegValue sym tp -> RegEntry sym tp
forall a b. (a -> b) -> a -> b
$ RegValue' sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
C.unRV (RegValue' sym tp -> RegValue sym tp)
-> RegValue' sym tp -> RegValue sym tp
forall a b. (a -> b) -> a -> b
$ (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
right) Assignment (RegValue' sym) ctx -> Index ctx tp -> RegValue' sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i)
  TypeRepr tp
_ -> String -> FixpointMonad sym (RegEntry sym tp)
forall a.
String -> StateT (MapF (SymExpr sym) (FixpointEntry sym)) IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> FixpointMonad sym (RegEntry sym tp))
-> String -> FixpointMonad sym (RegEntry sym tp)
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint.joinRegEntry: unsupported type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRepr tp -> String
forall a. Show a => a -> String
show (RegEntry sym tp -> TypeRepr tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
C.regType RegEntry sym tp
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 :: forall sym (ctx :: Ctx CrucibleType).
IsSymInterface sym =>
sym
-> MapF (SymExpr sym) (SymExpr sym)
-> Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx
applySubstitutionRegEntries sym
sym MapF (SymExpr sym) (SymExpr sym)
substitution = (forall (x :: CrucibleType). RegEntry sym x -> RegEntry sym x)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> Assignment (RegEntry sym) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (sym
-> MapF (SymExpr sym) (SymExpr sym)
-> RegEntry sym x
-> RegEntry sym x
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> MapF (SymExpr sym) (SymExpr sym)
-> RegEntry sym tp
-> RegEntry sym tp
applySubstitutionRegEntry sym
sym MapF (SymExpr sym) (SymExpr sym)
substitution)

applySubstitutionRegEntry ::
  C.IsSymInterface sym =>
  sym ->
  MapF (W4.SymExpr sym) (W4.SymExpr sym) ->
  C.RegEntry sym tp ->
  C.RegEntry sym tp
applySubstitutionRegEntry :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> MapF (SymExpr sym) (SymExpr sym)
-> RegEntry sym tp
-> RegEntry sym tp
applySubstitutionRegEntry sym
sym MapF (SymExpr sym) (SymExpr sym)
substitution RegEntry sym tp
entry = case RegEntry sym tp -> TypeRepr tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
C.regType RegEntry sym tp
entry of
  C.LLVMPointerRepr{} ->
    RegEntry sym tp
entry
      { C.regValue = C.LLVMPointer
          (C.llvmPointerBlock (C.regValue entry))
          (MapF.findWithDefault
            (C.llvmPointerOffset (C.regValue entry))
            (C.llvmPointerOffset (C.regValue entry))
            substitution)
      }
  TypeRepr tp
C.BoolRepr ->
    RegEntry sym tp
entry
  C.StructRepr CtxRepr ctx
field_types ->
    RegEntry sym tp
entry
      { C.regValue = fmapFC (C.RV . C.regValue) $
          applySubstitutionRegEntries sym substitution $
          Ctx.generate (Ctx.size field_types) $
          \Index ctx tp
i -> TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
C.RegEntry (CtxRepr ctx
field_types CtxRepr ctx -> Index ctx tp -> TypeRepr tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i) (RegValue sym tp -> RegEntry sym tp)
-> RegValue sym tp -> RegEntry sym tp
forall a b. (a -> b) -> a -> b
$ RegValue' sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
C.unRV (RegValue' sym tp -> RegValue sym tp)
-> RegValue' sym tp -> RegValue sym tp
forall a b. (a -> b) -> a -> b
$ (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
C.regValue RegEntry sym tp
entry) Assignment (RegValue' sym) ctx -> Index ctx tp -> RegValue' sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i
      }
  TypeRepr tp
_ -> String -> [String] -> RegEntry sym tp
forall a. HasCallStack => String -> [String] -> a
C.panic String
"SimpleLoopFixpoint.applySubstitutionRegEntry" [String
"unsupported type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRepr tp -> String
forall a. Show a => a -> String
show (RegEntry sym tp -> TypeRepr tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
C.regType RegEntry sym tp
entry)]


findLoopIndex ::
  (?logMessage :: String -> IO (), C.IsSymInterface sym, C.HasPtrWidth wptr) =>
  sym ->
  MapF (W4.SymExpr sym) (FixpointEntry sym) ->
  IO (W4.SymBV sym wptr, Natural, Natural)
findLoopIndex :: forall sym (wptr :: Natural).
(?logMessage::String -> IO (), IsSymInterface sym,
 HasPtrWidth wptr) =>
sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> IO (SymBV sym wptr, Natural, Natural)
findLoopIndex sym
sym MapF (SymExpr sym) (FixpointEntry sym)
substitution = do
  [(SymBV sym wptr, Natural, Natural)]
candidates <- [Maybe (SymBV sym wptr, Natural, Natural)]
-> [(SymBV sym wptr, Natural, Natural)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (SymBV sym wptr, Natural, Natural)]
 -> [(SymBV sym wptr, Natural, Natural)])
-> IO [Maybe (SymBV sym wptr, Natural, Natural)]
-> IO [(SymBV sym wptr, Natural, Natural)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pair (SymExpr sym) (FixpointEntry sym)
 -> IO (Maybe (SymBV sym wptr, Natural, Natural)))
-> [Pair (SymExpr sym) (FixpointEntry sym)]
-> IO [Maybe (SymBV sym wptr, Natural, Natural)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM
    (\(MapF.Pair SymExpr sym tp
variable FixpointEntry{SymExpr sym tp
headerValue :: forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
bodyValue :: forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
headerValue :: SymExpr sym tp
bodyValue :: SymExpr sym tp
..}) -> case BaseTypeRepr ('BaseBVType wptr)
-> BaseTypeRepr tp -> Maybe ('BaseBVType wptr :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
W4.testEquality (NatRepr wptr -> BaseTypeRepr ('BaseBVType wptr)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth) (SymExpr sym tp -> BaseTypeRepr tp
forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym tp
variable) of
      Just 'BaseBVType wptr :~: tp
Refl -> do
        SymBV sym wptr
diff <- IO (SymBV sym wptr) -> IO (SymBV sym wptr)
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym wptr) -> IO (SymBV sym wptr))
-> IO (SymBV sym wptr) -> IO (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym wptr -> SymBV sym wptr -> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSub sym
sym SymExpr sym tp
SymBV sym wptr
bodyValue SymExpr sym tp
SymBV sym wptr
variable
        case (BV wptr -> Natural
forall (w :: Natural). BV w -> Natural
BV.asNatural (BV wptr -> Natural) -> Maybe (BV wptr) -> Maybe Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym wptr -> Maybe (BV wptr)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W4.asBV SymExpr sym tp
SymBV sym wptr
headerValue, BV wptr -> Natural
forall (w :: Natural). BV w -> Natural
BV.asNatural (BV wptr -> Natural) -> Maybe (BV wptr) -> Maybe Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym wptr -> Maybe (BV wptr)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W4.asBV SymBV sym wptr
diff) of
          (Just Natural
start, Just Natural
step) -> do
            IO () -> IO ()
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
              String
"SimpleLoopFixpoint.findLoopIndex: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (SymBV sym wptr -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr SymExpr sym tp
SymBV sym wptr
variable) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Natural, Natural) -> String
forall a. Show a => a -> String
show (Natural
start, Natural
step)
            Maybe (SymBV sym wptr, Natural, Natural)
-> IO (Maybe (SymBV sym wptr, Natural, Natural))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (SymBV sym wptr, Natural, Natural)
 -> IO (Maybe (SymBV sym wptr, Natural, Natural)))
-> Maybe (SymBV sym wptr, Natural, Natural)
-> IO (Maybe (SymBV sym wptr, Natural, Natural))
forall a b. (a -> b) -> a -> b
$ (SymBV sym wptr, Natural, Natural)
-> Maybe (SymBV sym wptr, Natural, Natural)
forall a. a -> Maybe a
Just (SymExpr sym tp
variable, Natural
start, Natural
step)
          (Maybe Natural, Maybe Natural)
_ -> Maybe (SymBV sym wptr, Natural, Natural)
-> IO (Maybe (SymBV sym wptr, Natural, Natural))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (SymBV sym wptr, Natural, Natural)
forall a. Maybe a
Nothing
      Maybe ('BaseBVType wptr :~: tp)
Nothing -> Maybe (SymBV sym wptr, Natural, Natural)
-> IO (Maybe (SymBV sym wptr, Natural, Natural))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (SymBV sym wptr, Natural, Natural)
forall a. Maybe a
Nothing)
    (MapF (SymExpr sym) (FixpointEntry sym)
-> [Pair (SymExpr sym) (FixpointEntry sym)]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Pair k2 a]
MapF.toList MapF (SymExpr sym) (FixpointEntry sym)
substitution)
  case [(SymBV sym wptr, Natural, Natural)]
candidates of
    [(SymBV sym wptr, Natural, Natural)
candidate] -> (SymBV sym wptr, Natural, Natural)
-> IO (SymBV sym wptr, Natural, Natural)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymBV sym wptr, Natural, Natural)
candidate
    [(SymBV sym wptr, Natural, Natural)]
_ -> String -> IO (SymBV sym wptr, Natural, Natural)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"SimpleLoopFixpoint.findLoopIndex: loop index identification failure."

findLoopBound ::
  (C.IsSymInterface sym, C.HasPtrWidth wptr) =>
  sym ->
  W4.Pred sym ->
  Natural ->
  Natural ->
  IO (W4.SymBV sym wptr)
findLoopBound :: forall sym (wptr :: Natural).
(IsSymInterface sym, HasPtrWidth wptr) =>
sym -> Pred sym -> Natural -> Natural -> IO (SymBV sym wptr)
findLoopBound sym
sym Pred sym
condition Natural
_start Natural
step =
  case Set (Some (BoundVar sym)) -> [Some (BoundVar sym)]
forall a. Set a -> [a]
Set.toList (Set (Some (BoundVar sym)) -> [Some (BoundVar sym)])
-> Set (Some (BoundVar sym)) -> [Some (BoundVar sym)]
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym -> Set (Some (BoundVar sym))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
forall (tp :: BaseType).
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
W4.exprUninterpConstants sym
sym Pred sym
condition of

    -- this is a grungy hack, we are expecting exactly three variables and take the first
    [C.Some BoundVar sym x
loop_stop, Some (BoundVar sym)
_, Some (BoundVar sym)
_]
      | Just 'BaseBVType wptr :~: x
Refl <- BaseTypeRepr ('BaseBVType wptr)
-> BaseTypeRepr x -> Maybe ('BaseBVType wptr :~: x)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
W4.testEquality (NatRepr wptr -> BaseTypeRepr ('BaseBVType wptr)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth) (SymExpr sym x -> BaseTypeRepr x
forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType (SymExpr sym x -> BaseTypeRepr x)
-> SymExpr sym x -> BaseTypeRepr x
forall a b. (a -> b) -> a -> b
$ sym -> BoundVar sym x -> SymExpr sym x
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
forall (tp :: BaseType). sym -> BoundVar sym tp -> SymExpr sym tp
W4.varExpr sym
sym BoundVar sym x
loop_stop) ->
        sym -> SymBV sym wptr -> SymBV sym wptr -> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvMul sym
sym (sym -> BoundVar sym ('BaseBVType wptr) -> SymBV sym wptr
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
forall (tp :: BaseType). sym -> BoundVar sym tp -> SymExpr sym tp
W4.varExpr sym
sym BoundVar sym x
BoundVar sym ('BaseBVType wptr)
loop_stop) (SymBV sym wptr -> IO (SymBV sym wptr))
-> IO (SymBV sym wptr) -> IO (SymBV sym wptr)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr wptr -> BV wptr -> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (Integer -> BV wptr) -> Integer -> BV wptr
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
step)
    [Some (BoundVar sym)]
_ -> String -> IO (SymBV sym wptr)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"SimpleLoopFixpoint.findLoopBound: loop bound identification failure."


-- index variable information for fixed stride, bounded loops
data LoopIndexBound sym = forall w . 1 <= w => LoopIndexBound
  { ()
index :: W4.SymBV sym w
  , forall sym. LoopIndexBound sym -> Natural
start :: Natural
  , ()
stop :: W4.SymBV sym w
  , forall sym. LoopIndexBound sym -> Natural
step :: Natural
  }

findLoopIndexBound ::
  (?logMessage :: String -> IO (), C.IsSymInterface sym, C.HasPtrWidth wptr) =>
  sym ->
  MapF (W4.SymExpr sym) (FixpointEntry sym) ->
  Maybe (W4.Pred sym) ->
  IO (LoopIndexBound sym)
findLoopIndexBound :: forall sym (wptr :: Natural).
(?logMessage::String -> IO (), IsSymInterface sym,
 HasPtrWidth wptr) =>
sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> Maybe (Pred sym)
-> IO (LoopIndexBound sym)
findLoopIndexBound sym
_sym MapF (SymExpr sym) (FixpointEntry sym)
_substitition Maybe (Pred sym)
Nothing =
  String -> IO (LoopIndexBound sym)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"findLoopIndexBound: no loop condition recorded!"

findLoopIndexBound sym
sym MapF (SymExpr sym) (FixpointEntry sym)
substitution (Just Pred sym
condition) = do
  (SymExpr sym (BaseBVType wptr)
loop_index, Natural
start, Natural
step) <- sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> IO (SymExpr sym (BaseBVType wptr), Natural, Natural)
forall sym (wptr :: Natural).
(?logMessage::String -> IO (), IsSymInterface sym,
 HasPtrWidth wptr) =>
sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> IO (SymBV sym wptr, Natural, Natural)
findLoopIndex sym
sym MapF (SymExpr sym) (FixpointEntry sym)
substitution
  SymExpr sym (BaseBVType wptr)
stop <- sym
-> Pred sym
-> Natural
-> Natural
-> IO (SymExpr sym (BaseBVType wptr))
forall sym (wptr :: Natural).
(IsSymInterface sym, HasPtrWidth wptr) =>
sym -> Pred sym -> Natural -> Natural -> IO (SymBV sym wptr)
findLoopBound sym
sym Pred sym
condition Natural
start Natural
step
  LoopIndexBound sym -> IO (LoopIndexBound sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LoopIndexBound sym -> IO (LoopIndexBound sym))
-> LoopIndexBound sym -> IO (LoopIndexBound sym)
forall a b. (a -> b) -> a -> b
$ LoopIndexBound
    { index :: SymExpr sym (BaseBVType wptr)
index = SymExpr sym (BaseBVType wptr)
loop_index
    , start :: Natural
start = Natural
start
    , stop :: SymExpr sym (BaseBVType wptr)
stop = SymExpr sym (BaseBVType wptr)
stop
    , step :: Natural
step = Natural
step
    }

-- hard-coded here that we are always looking for a loop condition delimited by an unsigned comparison
loopIndexBoundCondition ::
  (C.IsSymInterface sym, 1 <= w) =>
  sym ->
  W4.SymBV sym w ->
  W4.SymBV sym w ->
  IO (W4.Pred sym)
loopIndexBoundCondition :: forall sym (w :: Natural).
(IsSymInterface sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
loopIndexBoundCondition = sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUlt

-- | Describes an assumed invariant on the loop index variable, which is that it is an offset
--   from the initial value that is a multiple of a discoveded stride value.
loopIndexStartStepCondition ::
  C.IsSymInterface sym =>
  sym ->
  LoopIndexBound sym ->
  IO (W4.Pred sym)
loopIndexStartStepCondition :: forall sym.
IsSymInterface sym =>
sym -> LoopIndexBound sym -> IO (Pred sym)
loopIndexStartStepCondition sym
sym LoopIndexBound{ index :: ()
index = SymBV sym w
loop_index, start :: forall sym. LoopIndexBound sym -> Natural
start = Natural
start, step :: forall sym. LoopIndexBound sym -> Natural
step = Natural
step } = do
  SymBV sym w
start_bv <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV sym w
loop_index) (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV sym w
loop_index) (Integer -> BV w) -> Integer -> BV w
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
start)
  SymBV sym w
step_bv <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV sym w
loop_index) (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV sym w
loop_index) (Integer -> BV w) -> Integer -> BV w
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
step)
  sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvEq sym
sym SymBV sym w
start_bv (SymBV sym w -> IO (Pred sym)) -> IO (SymBV sym w) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvUrem sym
sym SymBV sym w
loop_index SymBV sym w
step_bv


loadMemJoinVariables ::
  (C.IsSymBackend sym bak, C.HasPtrWidth wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) =>
  bak ->
  C.MemImpl sym ->
  Map (Natural, Natural, Natural) (MemFixpointEntry sym, C.StorageType) ->
  IO (MapF (W4.SymExpr sym) (W4.SymExpr sym))
loadMemJoinVariables :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO (MapF (SymExpr sym) (SymExpr sym))
loadMemJoinVariables bak
bak MemImpl sym
mem Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
subst =
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
C.backendGetSym bak
bak in
  [Pair (SymExpr sym) (SymExpr sym)]
-> MapF (SymExpr sym) (SymExpr sym)
forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
[Pair k a] -> MapF k a
MapF.fromList ([Pair (SymExpr sym) (SymExpr sym)]
 -> MapF (SymExpr sym) (SymExpr sym))
-> IO [Pair (SymExpr sym) (SymExpr sym)]
-> IO (MapF (SymExpr sym) (SymExpr sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))
 -> IO (Pair (SymExpr sym) (SymExpr sym)))
-> [((Natural, Natural, Natural),
     (MemFixpointEntry sym, StorageType))]
-> IO [Pair (SymExpr sym) (SymExpr sym)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM
    (\((Natural
blk, Natural
off, Natural
_sz), (MemFixpointEntry { memFixpointEntryJoinVariable :: ()
memFixpointEntryJoinVariable = SymBV sym w
join_varaible }, StorageType
storeage_type)) -> do
      LLVMPointer sym wptr
ptr <- SymNat sym -> SymBV sym wptr -> LLVMPointer sym wptr
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
C.LLVMPointer (SymNat sym -> SymBV sym wptr -> LLVMPointer sym wptr)
-> IO (SymNat sym) -> IO (SymBV sym wptr -> LLVMPointer sym wptr)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
W4.natLit sym
sym Natural
blk IO (SymBV sym wptr -> LLVMPointer sym wptr)
-> IO (SymBV sym wptr) -> IO (LLVMPointer sym wptr)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> NatRepr wptr -> BV wptr -> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (Integer -> BV wptr) -> Integer -> BV wptr
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
off)
      RegValue sym (LLVMPointerType w)
val <- bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr (LLVMPointerType w)
-> Alignment
-> IO (RegValue sym (LLVMPointerType w))
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr tp
-> Alignment
-> IO (RegValue sym tp)
C.doLoad bak
bak MemImpl sym
mem LLVMPtr sym wptr
LLVMPointer sym wptr
ptr StorageType
storeage_type (NatRepr w -> TypeRepr (LLVMPointerType w)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
C.LLVMPointerRepr (NatRepr w -> TypeRepr (LLVMPointerType w))
-> NatRepr w -> TypeRepr (LLVMPointerType w)
forall a b. (a -> b) -> a -> b
$ SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV sym w
join_varaible) Alignment
C.noAlignment
      case SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
W4.asNat (RegValue sym (LLVMPointerType w) -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
C.llvmPointerBlock RegValue sym (LLVMPointerType w)
val) of
        Just Natural
0 -> Pair (SymExpr sym) (SymExpr sym)
-> IO (Pair (SymExpr sym) (SymExpr sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pair (SymExpr sym) (SymExpr sym)
 -> IO (Pair (SymExpr sym) (SymExpr sym)))
-> Pair (SymExpr sym) (SymExpr sym)
-> IO (Pair (SymExpr sym) (SymExpr sym))
forall a b. (a -> b) -> a -> b
$ SymBV sym w -> SymBV sym w -> Pair (SymExpr sym) (SymExpr sym)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
MapF.Pair SymBV sym w
join_varaible (SymBV sym w -> Pair (SymExpr sym) (SymExpr sym))
-> SymBV sym w -> Pair (SymExpr sym) (SymExpr sym)
forall a b. (a -> b) -> a -> b
$ RegValue sym (LLVMPointerType w) -> SymBV sym w
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset RegValue sym (LLVMPointerType w)
val
        Maybe Natural
_ -> String -> IO (Pair (SymExpr sym) (SymExpr sym))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (Pair (SymExpr sym) (SymExpr sym)))
-> String -> IO (Pair (SymExpr sym) (SymExpr sym))
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint.loadMemJoinVariables: unexpected val:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (RegValue sym (LLVMPointerType w) -> Doc Any
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
C.ppPtr RegValue sym (LLVMPointerType w)
val))
    (Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> [((Natural, Natural, Natural),
     (MemFixpointEntry sym, StorageType))]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
subst)

storeMemJoinVariables ::
  (C.IsSymBackend sym bak, C.HasPtrWidth wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) =>
  bak ->
  C.MemImpl sym ->
  Map (Natural, Natural, Natural) (MemFixpointEntry sym, C.StorageType) ->
  MapF (W4.SymExpr sym) (W4.SymExpr sym) ->
  IO (C.MemImpl sym)
storeMemJoinVariables :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
storeMemJoinVariables bak
bak MemImpl sym
mem Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
mem_subst MapF (SymExpr sym) (SymExpr sym)
eq_subst =
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
C.backendGetSym bak
bak in
  (MemImpl sym
 -> ((Natural, Natural, Natural),
     (MemFixpointEntry sym, StorageType))
 -> IO (MemImpl sym))
-> MemImpl sym
-> [((Natural, Natural, Natural),
     (MemFixpointEntry sym, StorageType))]
-> IO (MemImpl sym)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
  (\MemImpl sym
mem_acc ((Natural
blk, Natural
off, Natural
_sz), (MemFixpointEntry { memFixpointEntryJoinVariable :: ()
memFixpointEntryJoinVariable = SymBV sym w
join_varaible }, StorageType
storeage_type)) -> do
    LLVMPointer sym wptr
ptr <- SymNat sym -> SymBV sym wptr -> LLVMPointer sym wptr
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
C.LLVMPointer (SymNat sym -> SymBV sym wptr -> LLVMPointer sym wptr)
-> IO (SymNat sym) -> IO (SymBV sym wptr -> LLVMPointer sym wptr)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
W4.natLit sym
sym Natural
blk IO (SymBV sym wptr -> LLVMPointer sym wptr)
-> IO (SymBV sym wptr) -> IO (LLVMPointer sym wptr)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> NatRepr wptr -> BV wptr -> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (Integer -> BV wptr) -> Integer -> BV wptr
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
off)
    bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr (LLVMPointerType w)
-> StorageType
-> Alignment
-> RegValue sym (LLVMPointerType w)
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr tp
-> StorageType
-> Alignment
-> RegValue sym tp
-> IO (MemImpl sym)
C.doStore bak
bak MemImpl sym
mem_acc LLVMPtr sym wptr
LLVMPointer sym wptr
ptr (NatRepr w -> TypeRepr (LLVMPointerType w)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
C.LLVMPointerRepr (NatRepr w -> TypeRepr (LLVMPointerType w))
-> NatRepr w -> TypeRepr (LLVMPointerType w)
forall a b. (a -> b) -> a -> b
$ SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV sym w
join_varaible) StorageType
storeage_type Alignment
C.noAlignment (RegValue sym (LLVMPointerType w) -> IO (MemImpl sym))
-> IO (RegValue sym (LLVMPointerType w)) -> IO (MemImpl sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<<
      sym -> SymBV sym w -> IO (RegValue sym (LLVMPointerType w))
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
C.llvmPointer_bv sym
sym (SymBV sym w
-> SymBV sym w -> MapF (SymExpr sym) (SymExpr sym) -> SymBV sym w
forall {v} (k :: v -> Type) (a :: v -> Type) (tp :: v).
OrdF k =>
a tp -> k tp -> MapF k a -> a tp
MapF.findWithDefault SymBV sym w
join_varaible SymBV sym w
join_varaible MapF (SymExpr sym) (SymExpr sym)
eq_subst))
  MemImpl sym
mem
  (Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> [((Natural, Natural, Natural),
     (MemFixpointEntry sym, StorageType))]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
mem_subst)

dropMemStackFrame :: C.IsSymInterface sym => C.MemImpl sym -> (C.MemImpl sym, C.MemAllocs sym, C.MemWrites sym)
dropMemStackFrame :: forall sym.
IsSymInterface sym =>
MemImpl sym -> (MemImpl sym, MemAllocs sym, MemWrites sym)
dropMemStackFrame MemImpl sym
mem = case (MemImpl sym -> Mem sym
forall sym. MemImpl sym -> Mem sym
C.memImplHeap MemImpl sym
mem) Mem sym
-> Getting (MemState sym) (Mem sym) (MemState sym) -> MemState sym
forall s a. s -> Getting a s a -> a
^. Getting (MemState sym) (Mem sym) (MemState sym)
forall sym (f :: Type -> Type).
Functor f =>
(MemState sym -> f (MemState sym)) -> Mem sym -> f (Mem sym)
C.memState of
  (C.StackFrame Int
_ Int
_ Text
_ (MemAllocs sym
a, MemWrites sym
w) MemState sym
s) -> ((MemImpl sym
mem { C.memImplHeap = (C.memImplHeap mem) & C.memState .~ s }), MemAllocs sym
a, MemWrites sym
w)
  MemState sym
_ -> String -> [String] -> (MemImpl sym, MemAllocs sym, MemWrites sym)
forall a. HasCallStack => String -> [String] -> a
C.panic String
"SimpleLoopFixpoint.dropMemStackFrame" [String
"not a stack frame:", Doc Any -> String
forall a. Show a => a -> String
show (Mem sym -> Doc Any
forall sym ann. IsExpr (SymExpr sym) => Mem sym -> Doc ann
C.ppMem (Mem sym -> Doc Any) -> Mem sym -> Doc Any
forall a b. (a -> b) -> a -> b
$ MemImpl sym -> Mem sym
forall sym. MemImpl sym -> Mem sym
C.memImplHeap MemImpl sym
mem)]


filterSubstitution ::
  C.IsSymInterface sym =>
  sym ->
  MapF (W4.SymExpr sym) (FixpointEntry sym) ->
  MapF (W4.SymExpr sym) (FixpointEntry sym)
filterSubstitution :: forall sym.
IsSymInterface sym =>
sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
filterSubstitution sym
sym MapF (SymExpr sym) (FixpointEntry sym)
substitution =
  -- TODO: fixpoint
  let uninterp_constants :: Set (Some (SymExpr sym))
uninterp_constants = (forall (s :: BaseType).
 FixpointEntry sym s -> Set (Some (SymExpr sym)))
-> MapF (SymExpr sym) (FixpointEntry sym)
-> Set (Some (SymExpr sym))
forall m (e :: BaseType -> Type).
Monoid m =>
(forall (s :: BaseType). e s -> m) -> MapF (SymExpr sym) e -> m
forall k (t :: (k -> Type) -> Type) m (e :: k -> Type).
(FoldableF t, Monoid m) =>
(forall (s :: k). e s -> m) -> t e -> m
foldMapF
        ((Some (BoundVar sym) -> Some (SymExpr sym))
-> Set (Some (BoundVar sym)) -> Set (Some (SymExpr sym))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((forall (tp :: BaseType). BoundVar sym tp -> SymExpr sym tp)
-> Some (BoundVar sym) -> Some (SymExpr sym)
forall {k} (f :: k -> Type) (g :: k -> Type).
(forall (tp :: k). f tp -> g tp) -> Some f -> Some g
C.mapSome ((forall (tp :: BaseType). BoundVar sym tp -> SymExpr sym tp)
 -> Some (BoundVar sym) -> Some (SymExpr sym))
-> (forall (tp :: BaseType). BoundVar sym tp -> SymExpr sym tp)
-> Some (BoundVar sym)
-> Some (SymExpr sym)
forall a b. (a -> b) -> a -> b
$ sym -> BoundVar sym tp -> SymExpr sym tp
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
forall (tp :: BaseType). sym -> BoundVar sym tp -> SymExpr sym tp
W4.varExpr sym
sym) (Set (Some (BoundVar sym)) -> Set (Some (SymExpr sym)))
-> (FixpointEntry sym s -> Set (Some (BoundVar sym)))
-> FixpointEntry sym s
-> Set (Some (SymExpr sym))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym -> SymExpr sym s -> Set (Some (BoundVar sym))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
forall (tp :: BaseType).
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
W4.exprUninterpConstants sym
sym (SymExpr sym s -> Set (Some (BoundVar sym)))
-> (FixpointEntry sym s -> SymExpr sym s)
-> FixpointEntry sym s
-> Set (Some (BoundVar sym))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FixpointEntry sym s -> SymExpr sym s
forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
bodyValue)
        MapF (SymExpr sym) (FixpointEntry sym)
substitution
  in
  (forall (tp :: BaseType).
 SymExpr sym tp -> FixpointEntry sym tp -> Bool)
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
forall {v} (k :: v -> Type) (f :: v -> Type).
(forall (tp :: v). k tp -> f tp -> Bool) -> MapF k f -> MapF k f
MapF.filterWithKey (\SymExpr sym tp
variable FixpointEntry sym tp
_entry -> Some (SymExpr sym) -> Set (Some (SymExpr sym)) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (SymExpr sym tp -> Some (SymExpr sym)
forall k (f :: k -> Type) (x :: k). f x -> Some f
C.Some SymExpr sym tp
variable) Set (Some (SymExpr sym))
uninterp_constants) MapF (SymExpr sym) (FixpointEntry sym)
substitution

-- find widening variables that are actually the same (up to syntactic equality)
-- and can be substituted for each other
uninterpretedConstantEqualitySubstitution ::
  forall sym .
  C.IsSymInterface sym =>
  sym ->
  MapF (W4.SymExpr sym) (FixpointEntry sym) ->
  (MapF (W4.SymExpr sym) (FixpointEntry sym), MapF (W4.SymExpr sym) (W4.SymExpr sym))
uninterpretedConstantEqualitySubstitution :: forall sym.
IsSymInterface sym =>
sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> (MapF (SymExpr sym) (FixpointEntry sym),
    MapF (SymExpr sym) (SymExpr sym))
uninterpretedConstantEqualitySubstitution sym
_sym MapF (SymExpr sym) (FixpointEntry sym)
substitution =
  let reverse_substitution :: MapF (FixpointEntry sym) (SymExpr sym)
reverse_substitution = (forall (s :: BaseType).
 MapF (FixpointEntry sym) (SymExpr sym)
 -> SymExpr sym s
 -> FixpointEntry sym s
 -> MapF (FixpointEntry sym) (SymExpr sym))
-> MapF (FixpointEntry sym) (SymExpr sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (FixpointEntry sym) (SymExpr sym)
forall {v} b (k :: v -> Type) (a :: v -> Type).
(forall (s :: v). b -> k s -> a s -> b) -> b -> MapF k a -> b
MapF.foldlWithKey'
        (\MapF (FixpointEntry sym) (SymExpr sym)
accumulator SymExpr sym s
variable FixpointEntry sym s
entry -> FixpointEntry sym s
-> SymExpr sym s
-> MapF (FixpointEntry sym) (SymExpr sym)
-> MapF (FixpointEntry sym) (SymExpr sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert FixpointEntry sym s
entry SymExpr sym s
variable MapF (FixpointEntry sym) (SymExpr sym)
accumulator)
        MapF (FixpointEntry sym) (SymExpr sym)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
        MapF (SymExpr sym) (FixpointEntry sym)
substitution
      uninterpreted_constant_substitution :: MapF (SymExpr sym) (SymExpr sym)
uninterpreted_constant_substitution = (forall (x :: BaseType). FixpointEntry sym x -> SymExpr sym x)
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (SymExpr sym)
forall {k} (m :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorF m =>
(forall (x :: k). f x -> g x) -> m f -> m g
forall (f :: BaseType -> Type) (g :: BaseType -> Type).
(forall (x :: BaseType). f x -> g x)
-> MapF (SymExpr sym) f -> MapF (SymExpr sym) g
fmapF
        (\FixpointEntry sym x
entry -> Maybe (SymExpr sym x) -> SymExpr sym x
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (SymExpr sym x) -> SymExpr sym x)
-> Maybe (SymExpr sym x) -> SymExpr sym x
forall a b. (a -> b) -> a -> b
$ FixpointEntry sym x
-> MapF (FixpointEntry sym) (SymExpr sym) -> Maybe (SymExpr sym x)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup FixpointEntry sym x
entry MapF (FixpointEntry sym) (SymExpr sym)
reverse_substitution)
        MapF (SymExpr sym) (FixpointEntry sym)
substitution
      normal_substitution :: MapF (SymExpr sym) (FixpointEntry sym)
normal_substitution = (forall (tp :: BaseType).
 SymExpr sym tp -> FixpointEntry sym tp -> Bool)
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
forall {v} (k :: v -> Type) (f :: v -> Type).
(forall (tp :: v). k tp -> f tp -> Bool) -> MapF k f -> MapF k f
MapF.filterWithKey
        (\SymExpr sym tp
variable FixpointEntry sym tp
_entry ->
          (tp :~: tp) -> Maybe (tp :~: tp)
forall a. a -> Maybe a
Just tp :~: tp
forall {k} (a :: k). a :~: a
Refl Maybe (tp :~: tp) -> Maybe (tp :~: tp) -> Bool
forall a. Eq a => a -> a -> Bool
== SymExpr sym tp -> SymExpr sym tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
SymExpr sym a -> SymExpr sym b -> Maybe (a :~: b)
W4.testEquality SymExpr sym tp
variable (Maybe (SymExpr sym tp) -> SymExpr sym tp
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (SymExpr sym tp) -> SymExpr sym tp)
-> Maybe (SymExpr sym tp) -> SymExpr sym tp
forall a b. (a -> b) -> a -> b
$ SymExpr sym tp
-> MapF (SymExpr sym) (SymExpr sym) -> Maybe (SymExpr sym tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup SymExpr sym tp
variable MapF (SymExpr sym) (SymExpr sym)
uninterpreted_constant_substitution))
        MapF (SymExpr sym) (FixpointEntry sym)
substitution
  in
  (MapF (SymExpr sym) (FixpointEntry sym)
normal_substitution, MapF (SymExpr sym) (SymExpr sym)
uninterpreted_constant_substitution)


userSymbol' :: String -> W4.SolverSymbol
userSymbol' :: String -> SolverSymbol
userSymbol' = SolverSymbol
-> Either SolverSymbolError SolverSymbol -> SolverSymbol
forall b a. b -> Either a b -> b
fromRight (String -> [String] -> SolverSymbol
forall a. HasCallStack => String -> [String] -> a
C.panic String
"SimpleLoopFixpoint.userSymbol'" []) (Either SolverSymbolError SolverSymbol -> SolverSymbol)
-> (String -> Either SolverSymbolError SolverSymbol)
-> String
-> SolverSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either SolverSymbolError SolverSymbol
W4.userSymbol


-- | 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 limititations.
--   Most notibly, it only really works properly for functions
--   consiting 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 strucutre are not
--   checked.
--
--   The basic use case here is for verifiying 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 ::
  forall sym ext p rtp blocks init ret .
  (C.IsSymInterface sym, 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 -} ->
  (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), W4.Pred sym)) ->
  IO (C.ExecutionFeature p sym ext rtp)
simpleLoopFixpoint :: forall sym ext p rtp (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, ?memOpts::MemOptions) =>
sym
-> CFG ext blocks init ret
-> GlobalVar Mem
-> (MapF (SymExpr sym) (FixpointEntry sym)
    -> Pred sym -> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym))
-> IO (ExecutionFeature p sym ext rtp)
simpleLoopFixpoint sym
sym cfg :: CFG ext blocks init ret
cfg@C.CFG{Bimap BreakpointName (Some (BlockID blocks))
FnHandle init ret
BlockID blocks init
BlockMap ext blocks ret
cfgHandle :: FnHandle init ret
cfgBlockMap :: BlockMap ext blocks ret
cfgEntryBlockID :: BlockID blocks init
cfgBreakpoints :: Bimap BreakpointName (Some (BlockID blocks))
cfgHandle :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgBlockMap :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgEntryBlockID :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgBreakpoints :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Bimap BreakpointName (Some (BlockID blocks))
..} GlobalVar Mem
mem_var MapF (SymExpr sym) (FixpointEntry sym)
-> Pred sym -> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym)
fixpoint_func = do
  let ?ptrWidth = forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64

  OptionSetting BaseIntegerType
verbSetting <- ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
W4.getOptionSetting ConfigOption BaseIntegerType
W4.verbosity (Config -> IO (OptionSetting BaseIntegerType))
-> Config -> IO (OptionSetting BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
W4.getConfiguration sym
sym
  Natural
verb <- Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> IO Integer -> IO Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
W4.getOpt OptionSetting BaseIntegerType
verbSetting

  -- 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 :: WTOComponent a -> [a]
flattenWTOComponent = \case
        C.SCC C.SCCData{a
[WTOComponent a]
wtoHead :: a
wtoComps :: [WTOComponent a]
wtoHead :: forall n. SCC n -> n
wtoComps :: forall n. SCC n -> [WTOComponent n]
..} ->  a
wtoHead a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (WTOComponent a -> [a]) -> [WTOComponent a] -> [a]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap WTOComponent a -> [a]
flattenWTOComponent [WTOComponent a]
wtoComps
        C.Vertex a
v -> [a
v]
  let loop_map :: Map (Some (BlockID blocks)) [Some (BlockID blocks)]
loop_map = [(Some (BlockID blocks), [Some (BlockID blocks)])]
-> Map (Some (BlockID blocks)) [Some (BlockID blocks)]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Some (BlockID blocks), [Some (BlockID blocks)])]
 -> Map (Some (BlockID blocks)) [Some (BlockID blocks)])
-> [(Some (BlockID blocks), [Some (BlockID blocks)])]
-> Map (Some (BlockID blocks)) [Some (BlockID blocks)]
forall a b. (a -> b) -> a -> b
$ (WTOComponent (Some (BlockID blocks))
 -> Maybe (Some (BlockID blocks), [Some (BlockID blocks)]))
-> [WTOComponent (Some (BlockID blocks))]
-> [(Some (BlockID blocks), [Some (BlockID blocks)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
        (\case
          C.SCC C.SCCData{[WTOComponent (Some (BlockID blocks))]
Some (BlockID blocks)
wtoHead :: forall n. SCC n -> n
wtoComps :: forall n. SCC n -> [WTOComponent n]
wtoHead :: Some (BlockID blocks)
wtoComps :: [WTOComponent (Some (BlockID blocks))]
..} -> (Some (BlockID blocks), [Some (BlockID blocks)])
-> Maybe (Some (BlockID blocks), [Some (BlockID blocks)])
forall a. a -> Maybe a
Just (Some (BlockID blocks)
wtoHead, Some (BlockID blocks)
wtoHead Some (BlockID blocks)
-> [Some (BlockID blocks)] -> [Some (BlockID blocks)]
forall a. a -> [a] -> [a]
: (WTOComponent (Some (BlockID blocks)) -> [Some (BlockID blocks)])
-> [WTOComponent (Some (BlockID blocks))]
-> [Some (BlockID blocks)]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap WTOComponent (Some (BlockID blocks)) -> [Some (BlockID blocks)]
forall {a}. WTOComponent a -> [a]
flattenWTOComponent [WTOComponent (Some (BlockID blocks))]
wtoComps)
          C.Vertex{} -> Maybe (Some (BlockID blocks), [Some (BlockID blocks)])
forall a. Maybe a
Nothing)
        (CFG ext blocks init ret -> [WTOComponent (Some (BlockID blocks))]
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> [WTOComponent (Some (BlockID blocks))]
C.cfgWeakTopologicalOrdering CFG ext blocks init ret
cfg)

  IORef (FixpointState sym blocks)
fixpoint_state_ref <- forall a. a -> IO (IORef a)
newIORef @(FixpointState sym blocks) FixpointState sym blocks
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointState sym blocks
BeforeFixpoint

  ExecutionFeature p sym ext rtp
-> IO (ExecutionFeature p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeature p sym ext rtp
 -> IO (ExecutionFeature p sym ext rtp))
-> ExecutionFeature p sym ext rtp
-> IO (ExecutionFeature p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ (ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall p sym ext rtp.
(ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
C.ExecutionFeature ((ExecState p sym ext rtp
  -> IO (ExecutionFeatureResult p sym ext rtp))
 -> ExecutionFeature p sym ext rtp)
-> (ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall a b. (a -> b) -> a -> b
$ \ExecState p sym ext rtp
exec_state -> do
    let ?logMessage = \String
msg -> Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Natural
verb Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= (Natural
3 :: Natural)) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          let h :: Handle
h = SimContext p sym ext -> Handle
forall personality sym ext.
SimContext personality sym ext -> Handle
C.printHandle (SimContext p sym ext -> Handle) -> SimContext p sym ext -> Handle
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ExecState p sym ext rtp
exec_state
          Handle -> String -> IO ()
System.IO.hPutStrLn Handle
h String
msg
          Handle -> IO ()
System.IO.hFlush Handle
h
    FixpointState sym blocks
fixpoint_state <- IORef (FixpointState sym blocks) -> IO (FixpointState sym blocks)
forall a. IORef a -> IO a
readIORef IORef (FixpointState sym blocks)
fixpoint_state_ref
    SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
C.withBackend (ExecState p sym ext rtp -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ExecState p sym ext rtp
exec_state) ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> IO (ExecutionFeatureResult p sym ext rtp))
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
     case ExecState p sym ext rtp
exec_state of
      C.RunningState (C.RunBlockStart BlockID blocks args
block_id) SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state
        | FnHandle init ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
C.SomeHandle FnHandle init ret
cfgHandle SomeHandle -> SomeHandle -> Bool
forall a. Eq a => a -> a -> Bool
== CallFrame sym ext blocks r args -> SomeHandle
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> SomeHandle
C.frameHandle (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (CallFrame sym ext blocks r args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (CallFrame sym ext blocks r args)
-> CallFrame sym ext blocks r args
forall s a. s -> Getting a s a -> a
^. Getting
  (CallFrame sym ext blocks r args)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
  (CallFrame sym ext blocks r args)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame)

        -- make sure the types match
        , Just blocks :~: blocks
Refl <- Assignment (Assignment TypeRepr) blocks
-> Assignment (Assignment TypeRepr) blocks
-> Maybe (blocks :~: blocks)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx (Ctx CrucibleType)) (b :: Ctx (Ctx CrucibleType)).
Assignment (Assignment TypeRepr) a
-> Assignment (Assignment TypeRepr) b -> Maybe (a :~: b)
W4.testEquality
            ((forall (x :: Ctx CrucibleType).
 Block ext blocks ret x -> Assignment TypeRepr x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (Block ext blocks ret) x
   -> Assignment (Assignment TypeRepr) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: Ctx CrucibleType -> Type)
       (g :: Ctx CrucibleType -> Type).
(forall (x :: Ctx CrucibleType). f x -> g x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment f x -> Assignment g x
fmapFC Block ext blocks ret x -> CtxRepr x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
forall (x :: Ctx CrucibleType).
Block ext blocks ret x -> Assignment TypeRepr x
C.blockInputs BlockMap ext blocks ret
cfgBlockMap)
            ((forall (x :: Ctx CrucibleType).
 Block ext blocks r x -> Assignment TypeRepr x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (Block ext blocks r) x
   -> Assignment (Assignment TypeRepr) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: Ctx CrucibleType -> Type)
       (g :: Ctx CrucibleType -> Type).
(forall (x :: Ctx CrucibleType). f x -> g x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment f x -> Assignment g x
fmapFC Block ext blocks r x -> CtxRepr x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
forall (x :: Ctx CrucibleType).
Block ext blocks r x -> Assignment TypeRepr x
C.blockInputs (Assignment (Block ext blocks r) blocks
 -> Assignment (Assignment TypeRepr) blocks)
-> Assignment (Block ext blocks r) blocks
-> Assignment (Assignment TypeRepr) blocks
forall a b. (a -> b) -> a -> b
$ CallFrame sym ext blocks r args
-> Assignment (Block ext blocks r) blocks
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret
C.frameBlockMap (CallFrame sym ext blocks r args
 -> Assignment (Block ext blocks r) blocks)
-> CallFrame sym ext blocks r args
-> Assignment (Block ext blocks r) blocks
forall a b. (a -> b) -> a -> b
$ SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (CallFrame sym ext blocks r args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (CallFrame sym ext blocks r args)
-> CallFrame sym ext blocks r args
forall s a. s -> Getting a s a -> a
^. Getting
  (CallFrame sym ext blocks r args)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
  (CallFrame sym ext blocks r args)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame)

          -- loop map is what we computed above, is this state at a loop header
        , Some (BlockID blocks)
-> Map (Some (BlockID blocks)) [Some (BlockID blocks)] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member (BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
C.Some BlockID blocks args
block_id) Map (Some (BlockID blocks)) [Some (BlockID blocks)]
Map (Some (BlockID blocks)) [Some (BlockID blocks)]
loop_map ->

            bak
-> GlobalVar Mem
-> (MapF (SymExpr sym) (FixpointEntry sym)
    -> Pred sym -> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym))
-> BlockID blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> FixpointState sym blocks
-> IORef (FixpointState sym blocks)
-> IO (ExecutionFeatureResult p sym ext rtp)
forall sym bak ext p rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType).
(IsSymBackend sym bak, HasLLVMAnn sym, ?memOpts::MemOptions,
 ?logMessage::String -> IO ()) =>
bak
-> GlobalVar Mem
-> (MapF (SymExpr sym) (FixpointEntry sym)
    -> Pred sym -> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym))
-> BlockID blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> FixpointState sym blocks
-> IORef (FixpointState sym blocks)
-> IO (ExecutionFeatureResult p sym ext rtp)
advanceFixpointState bak
bak GlobalVar Mem
mem_var MapF (SymExpr sym) (FixpointEntry sym)
-> Pred sym -> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym)
fixpoint_func BlockID blocks args
block_id SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state FixpointState sym blocks
FixpointState sym blocks
fixpoint_state IORef (FixpointState sym blocks)
IORef (FixpointState sym blocks)
fixpoint_state_ref

        | Bool
otherwise -> do
            ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint: RunningState: RunBlockStart: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BlockID blocks args -> String
forall a. Show a => a -> String
show BlockID blocks args
block_id
            ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange


      -- TODO: maybe need to rework this, so that we are sure to capture even concrete exits from the loop.
      C.SymbolicBranchState Pred sym
branch_condition PausedFrame p sym ext rtp f
true_frame PausedFrame p sym ext rtp f
false_frame CrucibleBranchTarget f postdom_args
_target SimState p sym ext rtp f ('Just args)
sim_state
          | Just FixpointRecord sym blocks
fixpoint_record <- FixpointState sym blocks -> Maybe (FixpointRecord sym blocks)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointState sym blocks -> Maybe (FixpointRecord sym blocks)
fixpointRecord FixpointState sym blocks
fixpoint_state
          , Just [Some (BlockID blocks)]
loop_body_some_block_ids <- Some (BlockID blocks)
-> Map (Some (BlockID blocks)) [Some (BlockID blocks)]
-> Maybe [Some (BlockID blocks)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (FixpointRecord sym blocks -> Some (BlockID blocks)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> Some (BlockID blocks)
fixpointBlockId FixpointRecord sym blocks
fixpoint_record) Map (Some (BlockID blocks)) [Some (BlockID blocks)]
loop_map
          , JustPausedFrameTgtId Some (BlockID b)
true_frame_some_block_id <- PausedFrame p sym ext rtp f -> MaybePausedFrameTgtId f
forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> MaybePausedFrameTgtId f
pausedFrameTgtId PausedFrame p sym ext rtp f
true_frame
          , JustPausedFrameTgtId Some (BlockID b)
false_frame_some_block_id <- PausedFrame p sym ext rtp f -> MaybePausedFrameTgtId f
forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> MaybePausedFrameTgtId f
pausedFrameTgtId PausedFrame p sym ext rtp f
false_frame
          , FnHandle init ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
C.SomeHandle FnHandle init ret
cfgHandle SomeHandle -> SomeHandle -> Bool
forall a. Eq a => a -> a -> Bool
== CallFrame sym ext b r args -> SomeHandle
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> SomeHandle
C.frameHandle (SimState p sym ext rtp f ('Just args)
sim_state SimState p sym ext rtp f ('Just args)
-> Getting
     (CallFrame sym ext b r args)
     (SimState p sym ext rtp f ('Just args))
     (CallFrame sym ext b r args)
-> CallFrame sym ext b r args
forall s a. s -> Getting a s a -> a
^. Getting
  (CallFrame sym ext b r args)
  (SimState p sym ext rtp f ('Just args))
  (CallFrame sym ext b r args)
(CallFrame sym ext b r args
 -> Const (CallFrame sym ext b r args) (CallFrame sym ext b r args))
-> SimState p sym ext rtp (CrucibleLang b r) ('Just args)
-> Const
     (CallFrame sym ext b r args)
     (SimState p sym ext rtp (CrucibleLang b r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame)
          , Just blocks :~: b
Refl <- Assignment (Assignment TypeRepr) blocks
-> Assignment (Assignment TypeRepr) b -> Maybe (blocks :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx (Ctx CrucibleType)) (b :: Ctx (Ctx CrucibleType)).
Assignment (Assignment TypeRepr) a
-> Assignment (Assignment TypeRepr) b -> Maybe (a :~: b)
W4.testEquality
              ((forall (x :: Ctx CrucibleType).
 Block ext blocks ret x -> Assignment TypeRepr x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (Block ext blocks ret) x
   -> Assignment (Assignment TypeRepr) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: Ctx CrucibleType -> Type)
       (g :: Ctx CrucibleType -> Type).
(forall (x :: Ctx CrucibleType). f x -> g x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment f x -> Assignment g x
fmapFC Block ext blocks ret x -> CtxRepr x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
forall (x :: Ctx CrucibleType).
Block ext blocks ret x -> Assignment TypeRepr x
C.blockInputs BlockMap ext blocks ret
cfgBlockMap)
              ((forall (x :: Ctx CrucibleType).
 Block ext b r x -> Assignment TypeRepr x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (Block ext b r) x -> Assignment (Assignment TypeRepr) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: Ctx CrucibleType -> Type)
       (g :: Ctx CrucibleType -> Type).
(forall (x :: Ctx CrucibleType). f x -> g x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment f x -> Assignment g x
fmapFC Block ext b r x -> CtxRepr x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
forall (x :: Ctx CrucibleType).
Block ext b r x -> Assignment TypeRepr x
C.blockInputs (Assignment (Block ext b r) b
 -> Assignment (Assignment TypeRepr) b)
-> Assignment (Block ext b r) b
-> Assignment (Assignment TypeRepr) b
forall a b. (a -> b) -> a -> b
$ CallFrame sym ext b r args -> Assignment (Block ext b r) b
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret
C.frameBlockMap (CallFrame sym ext b r args -> Assignment (Block ext b r) b)
-> CallFrame sym ext b r args -> Assignment (Block ext b r) b
forall a b. (a -> b) -> a -> b
$ SimState p sym ext rtp f ('Just args)
sim_state SimState p sym ext rtp f ('Just args)
-> Getting
     (CallFrame sym ext b r args)
     (SimState p sym ext rtp f ('Just args))
     (CallFrame sym ext b r args)
-> CallFrame sym ext b r args
forall s a. s -> Getting a s a -> a
^. Getting
  (CallFrame sym ext b r args)
  (SimState p sym ext rtp f ('Just args))
  (CallFrame sym ext b r args)
(CallFrame sym ext b r args
 -> Const (CallFrame sym ext b r args) (CallFrame sym ext b r args))
-> SimState p sym ext rtp (CrucibleLang b r) ('Just args)
-> Const
     (CallFrame sym ext b r args)
     (SimState p sym ext rtp (CrucibleLang b r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame)
          , Some (BlockID b) -> [Some (BlockID b)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
elem Some (BlockID b)
true_frame_some_block_id [Some (BlockID blocks)]
[Some (BlockID b)]
loop_body_some_block_ids Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Some (BlockID b) -> [Some (BlockID b)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
elem Some (BlockID b)
false_frame_some_block_id [Some (BlockID blocks)]
[Some (BlockID b)]
loop_body_some_block_ids -> do

            (Pred sym
loop_condition, PausedFrame p sym ext rtp f
inside_loop_frame, PausedFrame p sym ext rtp f
outside_loop_frame) <-
              if Some (BlockID b) -> [Some (BlockID b)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
elem Some (BlockID b)
true_frame_some_block_id [Some (BlockID blocks)]
[Some (BlockID b)]
loop_body_some_block_ids
              then
                (Pred sym, PausedFrame p sym ext rtp f,
 PausedFrame p sym ext rtp f)
-> IO
     (Pred sym, PausedFrame p sym ext rtp f,
      PausedFrame p sym ext rtp f)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
branch_condition, PausedFrame p sym ext rtp f
true_frame, PausedFrame p sym ext rtp f
false_frame)
              else do
                Pred sym
not_branch_condition <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred sym
sym Pred sym
branch_condition
                (Pred sym, PausedFrame p sym ext rtp f,
 PausedFrame p sym ext rtp f)
-> IO
     (Pred sym, PausedFrame p sym ext rtp f,
      PausedFrame p sym ext rtp f)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
not_branch_condition, PausedFrame p sym ext rtp f
false_frame, PausedFrame p sym ext rtp f
true_frame)

            (Pred sym
condition, PausedFrame p sym ext rtp f
frame) <- case FixpointState sym blocks
fixpoint_state of
              FixpointState sym blocks
BeforeFixpoint -> String -> [String] -> IO (Pred sym, PausedFrame p sym ext rtp f)
forall a. HasCallStack => String -> [String] -> a
C.panic String
"SimpleLoopFixpoint.simpleLoopFixpoint:" [String
"BeforeFixpoint"]

              ComputeFixpoint FixpointRecord sym blocks
_fixpoint_record -> do
                -- continue in the loop
                ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint: SymbolicBranchState: ComputeFixpoint"
                IORef (FixpointState sym blocks)
-> FixpointState sym blocks -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (FixpointState sym blocks)
fixpoint_state_ref (FixpointState sym blocks -> IO ())
-> FixpointState sym blocks -> IO ()
forall a b. (a -> b) -> a -> b
$
                  FixpointRecord sym blocks -> FixpointState sym blocks
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> FixpointState sym blocks
ComputeFixpoint FixpointRecord sym blocks
fixpoint_record { fixpointLoopCondition = Just loop_condition }
                (Pred sym, PausedFrame p sym ext rtp f)
-> IO (Pred sym, PausedFrame p sym ext rtp f)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
loop_condition, PausedFrame p sym ext rtp f
inside_loop_frame)

              CheckFixpoint FixpointRecord sym blocks
_fixpoint_record LoopIndexBound sym
_loop_bound -> do
                -- continue in the loop
                ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint: SymbolicBranchState: CheckFixpoint"
                (Pred sym, PausedFrame p sym ext rtp f)
-> IO (Pred sym, PausedFrame p sym ext rtp f)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
loop_condition, PausedFrame p sym ext rtp f
inside_loop_frame)

              AfterFixpoint FixpointRecord sym blocks
_fixpoint_record LoopIndexBound sym
_loop_bound -> do
                -- break out of the loop
                ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint: SymbolicBranchState: AfterFixpoint"
                Pred sym
not_loop_condition <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred sym
sym Pred sym
loop_condition
                (Pred sym, PausedFrame p sym ext rtp f)
-> IO (Pred sym, PausedFrame p sym ext rtp f)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
not_loop_condition, PausedFrame p sym ext rtp f
outside_loop_frame)

            ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
W4.getCurrentProgramLoc sym
sym
            bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
C.addAssumption bak
bak (Assumption sym -> IO ()) -> Assumption sym -> IO ()
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Maybe ProgramLoc -> Pred sym -> Assumption sym
forall (e :: BaseType -> Type).
ProgramLoc
-> Maybe ProgramLoc -> e BaseBoolType -> CrucibleAssumption e
C.BranchCondition ProgramLoc
loc (PausedFrame p sym ext rtp f -> Maybe ProgramLoc
forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> Maybe ProgramLoc
C.pausedLoc PausedFrame p sym ext rtp f
frame) Pred sym
condition
            ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNewState (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp)
-> IO (ExecState p sym ext rtp)
-> IO (ExecutionFeatureResult p sym ext rtp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
              ReaderT
  (SimState p sym ext rtp f ('Just args))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp f ('Just args)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT
                (PausedFrame p sym ext rtp f
-> ValueFromFrame p sym ext rtp f
-> ReaderT
     (SimState p sym ext rtp f ('Just args))
     IO
     (ExecState p sym ext rtp)
forall sym p ext rtp f g (ba :: Maybe (Ctx CrucibleType)).
IsSymInterface sym =>
PausedFrame p sym ext rtp f
-> ValueFromFrame p sym ext rtp f -> ExecCont p sym ext rtp g ba
C.resumeFrame (PausedFrame p sym ext rtp f -> PausedFrame p sym ext rtp f
forall p sym ext rtp g.
PausedFrame p sym ext rtp g -> PausedFrame p sym ext rtp g
C.forgetPostdomFrame PausedFrame p sym ext rtp f
frame) (ValueFromFrame p sym ext rtp f
 -> ReaderT
      (SimState p sym ext rtp f ('Just args))
      IO
      (ExecState p sym ext rtp))
-> ValueFromFrame p sym ext rtp f
-> ReaderT
     (SimState p sym ext rtp f ('Just args))
     IO
     (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ SimState p sym ext rtp f ('Just args)
sim_state SimState p sym ext rtp f ('Just args)
-> Getting
     (ValueFromFrame p sym ext rtp f)
     (SimState p sym ext rtp f ('Just args))
     (ValueFromFrame p sym ext rtp f)
-> ValueFromFrame p sym ext rtp f
forall s a. s -> Getting a s a -> a
^. ((ActiveTree p sym ext rtp f ('Just args)
 -> Const
      (ValueFromFrame p sym ext rtp f)
      (ActiveTree p sym ext rtp f ('Just args)))
-> SimState p sym ext rtp f ('Just args)
-> Const
     (ValueFromFrame p sym ext rtp f)
     (SimState p sym ext rtp f ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
C.stateTree ((ActiveTree p sym ext rtp f ('Just args)
  -> Const
       (ValueFromFrame p sym ext rtp f)
       (ActiveTree p sym ext rtp f ('Just args)))
 -> SimState p sym ext rtp f ('Just args)
 -> Const
      (ValueFromFrame p sym ext rtp f)
      (SimState p sym ext rtp f ('Just args)))
-> ((ValueFromFrame p sym ext rtp f
     -> Const
          (ValueFromFrame p sym ext rtp f) (ValueFromFrame p sym ext rtp f))
    -> ActiveTree p sym ext rtp f ('Just args)
    -> Const
         (ValueFromFrame p sym ext rtp f)
         (ActiveTree p sym ext rtp f ('Just args)))
-> Getting
     (ValueFromFrame p sym ext rtp f)
     (SimState p sym ext rtp f ('Just args))
     (ValueFromFrame p sym ext rtp f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValueFromFrame p sym ext rtp f
 -> Const
      (ValueFromFrame p sym ext rtp f) (ValueFromFrame p sym ext rtp f))
-> ActiveTree p sym ext rtp f ('Just args)
-> Const
     (ValueFromFrame p sym ext rtp f)
     (ActiveTree p sym ext rtp f ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(ValueFromFrame p sym ext root f1
 -> f2 (ValueFromFrame p sym ext root f1))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args)
C.actContext))
                SimState p sym ext rtp f ('Just args)
sim_state

      ExecState p sym ext rtp
_ -> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange


advanceFixpointState ::
  forall sym bak ext p rtp blocks r args .
  (C.IsSymBackend sym bak, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) =>
  bak ->
  C.GlobalVar C.Mem ->
  (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), W4.Pred sym)) ->
  C.BlockID blocks args ->
  C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) ->
  FixpointState sym blocks ->
  IORef (FixpointState sym blocks) ->
  IO (C.ExecutionFeatureResult p sym ext rtp)

advanceFixpointState :: forall sym bak ext p rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType).
(IsSymBackend sym bak, HasLLVMAnn sym, ?memOpts::MemOptions,
 ?logMessage::String -> IO ()) =>
bak
-> GlobalVar Mem
-> (MapF (SymExpr sym) (FixpointEntry sym)
    -> Pred sym -> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym))
-> BlockID blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> FixpointState sym blocks
-> IORef (FixpointState sym blocks)
-> IO (ExecutionFeatureResult p sym ext rtp)
advanceFixpointState bak
bak GlobalVar Mem
mem_var MapF (SymExpr sym) (FixpointEntry sym)
-> Pred sym -> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym)
fixpoint_func BlockID blocks args
block_id SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state FixpointState sym blocks
fixpoint_state IORef (FixpointState sym blocks)
fixpoint_state_ref =
  let ?ptrWidth = forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64 in
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
C.backendGetSym bak
bak in
  case FixpointState sym blocks
fixpoint_state of
    FixpointState sym blocks
BeforeFixpoint -> do
      ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint: RunningState: BeforeFixpoint -> ComputeFixpoint"
      FrameIdentifier
assumption_frame_identifier <- bak -> IO FrameIdentifier
forall sym bak. IsSymBackend sym bak => bak -> IO FrameIdentifier
C.pushAssumptionFrame bak
bak
      let mem_impl :: MemImpl sym
mem_impl = Maybe (MemImpl sym) -> MemImpl sym
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (MemImpl sym) -> MemImpl sym)
-> Maybe (MemImpl sym) -> MemImpl sym
forall a b. (a -> b) -> a -> b
$ GlobalVar Mem -> SymGlobalState sym -> Maybe (RegValue sym Mem)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
C.lookupGlobal GlobalVar Mem
mem_var (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^. Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
  (SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals)
      let res_mem_impl :: MemImpl sym
res_mem_impl = MemImpl sym
mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" $ C.memImplHeap mem_impl }
      IORef (FixpointState sym blocks)
-> FixpointState sym blocks -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (FixpointState sym blocks)
fixpoint_state_ref (FixpointState sym blocks -> IO ())
-> FixpointState sym blocks -> IO ()
forall a b. (a -> b) -> a -> b
$ FixpointRecord sym blocks -> FixpointState sym blocks
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> FixpointState sym blocks
ComputeFixpoint (FixpointRecord sym blocks -> FixpointState sym blocks)
-> FixpointRecord sym blocks -> FixpointState sym blocks
forall a b. (a -> b) -> a -> b
$
        FixpointRecord
        { fixpointBlockId :: Some (BlockID blocks)
fixpointBlockId = BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
C.Some BlockID blocks args
block_id
        , fixpointAssumptionFrameIdentifier :: FrameIdentifier
fixpointAssumptionFrameIdentifier = FrameIdentifier
assumption_frame_identifier
        , fixpointSubstitution :: MapF (SymExpr sym) (FixpointEntry sym)
fixpointSubstitution = MapF (SymExpr sym) (FixpointEntry sym)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
        , fixpointRegMap :: RegMap sym args
fixpointRegMap = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (RegMap sym args)
-> RegMap sym args
forall s a. s -> Getting a s a -> a
^. ((CallFrame sym ext blocks r args
 -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame ((CallFrame sym ext blocks r args
  -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      (RegMap sym args)
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> CallFrame sym ext blocks r args
    -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (RegMap sym args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> CallFrame sym ext blocks r args
-> Const (RegMap sym args) (CallFrame sym ext blocks r args)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
C.frameRegs)
        , fixpointMemSubstitution :: Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution = Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
forall k a. Map k a
Map.empty
        , fixpointLoopCondition :: Maybe (Pred sym)
fixpointLoopCondition = Maybe (Pred sym)
forall a. Maybe a
Nothing -- we don't know the loop condition yet
        }
      ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeatureResult p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureModifiedState (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp)
-> ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall a b. (a -> b) -> a -> b
$ RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType).
RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
C.RunningState (BlockID blocks args -> RunningStateInfo blocks args
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
BlockID blocks args -> RunningStateInfo blocks args
C.RunBlockStart BlockID blocks args
block_id) (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> ExecState p sym ext rtp)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall a b. (a -> b) -> a -> b
$
        SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall a b. a -> (a -> b) -> b
& (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> (SymGlobalState sym -> SymGlobalState sym)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ GlobalVar Mem
-> RegValue sym Mem -> SymGlobalState sym -> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
C.insertGlobal GlobalVar Mem
mem_var RegValue sym Mem
MemImpl sym
res_mem_impl

    ComputeFixpoint FixpointRecord sym blocks
fixpoint_record
      | FixpointRecord { fixpointRegMap :: ()
fixpointRegMap = RegMap sym args
reg_map } <- FixpointRecord sym blocks
fixpoint_record
      , Just args :~: args
Refl <- Assignment TypeRepr args
-> Assignment TypeRepr args -> Maybe (args :~: args)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
Assignment TypeRepr a -> Assignment TypeRepr b -> Maybe (a :~: b)
W4.testEquality
          ((forall (x :: CrucibleType). RegEntry sym x -> TypeRepr x)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> Assignment TypeRepr x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC RegEntry sym x -> TypeRepr x
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
forall (x :: CrucibleType). RegEntry sym x -> TypeRepr x
C.regType (Assignment (RegEntry sym) args -> Assignment TypeRepr args)
-> Assignment (RegEntry sym) args -> Assignment TypeRepr args
forall a b. (a -> b) -> a -> b
$ RegMap sym args -> Assignment (RegEntry sym) args
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap RegMap sym args
reg_map)
          ((forall (x :: CrucibleType). RegEntry sym x -> TypeRepr x)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> Assignment TypeRepr x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC RegEntry sym x -> TypeRepr x
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
forall (x :: CrucibleType). RegEntry sym x -> TypeRepr x
C.regType (Assignment (RegEntry sym) args -> Assignment TypeRepr args)
-> Assignment (RegEntry sym) args -> Assignment TypeRepr args
forall a b. (a -> b) -> a -> b
$ RegMap sym args -> Assignment (RegEntry sym) args
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap (RegMap sym args -> Assignment (RegEntry sym) args)
-> RegMap sym args -> Assignment (RegEntry sym) args
forall a b. (a -> b) -> a -> b
$ SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (RegMap sym args)
-> RegMap sym args
forall s a. s -> Getting a s a -> a
^. ((CallFrame sym ext blocks r args
 -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame ((CallFrame sym ext blocks r args
  -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      (RegMap sym args)
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> CallFrame sym ext blocks r args
    -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (RegMap sym args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> CallFrame sym ext blocks r args
-> Const (RegMap sym args) (CallFrame sym ext blocks r args)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
C.frameRegs)) -> do


        ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint: RunningState: ComputeFixpoint: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BlockID blocks args -> String
forall a. Show a => a -> String
show BlockID blocks args
block_id
        (CrucibleAssumptions (SymExpr sym),
 Maybe
   (Goals
      (CrucibleAssumptions (SymExpr sym))
      (LabeledPred (Pred sym) SimError)))
_ <- bak
-> FrameIdentifier
-> IO
     (CrucibleAssumptions (SymExpr sym),
      Maybe
        (Goals
           (CrucibleAssumptions (SymExpr sym))
           (LabeledPred (Pred sym) SimError)))
forall sym bak.
IsSymBackend sym bak =>
bak
-> FrameIdentifier -> IO (Assumptions sym, ProofObligations sym)
C.popAssumptionFrameAndObligations bak
bak (FrameIdentifier
 -> IO
      (CrucibleAssumptions (SymExpr sym),
       Maybe
         (Goals
            (CrucibleAssumptions (SymExpr sym))
            (LabeledPred (Pred sym) SimError))))
-> FrameIdentifier
-> IO
     (CrucibleAssumptions (SymExpr sym),
      Maybe
        (Goals
           (CrucibleAssumptions (SymExpr sym))
           (LabeledPred (Pred sym) SimError)))
forall a b. (a -> b) -> a -> b
$ FixpointRecord sym blocks -> FrameIdentifier
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> FrameIdentifier
fixpointAssumptionFrameIdentifier FixpointRecord sym blocks
fixpoint_record

        -- widen the inductive condition
        (Assignment (RegEntry sym) args
join_reg_map, MapF (SymExpr sym) (FixpointEntry sym)
join_substitution) <- StateT
  (MapF (SymExpr sym) (FixpointEntry sym))
  IO
  (Assignment (RegEntry sym) args)
-> MapF (SymExpr sym) (FixpointEntry sym)
-> IO
     (Assignment (RegEntry sym) args,
      MapF (SymExpr sym) (FixpointEntry sym))
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT
          (sym
-> Assignment (RegEntry sym) args
-> Assignment (RegEntry sym) args
-> StateT
     (MapF (SymExpr sym) (FixpointEntry sym))
     IO
     (Assignment (RegEntry sym) args)
forall sym (ctx :: Ctx CrucibleType).
(?logMessage::String -> IO (), IsSymInterface sym) =>
sym
-> Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx
-> FixpointMonad sym (Assignment (RegEntry sym) ctx)
joinRegEntries sym
sym
            (RegMap sym args -> Assignment (RegEntry sym) args
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap RegMap sym args
reg_map)
            (RegMap sym args -> Assignment (RegEntry sym) args
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap (RegMap sym args -> Assignment (RegEntry sym) args)
-> RegMap sym args -> Assignment (RegEntry sym) args
forall a b. (a -> b) -> a -> b
$ SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (RegMap sym args)
-> RegMap sym args
forall s a. s -> Getting a s a -> a
^. ((CallFrame sym ext blocks r args
 -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame ((CallFrame sym ext blocks r args
  -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      (RegMap sym args)
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> CallFrame sym ext blocks r args
    -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (RegMap sym args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> CallFrame sym ext blocks r args
-> Const (RegMap sym args) (CallFrame sym ext blocks r args)
(RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> CallFrame sym ext blocks r args
-> Const (RegMap sym args) (CallFrame sym ext blocks r args)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
C.frameRegs))) (MapF (SymExpr sym) (FixpointEntry sym)
 -> IO
      (Assignment (RegEntry sym) args,
       MapF (SymExpr sym) (FixpointEntry sym)))
-> MapF (SymExpr sym) (FixpointEntry sym)
-> IO
     (Assignment (RegEntry sym) args,
      MapF (SymExpr sym) (FixpointEntry sym))
forall a b. (a -> b) -> a -> b
$
          FixpointRecord sym blocks -> MapF (SymExpr sym) (FixpointEntry sym)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> MapF (SymExpr sym) (FixpointEntry sym)
fixpointSubstitution FixpointRecord sym blocks
fixpoint_record

        let body_mem_impl :: MemImpl sym
body_mem_impl = Maybe (MemImpl sym) -> MemImpl sym
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (MemImpl sym) -> MemImpl sym)
-> Maybe (MemImpl sym) -> MemImpl sym
forall a b. (a -> b) -> a -> b
$ GlobalVar Mem -> SymGlobalState sym -> Maybe (RegValue sym Mem)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
C.lookupGlobal GlobalVar Mem
mem_var (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^. Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
  (SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals)
        let (MemImpl sym
header_mem_impl, MemAllocs sym
mem_allocs, MemWrites sym
mem_writes) = MemImpl sym -> (MemImpl sym, MemAllocs sym, MemWrites sym)
forall sym.
IsSymInterface sym =>
MemImpl sym -> (MemImpl sym, MemAllocs sym, MemWrites sym)
dropMemStackFrame MemImpl sym
body_mem_impl
        Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (MemAllocs sym -> Int
forall sym. MemAllocs sym -> Int
C.sizeMemAllocs MemAllocs sym
mem_allocs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
          String -> IO ()
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"SimpleLoopFixpoint: unsupported memory allocation in loop body."

        -- widen the memory
        Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
mem_substitution_candidate <- [((Natural, Natural, Natural),
  (MemFixpointEntry sym, StorageType))]
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((Natural, Natural, Natural),
   (MemFixpointEntry sym, StorageType))]
 -> Map
      (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType))
-> ([Maybe
       ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))]
    -> [((Natural, Natural, Natural),
         (MemFixpointEntry sym, StorageType))])
-> [Maybe
      ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))]
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe
   ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))]
-> [((Natural, Natural, Natural),
     (MemFixpointEntry sym, StorageType))]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe
    ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))]
 -> Map
      (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType))
-> IO
     [Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))]
-> IO
     (Map
        (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> case MemWrites sym
mem_writes of
          C.MemWrites [C.MemWritesChunkIndexed IntMap [MemWrite sym]
mmm] -> (MemWrite sym
 -> IO
      (Maybe
         ((Natural, Natural, Natural),
          (MemFixpointEntry sym, StorageType))))
-> [MemWrite sym]
-> IO
     [Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM
            (\case
              (C.MemWrite LLVMPtr sym w
ptr (C.MemStore LLVMVal sym
_ StorageType
storeage_type Alignment
_))
                | Just Natural
blk <- SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
W4.asNat (LLVMPtr sym w -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
C.llvmPointerBlock LLVMPtr sym w
ptr)
                , Just Natural
off <- BV w -> Natural
forall (w :: Natural). BV w -> Natural
BV.asNatural (BV w -> Natural) -> Maybe (BV w) -> Maybe Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W4.asBV (LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset LLVMPtr sym w
ptr) -> do
                  let sz :: Addr
sz = Addr -> StorageType -> Addr
C.typeEnd Addr
0 StorageType
storeage_type
                  MemFixpointEntry sym
some_join_varaible <- IO (MemFixpointEntry sym) -> IO (MemFixpointEntry sym)
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MemFixpointEntry sym) -> IO (MemFixpointEntry sym))
-> IO (MemFixpointEntry sym) -> IO (MemFixpointEntry sym)
forall a b. (a -> b) -> a -> b
$ case Natural -> Some NatRepr
W4.mkNatRepr (Natural -> Some NatRepr) -> Natural -> Some NatRepr
forall a b. (a -> b) -> a -> b
$ Addr -> Natural
C.bytesToBits Addr
sz of
                    C.Some NatRepr x
bv_width
                      | Just LeqProof 1 x
C.LeqProof <- NatRepr 1 -> NatRepr x -> Maybe (LeqProof 1 x)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
W4.testLeq (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @1) NatRepr x
bv_width -> do
                        SymExpr sym ('BaseBVType x)
join_varaible <- sym
-> SolverSymbol
-> BaseTypeRepr ('BaseBVType x)
-> IO (SymExpr sym ('BaseBVType x))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
W4.freshConstant sym
sym
                          (String -> SolverSymbol
userSymbol' String
"mem_join_var")
                          (NatRepr x -> BaseTypeRepr ('BaseBVType x)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr NatRepr x
bv_width)
                        MemFixpointEntry sym -> IO (MemFixpointEntry sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemFixpointEntry sym -> IO (MemFixpointEntry sym))
-> MemFixpointEntry sym -> IO (MemFixpointEntry sym)
forall a b. (a -> b) -> a -> b
$ MemFixpointEntry
                          { memFixpointEntrySym :: sym
memFixpointEntrySym = sym
sym
                          , memFixpointEntryJoinVariable :: SymExpr sym ('BaseBVType x)
memFixpointEntryJoinVariable = SymExpr sym ('BaseBVType x)
join_varaible
                          }
                      | Bool
otherwise ->
                        String -> [String] -> IO (MemFixpointEntry sym)
forall a. HasCallStack => String -> [String] -> a
C.panic
                          String
"SimpleLoopFixpoint.simpleLoopFixpoint"
                          [String
"unexpected storage type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ StorageType -> String
forall a. Show a => a -> String
show StorageType
storeage_type String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" of size " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Addr -> String
forall a. Show a => a -> String
show Addr
sz]
                  Maybe
  ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))
-> IO
     (Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType)))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe
   ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))
 -> IO
      (Maybe
         ((Natural, Natural, Natural),
          (MemFixpointEntry sym, StorageType))))
-> Maybe
     ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))
-> IO
     (Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType)))
forall a b. (a -> b) -> a -> b
$ ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))
-> Maybe
     ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))
forall a. a -> Maybe a
Just ((Natural
blk, Natural
off, Addr -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Addr
sz), (MemFixpointEntry sym
some_join_varaible, StorageType
storeage_type))
                | Just Natural
blk <- SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
W4.asNat (LLVMPtr sym w -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
C.llvmPointerBlock LLVMPtr sym w
ptr)
                , Just 64 :~: w
Refl <- NatRepr 64 -> NatRepr w -> Maybe (64 :~: w)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality ?ptrWidth::NatRepr 64
NatRepr 64
?ptrWidth (LLVMPtr sym w -> NatRepr w
forall sym (w :: Natural).
IsExprBuilder sym =>
LLVMPtr sym w -> NatRepr w
C.ptrWidth LLVMPtr sym w
ptr) -> do
                  Maybe
  (Map
     Natural
     [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))])
maybe_ranges <- MaybeT
  IO
  (Map
     Natural
     [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))])
-> IO
     (Maybe
        (Map
           Natural
           [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))]))
forall (m :: Type -> Type) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT
   IO
   (Map
      Natural
      [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))])
 -> IO
      (Maybe
         (Map
            Natural
            [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))])))
-> MaybeT
     IO
     (Map
        Natural
        [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))])
-> IO
     (Maybe
        (Map
           Natural
           [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))]))
forall a b. (a -> b) -> a -> b
$
                    forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> Mem sym -> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
C.writeRangesMem @_ @64 sym
sym (Mem sym
 -> MaybeT
      IO
      (Map
         Natural
         [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))]))
-> Mem sym
-> MaybeT
     IO
     (Map
        Natural
        [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))])
forall a b. (a -> b) -> a -> b
$ MemImpl sym -> Mem sym
forall sym. MemImpl sym -> Mem sym
C.memImplHeap MemImpl sym
header_mem_impl
                  case Maybe
  (Map
     Natural
     [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))])
maybe_ranges of
                    Just Map
  Natural
  [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))]
ranges -> do
                      SymExpr sym (BaseBVType 64)
sz <- sym -> NatRepr 64 -> BV 64 -> IO (SymExpr sym (BaseBVType 64))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym ?ptrWidth::NatRepr 64
NatRepr 64
?ptrWidth (BV 64 -> IO (SymExpr sym (BaseBVType 64)))
-> BV 64 -> IO (SymExpr sym (BaseBVType 64))
forall a b. (a -> b) -> a -> b
$ NatRepr 64 -> Integer -> BV 64
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr 64
NatRepr 64
?ptrWidth (Integer -> BV 64) -> Integer -> BV 64
forall a b. (a -> b) -> a -> b
$ Addr -> Integer
forall a. Integral a => a -> Integer
toInteger (Addr -> Integer) -> Addr -> Integer
forall a b. (a -> b) -> a -> b
$ Addr -> StorageType -> Addr
C.typeEnd Addr
0 StorageType
storeage_type
                      [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))]
-> ((SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))
    -> IO ())
-> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))]
-> Natural
-> Map
     Natural
     [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))]
-> [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Natural
blk Map
  Natural
  [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))]
ranges) (((SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))
  -> IO ())
 -> IO ())
-> ((SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))
    -> IO ())
-> IO ()
forall a b. (a -> b) -> a -> b
$ \(SymExpr sym (BaseBVType 64)
prev_off, SymExpr sym (BaseBVType 64)
prev_sz) -> do
                        Pred sym
disjoint_pred <- sym
-> LLVMPtr sym 64
-> SymExpr sym (BaseBVType 64)
-> LLVMPtr sym 64
-> SymExpr sym (BaseBVType 64)
-> IO (Pred sym)
forall (wptr :: Natural) sym.
(HasPtrWidth wptr, IsSymInterface sym) =>
sym
-> LLVMPtr sym wptr
-> SymBV sym wptr
-> LLVMPtr sym wptr
-> SymBV sym wptr
-> IO (Pred sym)
C.buildDisjointRegionsAssertionWithSub
                          sym
sym
                          LLVMPtr sym w
LLVMPtr sym 64
ptr
                          SymExpr sym (BaseBVType 64)
sz
                          (SymNat sym -> SymExpr sym (BaseBVType 64) -> LLVMPointer sym 64
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
C.LLVMPointer (LLVMPtr sym 64 -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
C.llvmPointerBlock LLVMPtr sym w
LLVMPtr sym 64
ptr) SymExpr sym (BaseBVType 64)
prev_off)
                          SymExpr sym (BaseBVType 64)
prev_sz
                        Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred Pred sym
disjoint_pred Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
                          String -> IO ()
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
                            String
"SimpleLoopFixpoint: non-disjoint ranges: off1="
                            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseBVType 64) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr (LLVMPtr sym 64 -> SymExpr sym (BaseBVType 64)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset LLVMPtr sym w
LLVMPtr sym 64
ptr))
                            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", sz1="
                            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseBVType 64) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr SymExpr sym (BaseBVType 64)
sz)
                            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", off2="
                            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseBVType 64) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr SymExpr sym (BaseBVType 64)
prev_off)
                            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", sz2="
                            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseBVType 64) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr SymExpr sym (BaseBVType 64)
prev_sz)
                      Maybe
  ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))
-> IO
     (Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType)))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe
  ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))
forall a. Maybe a
Nothing
                    Maybe
  (Map
     Natural
     [(SymExpr sym (BaseBVType 64), SymExpr sym (BaseBVType 64))])
Nothing -> String
-> IO
     (Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType)))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
 -> IO
      (Maybe
         ((Natural, Natural, Natural),
          (MemFixpointEntry sym, StorageType))))
-> String
-> IO
     (Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType)))
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint: unsupported symbolic pointers"
              MemWrite sym
_ -> String
-> IO
     (Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType)))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
 -> IO
      (Maybe
         ((Natural, Natural, Natural),
          (MemFixpointEntry sym, StorageType))))
-> String
-> IO
     (Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType)))
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint: not MemWrite: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (MemWrites sym -> Doc Any
forall sym ann. IsExpr (SymExpr sym) => MemWrites sym -> Doc ann
C.ppMemWrites MemWrites sym
mem_writes))
            ([[MemWrite sym]] -> [MemWrite sym]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
List.concat ([[MemWrite sym]] -> [MemWrite sym])
-> [[MemWrite sym]] -> [MemWrite sym]
forall a b. (a -> b) -> a -> b
$ IntMap [MemWrite sym] -> [[MemWrite sym]]
forall a. IntMap a -> [a]
IntMap.elems IntMap [MemWrite sym]
mmm)
          MemWrites sym
_ -> String
-> IO
     [Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))]
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
 -> IO
      [Maybe
         ((Natural, Natural, Natural),
          (MemFixpointEntry sym, StorageType))])
-> String
-> IO
     [Maybe
        ((Natural, Natural, Natural), (MemFixpointEntry sym, StorageType))]
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopFixpoint: not MemWritesChunkIndexed: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (MemWrites sym -> Doc Any
forall sym ann. IsExpr (SymExpr sym) => MemWrites sym -> Doc ann
C.ppMemWrites MemWrites sym
mem_writes)

        -- check that the mem substitution always computes the same footprint on every iteration (!?!)
        Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
mem_substitution <- if Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> Bool
forall k a. Map k a -> Bool
Map.null (FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution FixpointRecord sym blocks
fixpoint_record)
          then Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO
     (Map
        (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
mem_substitution_candidate
          else if Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> [(Natural, Natural, Natural)]
forall k a. Map k a -> [k]
Map.keys Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
mem_substitution_candidate [(Natural, Natural, Natural)]
-> [(Natural, Natural, Natural)] -> Bool
forall a. Eq a => a -> a -> Bool
== Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> [(Natural, Natural, Natural)]
forall k a. Map k a -> [k]
Map.keys (FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution FixpointRecord sym blocks
fixpoint_record)
            then Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO
     (Map
        (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Map
   (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
 -> IO
      (Map
         (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)))
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO
     (Map
        (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType))
forall a b. (a -> b) -> a -> b
$ FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution FixpointRecord sym blocks
fixpoint_record
            else String
-> IO
     (Map
        (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"SimpleLoopFixpoint: unsupported memory writes change"

        FrameIdentifier
assumption_frame_identifier <- bak -> IO FrameIdentifier
forall sym bak. IsSymBackend sym bak => bak -> IO FrameIdentifier
C.pushAssumptionFrame bak
bak

        -- check if we are done; if we did not introduce any new variables, we don't have to widen any more
        if MapF (SymExpr sym) (FixpointEntry sym) -> [Some (SymExpr sym)]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Some k2]
MapF.keys MapF (SymExpr sym) (FixpointEntry sym)
join_substitution [Some (SymExpr sym)] -> [Some (SymExpr sym)] -> Bool
forall a. Eq a => a -> a -> Bool
== MapF (SymExpr sym) (FixpointEntry sym) -> [Some (SymExpr sym)]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Some k2]
MapF.keys (FixpointRecord sym blocks -> MapF (SymExpr sym) (FixpointEntry sym)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> MapF (SymExpr sym) (FixpointEntry sym)
fixpointSubstitution FixpointRecord sym blocks
fixpoint_record)

          -- we found the fixpoint, get ready to wrap up
          then do
            ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
              String
"SimpleLoopFixpoint: RunningState: ComputeFixpoint -> CheckFixpoint"
            ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
              String
"SimpleLoopFixpoint: cond: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                  Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> (Pred sym -> Doc Any) -> Maybe (Pred sym) -> Doc Any
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc Any
"Nothing" Pred sym -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr (Maybe (Pred sym) -> Doc Any) -> Maybe (Pred sym) -> Doc Any
forall a b. (a -> b) -> a -> b
$ FixpointRecord sym blocks -> Maybe (Pred sym)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> Maybe (Pred sym)
fixpointLoopCondition FixpointRecord sym blocks
fixpoint_record)

            -- we have delayed populating the main substituation map with
            --  memory variables, so we have to do that now

            MapF (SymExpr sym) (SymExpr sym)
header_mem_substitution <- bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO (MapF (SymExpr sym) (SymExpr sym))
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO (MapF (SymExpr sym) (SymExpr sym))
loadMemJoinVariables bak
bak MemImpl sym
header_mem_impl (Map
   (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
 -> IO (MapF (SymExpr sym) (SymExpr sym)))
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO (MapF (SymExpr sym) (SymExpr sym))
forall a b. (a -> b) -> a -> b
$
              FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution FixpointRecord sym blocks
fixpoint_record
            MapF (SymExpr sym) (SymExpr sym)
body_mem_substitution <- bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO (MapF (SymExpr sym) (SymExpr sym))
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO (MapF (SymExpr sym) (SymExpr sym))
loadMemJoinVariables bak
bak MemImpl sym
body_mem_impl (Map
   (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
 -> IO (MapF (SymExpr sym) (SymExpr sym)))
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO (MapF (SymExpr sym) (SymExpr sym))
forall a b. (a -> b) -> a -> b
$
              FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution FixpointRecord sym blocks
fixpoint_record

            -- try to unify widening variables that have the same values
            let (MapF (SymExpr sym) (FixpointEntry sym)
normal_substitution, MapF (SymExpr sym) (SymExpr sym)
equality_substitution) = sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> (MapF (SymExpr sym) (FixpointEntry sym),
    MapF (SymExpr sym) (SymExpr sym))
forall sym.
IsSymInterface sym =>
sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> (MapF (SymExpr sym) (FixpointEntry sym),
    MapF (SymExpr sym) (SymExpr sym))
uninterpretedConstantEqualitySubstitution sym
sym (MapF (SymExpr sym) (FixpointEntry sym)
 -> (MapF (SymExpr sym) (FixpointEntry sym),
     MapF (SymExpr sym) (SymExpr sym)))
-> MapF (SymExpr sym) (FixpointEntry sym)
-> (MapF (SymExpr sym) (FixpointEntry sym),
    MapF (SymExpr sym) (SymExpr sym))
forall a b. (a -> b) -> a -> b
$
                  -- drop variables that don't appear along some back edge (? understand this better)
                  sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
forall sym.
IsSymInterface sym =>
sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
filterSubstitution sym
sym (MapF (SymExpr sym) (FixpointEntry sym)
 -> MapF (SymExpr sym) (FixpointEntry sym))
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
forall a b. (a -> b) -> a -> b
$
                  MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
MapF k a -> MapF k a -> MapF k a
MapF.union MapF (SymExpr sym) (FixpointEntry sym)
join_substitution (MapF (SymExpr sym) (FixpointEntry sym)
 -> MapF (SymExpr sym) (FixpointEntry sym))
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
forall a b. (a -> b) -> a -> b
$
                  -- this implements zip, because the two maps have the same keys
                  (forall (tp :: BaseType).
 SymExpr sym tp
 -> SymExpr sym tp
 -> SymExpr sym tp
 -> Maybe (FixpointEntry sym tp))
-> MapF (SymExpr sym) (SymExpr sym)
-> MapF (SymExpr sym) (SymExpr sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
forall {v} (k :: v -> Type) (a :: v -> Type) (b :: v -> Type)
       (c :: v -> Type).
OrdF k =>
(forall (tp :: v). k tp -> a tp -> b tp -> Maybe (c tp))
-> MapF k a -> MapF k b -> MapF k c
MapF.intersectWithKeyMaybe
                    (\SymExpr sym tp
_k SymExpr sym tp
x SymExpr sym tp
y -> FixpointEntry sym tp -> Maybe (FixpointEntry sym tp)
forall a. a -> Maybe a
Just (FixpointEntry sym tp -> Maybe (FixpointEntry sym tp))
-> FixpointEntry sym tp -> Maybe (FixpointEntry sym tp)
forall a b. (a -> b) -> a -> b
$ FixpointEntry{ headerValue :: SymExpr sym tp
headerValue = SymExpr sym tp
x, bodyValue :: SymExpr sym tp
bodyValue = SymExpr sym tp
y })
                    MapF (SymExpr sym) (SymExpr sym)
header_mem_substitution
                    MapF (SymExpr sym) (SymExpr sym)
body_mem_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 :: Assignment (RegEntry sym) args
res_reg_map = sym
-> MapF (SymExpr sym) (SymExpr sym)
-> Assignment (RegEntry sym) args
-> Assignment (RegEntry sym) args
forall sym (ctx :: Ctx CrucibleType).
IsSymInterface sym =>
sym
-> MapF (SymExpr sym) (SymExpr sym)
-> Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx
applySubstitutionRegEntries sym
sym MapF (SymExpr sym) (SymExpr sym)
equality_substitution Assignment (RegEntry sym) args
join_reg_map

            -- unify widening varialbes in the memory subst
            MemImpl sym
res_mem_impl <- bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
storeMemJoinVariables
              bak
bak
              (MemImpl sym
header_mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" (C.memImplHeap header_mem_impl) })
              Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
mem_substitution
              MapF (SymExpr sym) (SymExpr sym)
equality_substitution

            -- finally we can determine the loop bounds
            LoopIndexBound sym
loop_index_bound <- sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> Maybe (Pred sym)
-> IO (LoopIndexBound sym)
forall sym (wptr :: Natural).
(?logMessage::String -> IO (), IsSymInterface sym,
 HasPtrWidth wptr) =>
sym
-> MapF (SymExpr sym) (FixpointEntry sym)
-> Maybe (Pred sym)
-> IO (LoopIndexBound sym)
findLoopIndexBound sym
sym MapF (SymExpr sym) (FixpointEntry sym)
normal_substitution (Maybe (Pred sym) -> IO (LoopIndexBound sym))
-> Maybe (Pred sym) -> IO (LoopIndexBound sym)
forall a b. (a -> b) -> a -> b
$ FixpointRecord sym blocks -> Maybe (Pred sym)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> Maybe (Pred sym)
fixpointLoopCondition FixpointRecord sym blocks
fixpoint_record

            (()
_ :: ()) <- case LoopIndexBound sym
loop_index_bound of
              LoopIndexBound{ index :: ()
index = SymBV sym w
loop_index, stop :: ()
stop = SymBV sym w
loop_stop } -> do
                ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
W4.getCurrentProgramLoc sym
sym
                Pred sym
index_bound_condition <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsSymInterface sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
loopIndexBoundCondition sym
sym SymBV sym w
loop_index SymBV sym w
loop_stop
                bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
C.addAssumption bak
bak (Assumption sym -> IO ()) -> Assumption sym -> IO ()
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> String -> Pred sym -> Assumption sym
forall (e :: BaseType -> Type).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
C.GenericAssumption ProgramLoc
loc String
"" Pred sym
index_bound_condition
                Pred sym
index_start_step_condition <- sym -> LoopIndexBound sym -> IO (Pred sym)
forall sym.
IsSymInterface sym =>
sym -> LoopIndexBound sym -> IO (Pred sym)
loopIndexStartStepCondition sym
sym LoopIndexBound sym
loop_index_bound
                bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
C.addAssumption bak
bak (Assumption sym -> IO ()) -> Assumption sym -> IO ()
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> String -> Pred sym -> Assumption sym
forall (e :: BaseType -> Type).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
C.GenericAssumption ProgramLoc
loc String
"" Pred sym
index_start_step_condition

            IORef (FixpointState sym blocks)
-> FixpointState sym blocks -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (FixpointState sym blocks)
fixpoint_state_ref (FixpointState sym blocks -> IO ())
-> FixpointState sym blocks -> IO ()
forall a b. (a -> b) -> a -> b
$
              FixpointRecord sym blocks
-> LoopIndexBound sym -> FixpointState sym blocks
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks
-> LoopIndexBound sym -> FixpointState sym blocks
CheckFixpoint
                FixpointRecord
                { fixpointBlockId :: Some (BlockID blocks)
fixpointBlockId = BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
C.Some BlockID blocks args
block_id
                , fixpointAssumptionFrameIdentifier :: FrameIdentifier
fixpointAssumptionFrameIdentifier = FrameIdentifier
assumption_frame_identifier
                , fixpointSubstitution :: MapF (SymExpr sym) (FixpointEntry sym)
fixpointSubstitution = MapF (SymExpr sym) (FixpointEntry sym)
normal_substitution
                , fixpointRegMap :: RegMap sym args
fixpointRegMap = Assignment (RegEntry sym) args -> RegMap sym args
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
C.RegMap Assignment (RegEntry sym) args
res_reg_map
                , fixpointMemSubstitution :: Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution = Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
mem_substitution
                , fixpointLoopCondition :: Maybe (Pred sym)
fixpointLoopCondition = FixpointRecord sym blocks -> Maybe (Pred sym)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> Maybe (Pred sym)
fixpointLoopCondition FixpointRecord sym blocks
fixpoint_record
                }
                LoopIndexBound sym
loop_index_bound

            ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeatureResult p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureModifiedState (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp)
-> ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall a b. (a -> b) -> a -> b
$ RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType).
RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
C.RunningState (BlockID blocks args -> RunningStateInfo blocks args
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
BlockID blocks args -> RunningStateInfo blocks args
C.RunBlockStart BlockID blocks args
block_id) (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> ExecState p sym ext rtp)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall a b. (a -> b) -> a -> b
$
              SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall a b. a -> (a -> b) -> b
& ((CallFrame sym ext blocks r args
 -> Identity (CallFrame sym ext blocks r args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame ((CallFrame sym ext blocks r args
  -> Identity (CallFrame sym ext blocks r args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((RegMap sym args -> Identity (RegMap sym args))
    -> CallFrame sym ext blocks r args
    -> Identity (CallFrame sym ext blocks r args))
-> (RegMap sym args -> Identity (RegMap sym args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RegMap sym args -> Identity (RegMap sym args))
-> CallFrame sym ext blocks r args
-> Identity (CallFrame sym ext blocks r args)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
C.frameRegs) ((RegMap sym args -> Identity (RegMap sym args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> RegMap sym args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Assignment (RegEntry sym) args -> RegMap sym args
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
C.RegMap Assignment (RegEntry sym) args
Assignment (RegEntry sym) args
res_reg_map
                SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall a b. a -> (a -> b) -> b
& (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> (SymGlobalState sym -> SymGlobalState sym)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ GlobalVar Mem
-> RegValue sym Mem -> SymGlobalState sym -> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
C.insertGlobal GlobalVar Mem
mem_var RegValue sym Mem
MemImpl sym
res_mem_impl

          else do
            ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
              String
"SimpleLoopFixpoint: RunningState: ComputeFixpoint: -> ComputeFixpoint"

            -- write any new widening variables into memory state
            MemImpl sym
res_mem_impl <- bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
storeMemJoinVariables bak
bak
              (MemImpl sym
header_mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" (C.memImplHeap header_mem_impl) })
              Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
mem_substitution
              MapF (SymExpr sym) (SymExpr sym)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty

            IORef (FixpointState sym blocks)
-> FixpointState sym blocks -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (FixpointState sym blocks)
fixpoint_state_ref (FixpointState sym blocks -> IO ())
-> FixpointState sym blocks -> IO ()
forall a b. (a -> b) -> a -> b
$ FixpointRecord sym blocks -> FixpointState sym blocks
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> FixpointState sym blocks
ComputeFixpoint
              FixpointRecord
              { fixpointBlockId :: Some (BlockID blocks)
fixpointBlockId = BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
C.Some BlockID blocks args
block_id
              , fixpointAssumptionFrameIdentifier :: FrameIdentifier
fixpointAssumptionFrameIdentifier = FrameIdentifier
assumption_frame_identifier
              , fixpointSubstitution :: MapF (SymExpr sym) (FixpointEntry sym)
fixpointSubstitution = MapF (SymExpr sym) (FixpointEntry sym)
join_substitution
              , fixpointRegMap :: RegMap sym args
fixpointRegMap = Assignment (RegEntry sym) args -> RegMap sym args
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
C.RegMap Assignment (RegEntry sym) args
join_reg_map
              , fixpointMemSubstitution :: Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution = Map (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
mem_substitution
              , fixpointLoopCondition :: Maybe (Pred sym)
fixpointLoopCondition = Maybe (Pred sym)
forall a. Maybe a
Nothing
              }
            ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeatureResult p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureModifiedState (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp)
-> ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall a b. (a -> b) -> a -> b
$ RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType).
RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
C.RunningState (BlockID blocks args -> RunningStateInfo blocks args
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
BlockID blocks args -> RunningStateInfo blocks args
C.RunBlockStart BlockID blocks args
block_id) (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> ExecState p sym ext rtp)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall a b. (a -> b) -> a -> b
$
              SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall a b. a -> (a -> b) -> b
& ((CallFrame sym ext blocks r args
 -> Identity (CallFrame sym ext blocks r args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame ((CallFrame sym ext blocks r args
  -> Identity (CallFrame sym ext blocks r args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((RegMap sym args -> Identity (RegMap sym args))
    -> CallFrame sym ext blocks r args
    -> Identity (CallFrame sym ext blocks r args))
-> (RegMap sym args -> Identity (RegMap sym args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RegMap sym args -> Identity (RegMap sym args))
-> CallFrame sym ext blocks r args
-> Identity (CallFrame sym ext blocks r args)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
C.frameRegs) ((RegMap sym args -> Identity (RegMap sym args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> RegMap sym args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Assignment (RegEntry sym) args -> RegMap sym args
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
C.RegMap Assignment (RegEntry sym) args
Assignment (RegEntry sym) args
join_reg_map
                SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall a b. a -> (a -> b) -> b
& (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> (SymGlobalState sym -> SymGlobalState sym)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ GlobalVar Mem
-> RegValue sym Mem -> SymGlobalState sym -> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
C.insertGlobal GlobalVar Mem
mem_var RegValue sym Mem
MemImpl sym
res_mem_impl

      | Bool
otherwise -> String -> [String] -> IO (ExecutionFeatureResult p sym ext rtp)
forall a. HasCallStack => String -> [String] -> a
C.panic String
"SimpleLoopFixpoint.simpleLoopFixpoint" [String
"type mismatch: ComputeFixpoint"]

    CheckFixpoint FixpointRecord sym blocks
fixpoint_record LoopIndexBound sym
loop_bound
      | FixpointRecord { fixpointRegMap :: ()
fixpointRegMap = RegMap sym args
reg_map } <- FixpointRecord sym blocks
fixpoint_record
      , Just args :~: args
Refl <- Assignment TypeRepr args
-> Assignment TypeRepr args -> Maybe (args :~: args)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
Assignment TypeRepr a -> Assignment TypeRepr b -> Maybe (a :~: b)
W4.testEquality
          ((forall (x :: CrucibleType). RegEntry sym x -> TypeRepr x)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> Assignment TypeRepr x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC RegEntry sym x -> TypeRepr x
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
forall (x :: CrucibleType). RegEntry sym x -> TypeRepr x
C.regType (Assignment (RegEntry sym) args -> Assignment TypeRepr args)
-> Assignment (RegEntry sym) args -> Assignment TypeRepr args
forall a b. (a -> b) -> a -> b
$ RegMap sym args -> Assignment (RegEntry sym) args
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap RegMap sym args
reg_map)
          ((forall (x :: CrucibleType). RegEntry sym x -> TypeRepr x)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> Assignment TypeRepr x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC RegEntry sym x -> TypeRepr x
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
forall (x :: CrucibleType). RegEntry sym x -> TypeRepr x
C.regType (Assignment (RegEntry sym) args -> Assignment TypeRepr args)
-> Assignment (RegEntry sym) args -> Assignment TypeRepr args
forall a b. (a -> b) -> a -> b
$ RegMap sym args -> Assignment (RegEntry sym) args
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap (RegMap sym args -> Assignment (RegEntry sym) args)
-> RegMap sym args -> Assignment (RegEntry sym) args
forall a b. (a -> b) -> a -> b
$ SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (RegMap sym args)
-> RegMap sym args
forall s a. s -> Getting a s a -> a
^. ((CallFrame sym ext blocks r args
 -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame ((CallFrame sym ext blocks r args
  -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      (RegMap sym args)
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> CallFrame sym ext blocks r args
    -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (RegMap sym args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> CallFrame sym ext blocks r args
-> Const (RegMap sym args) (CallFrame sym ext blocks r args)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
C.frameRegs)) -> do
        ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
          String
"SimpleLoopFixpoint: RunningState: "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"CheckFixpoint"
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -> "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"AfterFixpoint"
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ BlockID blocks args -> String
forall a. Show a => a -> String
show BlockID blocks args
block_id

        ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
W4.getCurrentProgramLoc sym
sym

        -- assert that the hypothesis we made about the loop termination condition is true
        (()
_ :: ()) <- case LoopIndexBound sym
loop_bound of
          LoopIndexBound{ index :: ()
index = SymBV sym w
loop_index, stop :: ()
stop = SymBV sym w
loop_stop } -> do
            -- check the loop index bound condition
            Pred sym
index_bound_condition <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsSymInterface sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
loopIndexBoundCondition
              sym
sym
              (FixpointEntry sym (BaseBVType w) -> SymBV sym w
forall sym (tp :: BaseType). FixpointEntry sym tp -> SymExpr sym tp
bodyValue (FixpointEntry sym (BaseBVType w) -> SymBV sym w)
-> FixpointEntry sym (BaseBVType w) -> SymBV sym w
forall a b. (a -> b) -> a -> b
$ Maybe (FixpointEntry sym (BaseBVType w))
-> FixpointEntry sym (BaseBVType w)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (FixpointEntry sym (BaseBVType w))
 -> FixpointEntry sym (BaseBVType w))
-> Maybe (FixpointEntry sym (BaseBVType w))
-> FixpointEntry sym (BaseBVType w)
forall a b. (a -> b) -> a -> b
$ SymBV sym w
-> MapF (SymExpr sym) (FixpointEntry sym)
-> Maybe (FixpointEntry sym (BaseBVType w))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup SymBV sym w
loop_index (MapF (SymExpr sym) (FixpointEntry sym)
 -> Maybe (FixpointEntry sym (BaseBVType w)))
-> MapF (SymExpr sym) (FixpointEntry sym)
-> Maybe (FixpointEntry sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ FixpointRecord sym blocks -> MapF (SymExpr sym) (FixpointEntry sym)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> MapF (SymExpr sym) (FixpointEntry sym)
fixpointSubstitution FixpointRecord sym blocks
fixpoint_record)
              SymBV sym w
loop_stop
            bak -> LabeledPred (Pred sym) SimError -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
C.addProofObligation bak
bak (LabeledPred (Pred sym) SimError -> IO ())
-> LabeledPred (Pred sym) SimError -> IO ()
forall a b. (a -> b) -> a -> b
$ Pred sym -> SimError -> LabeledPred (Pred sym) SimError
forall pred msg. pred -> msg -> LabeledPred pred msg
C.LabeledPred Pred sym
index_bound_condition (SimError -> LabeledPred (Pred sym) SimError)
-> SimError -> LabeledPred (Pred sym) SimError
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> SimErrorReason -> SimError
C.SimError ProgramLoc
loc SimErrorReason
""

        CrucibleAssumptions (SymExpr sym)
_ <- bak -> FrameIdentifier -> IO (CrucibleAssumptions (SymExpr sym))
forall sym bak.
IsSymBackend sym bak =>
bak -> FrameIdentifier -> IO (Assumptions sym)
C.popAssumptionFrame bak
bak (FrameIdentifier -> IO (CrucibleAssumptions (SymExpr sym)))
-> FrameIdentifier -> IO (CrucibleAssumptions (SymExpr sym))
forall a b. (a -> b) -> a -> b
$ FixpointRecord sym blocks -> FrameIdentifier
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> FrameIdentifier
fixpointAssumptionFrameIdentifier FixpointRecord sym blocks
fixpoint_record

        let body_mem_impl :: MemImpl sym
body_mem_impl = Maybe (MemImpl sym) -> MemImpl sym
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (MemImpl sym) -> MemImpl sym)
-> Maybe (MemImpl sym) -> MemImpl sym
forall a b. (a -> b) -> a -> b
$ GlobalVar Mem -> SymGlobalState sym -> Maybe (RegValue sym Mem)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
C.lookupGlobal GlobalVar Mem
mem_var (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^. Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
  (SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals)
        let (MemImpl sym
header_mem_impl, MemAllocs sym
_mem_allocs, MemWrites sym
_mem_writes) = MemImpl sym -> (MemImpl sym, MemAllocs sym, MemWrites sym)
forall sym.
IsSymInterface sym =>
MemImpl sym -> (MemImpl sym, MemAllocs sym, MemWrites sym)
dropMemStackFrame MemImpl sym
body_mem_impl

        MapF (SymExpr sym) (SymExpr sym)
body_mem_substitution <- bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO (MapF (SymExpr sym) (SymExpr sym))
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO (MapF (SymExpr sym) (SymExpr sym))
loadMemJoinVariables bak
bak MemImpl sym
body_mem_impl (Map
   (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
 -> IO (MapF (SymExpr sym) (SymExpr sym)))
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> IO (MapF (SymExpr sym) (SymExpr sym))
forall a b. (a -> b) -> a -> b
$ FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution FixpointRecord sym blocks
fixpoint_record
        let res_substitution :: MapF (SymExpr sym) (FixpointEntry sym)
res_substitution = (forall (tp :: BaseType).
 SymExpr sym tp -> FixpointEntry sym tp -> FixpointEntry sym tp)
-> MapF (SymExpr sym) (FixpointEntry sym)
-> MapF (SymExpr sym) (FixpointEntry sym)
forall {v} (ktp :: v -> Type) (f :: v -> Type) (g :: v -> Type).
(forall (tp :: v). ktp tp -> f tp -> g tp)
-> MapF ktp f -> MapF ktp g
MapF.mapWithKey
              (\SymExpr sym tp
variable FixpointEntry sym tp
fixpoint_entry ->
                FixpointEntry sym tp
fixpoint_entry
                  { bodyValue = MapF.findWithDefault (bodyValue fixpoint_entry) variable body_mem_substitution
                  })
              (FixpointRecord sym blocks -> MapF (SymExpr sym) (FixpointEntry sym)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> MapF (SymExpr sym) (FixpointEntry sym)
fixpointSubstitution FixpointRecord sym blocks
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
        (MapF (SymExpr sym) (SymExpr sym)
fixpoint_func_substitution, Pred sym
fixpoint_func_condition) <- IO (MapF (SymExpr sym) (SymExpr sym), Pred sym)
-> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym)
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MapF (SymExpr sym) (SymExpr sym), Pred sym)
 -> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym))
-> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym)
-> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym)
forall a b. (a -> b) -> a -> b
$
          case FixpointRecord sym blocks -> Maybe (Pred sym)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks -> Maybe (Pred sym)
fixpointLoopCondition FixpointRecord sym blocks
fixpoint_record of
            Maybe (Pred sym)
Nothing -> String -> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"When checking the result of a fixpoint, no loop condition was found!"
            Just Pred sym
c  -> MapF (SymExpr sym) (FixpointEntry sym)
-> Pred sym -> IO (MapF (SymExpr sym) (SymExpr sym), Pred sym)
fixpoint_func MapF (SymExpr sym) (FixpointEntry sym)
res_substitution Pred sym
c

        bak -> LabeledPred (Pred sym) SimError -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
C.addProofObligation bak
bak (LabeledPred (Pred sym) SimError -> IO ())
-> LabeledPred (Pred sym) SimError -> IO ()
forall a b. (a -> b) -> a -> b
$ Pred sym -> SimError -> LabeledPred (Pred sym) SimError
forall pred msg. pred -> msg -> LabeledPred pred msg
C.LabeledPred Pred sym
fixpoint_func_condition (SimError -> LabeledPred (Pred sym) SimError)
-> SimError -> LabeledPred (Pred sym) SimError
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> SimErrorReason -> SimError
C.SimError ProgramLoc
loc SimErrorReason
""
        -- ?logMessage $ "fixpoint_func_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList fixpoint_func_substitution)

        let res_reg_map :: RegMap sym args
res_reg_map = Assignment (RegEntry sym) args -> RegMap sym args
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
C.RegMap (Assignment (RegEntry sym) args -> RegMap sym args)
-> Assignment (RegEntry sym) args -> RegMap sym args
forall a b. (a -> b) -> a -> b
$
              sym
-> MapF (SymExpr sym) (SymExpr sym)
-> Assignment (RegEntry sym) args
-> Assignment (RegEntry sym) args
forall sym (ctx :: Ctx CrucibleType).
IsSymInterface sym =>
sym
-> MapF (SymExpr sym) (SymExpr sym)
-> Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx
applySubstitutionRegEntries sym
sym MapF (SymExpr sym) (SymExpr sym)
fixpoint_func_substitution (RegMap sym args -> Assignment (RegEntry sym) args
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap RegMap sym args
reg_map)

        MemImpl sym
res_mem_impl <- bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
storeMemJoinVariables bak
bak
          MemImpl sym
header_mem_impl
          (FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks
-> Map
     (Natural, Natural, Natural) (MemFixpointEntry sym, StorageType)
fixpointMemSubstitution FixpointRecord sym blocks
fixpoint_record)
          MapF (SymExpr sym) (SymExpr sym)
fixpoint_func_substitution

        (()
_ :: ()) <- case LoopIndexBound sym
loop_bound of
          LoopIndexBound{ index :: ()
index = SymBV sym w
loop_index, stop :: ()
stop = SymBV sym w
loop_stop } -> do
            let loop_index' :: SymBV sym w
loop_index' = SymBV sym w
-> SymBV sym w -> MapF (SymExpr sym) (SymExpr sym) -> SymBV sym w
forall {v} (k :: v -> Type) (a :: v -> Type) (tp :: v).
OrdF k =>
a tp -> k tp -> MapF k a -> a tp
MapF.findWithDefault SymBV sym w
loop_index SymBV sym w
loop_index MapF (SymExpr sym) (SymExpr sym)
fixpoint_func_substitution
            Pred sym
index_bound_condition <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsSymInterface sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
loopIndexBoundCondition sym
sym SymBV sym w
loop_index' SymBV sym w
loop_stop
            bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
C.addAssumption bak
bak (Assumption sym -> IO ()) -> Assumption sym -> IO ()
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> String -> Pred sym -> Assumption sym
forall (e :: BaseType -> Type).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
C.GenericAssumption ProgramLoc
loc String
"" Pred sym
index_bound_condition
            Pred sym
index_start_step_condition <- sym -> LoopIndexBound sym -> IO (Pred sym)
forall sym.
IsSymInterface sym =>
sym -> LoopIndexBound sym -> IO (Pred sym)
loopIndexStartStepCondition sym
sym (LoopIndexBound sym -> IO (Pred sym))
-> LoopIndexBound sym -> IO (Pred sym)
forall a b. (a -> b) -> a -> b
$ LoopIndexBound
              { index :: SymBV sym w
index = SymBV sym w
loop_index'
              , start :: Natural
start = LoopIndexBound sym -> Natural
forall sym. LoopIndexBound sym -> Natural
start LoopIndexBound sym
loop_bound
              , stop :: SymBV sym w
stop = SymBV sym w
loop_stop
              , step :: Natural
step = LoopIndexBound sym -> Natural
forall sym. LoopIndexBound sym -> Natural
step LoopIndexBound sym
loop_bound
              }
            bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
C.addAssumption bak
bak (Assumption sym -> IO ()) -> Assumption sym -> IO ()
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> String -> Pred sym -> Assumption sym
forall (e :: BaseType -> Type).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
C.GenericAssumption ProgramLoc
loc String
"" Pred sym
index_start_step_condition

        IORef (FixpointState sym blocks)
-> FixpointState sym blocks -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (FixpointState sym blocks)
fixpoint_state_ref (FixpointState sym blocks -> IO ())
-> FixpointState sym blocks -> IO ()
forall a b. (a -> b) -> a -> b
$
          FixpointRecord sym blocks
-> LoopIndexBound sym -> FixpointState sym blocks
forall sym (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord sym blocks
-> LoopIndexBound sym -> FixpointState sym blocks
AfterFixpoint
            FixpointRecord sym blocks
fixpoint_record{ fixpointSubstitution = res_substitution }
            LoopIndexBound sym
loop_bound

        ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeatureResult p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureModifiedState (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp)
-> ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall a b. (a -> b) -> a -> b
$ RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType).
RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
C.RunningState (BlockID blocks args -> RunningStateInfo blocks args
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
BlockID blocks args -> RunningStateInfo blocks args
C.RunBlockStart BlockID blocks args
block_id) (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> ExecState p sym ext rtp)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall a b. (a -> b) -> a -> b
$
          SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall a b. a -> (a -> b) -> b
& ((CallFrame sym ext blocks r args
 -> Identity (CallFrame sym ext blocks r args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame ((CallFrame sym ext blocks r args
  -> Identity (CallFrame sym ext blocks r args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((RegMap sym args -> Identity (RegMap sym args))
    -> CallFrame sym ext blocks r args
    -> Identity (CallFrame sym ext blocks r args))
-> (RegMap sym args -> Identity (RegMap sym args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RegMap sym args -> Identity (RegMap sym args))
-> CallFrame sym ext blocks r args
-> Identity (CallFrame sym ext blocks r args)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
C.frameRegs) ((RegMap sym args -> Identity (RegMap sym args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> RegMap sym args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ RegMap sym args
RegMap sym args
res_reg_map
            SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall a b. a -> (a -> b) -> b
& (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> (SymGlobalState sym -> SymGlobalState sym)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ GlobalVar Mem
-> RegValue sym Mem -> SymGlobalState sym -> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
C.insertGlobal GlobalVar Mem
mem_var RegValue sym Mem
MemImpl sym
res_mem_impl

      | Bool
otherwise -> String -> [String] -> IO (ExecutionFeatureResult p sym ext rtp)
forall a. HasCallStack => String -> [String] -> a
C.panic String
"SimpleLoopFixpoint.simpleLoopFixpoint" [String
"type mismatch: CheckFixpoint"]

    AfterFixpoint{} -> String -> [String] -> IO (ExecutionFeatureResult p sym ext rtp)
forall a. HasCallStack => String -> [String] -> a
C.panic String
"SimpleLoopFixpoint.simpleLoopFixpoint" [String
"AfterFixpoint"]


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 :: forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> MaybePausedFrameTgtId f
pausedFrameTgtId C.PausedFrame{ resume :: forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> ControlResumption p sym ext rtp f
resume = ControlResumption p sym ext rtp f
resume } = case ControlResumption p sym ext rtp f
resume of
  C.ContinueResumption (C.ResolvedJump BlockID blocks args
tgt_id RegMap sym args
_) -> Some (BlockID blocks)
-> MaybePausedFrameTgtId (CrucibleLang blocks r)
forall (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Some (BlockID b) -> MaybePausedFrameTgtId (CrucibleLang b r)
JustPausedFrameTgtId (Some (BlockID blocks)
 -> MaybePausedFrameTgtId (CrucibleLang blocks r))
-> Some (BlockID blocks)
-> MaybePausedFrameTgtId (CrucibleLang blocks r)
forall a b. (a -> b) -> a -> b
$ BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
C.Some BlockID blocks args
tgt_id
  C.CheckMergeResumption (C.ResolvedJump BlockID blocks args
tgt_id RegMap sym args
_) -> Some (BlockID blocks)
-> MaybePausedFrameTgtId (CrucibleLang blocks r)
forall (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Some (BlockID b) -> MaybePausedFrameTgtId (CrucibleLang b r)
JustPausedFrameTgtId (Some (BlockID blocks)
 -> MaybePausedFrameTgtId (CrucibleLang blocks r))
-> Some (BlockID blocks)
-> MaybePausedFrameTgtId (CrucibleLang blocks r)
forall a b. (a -> b) -> a -> b
$ BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
C.Some BlockID blocks args
tgt_id
  ControlResumption p sym ext rtp f
_ -> MaybePausedFrameTgtId f
forall f. MaybePausedFrameTgtId f
NothingPausedFrameTgtId