------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.SimpleLoopInvariant
-- Description      : Execution feature to perform verification of simply
--                    structured loops via invariants.
-- Copyright        : (c) Galois, Inc 2022
-- License          : BSD3
-- Stability        : provisional
--
--
-- This module provides an execution feature that can be installed
-- into the Crucible simulator which facilitates reasoning about
-- certain kinds of loops by using loop invariants instead of
-- requiring that loops symbolically terminate. In order for this
-- feature to work, the loop in question needs to be
-- single-entry/single-exit, and needs to have a constant memory
-- footprint on each loop iteration (except that memory regions backed
-- by SMT arrays are treated as a whole, so loops can write into
-- different regions of an SMT-array memory region on different
-- iterations). In addition, loop-involved memory writes must be
-- sufficiently concrete that we can determine their region values,
-- and writes to the same region value must have concrete distances
-- from each other, so we can determine if/when they alias.
--
-- To set up a loop invariant for a loop, you must specify which CFG the
-- loop is in, indicate which loop (of potentially several) in the CFG
-- is the one of interest, and give a function that is used to construct
-- the statement of the loop invariant. When given a CFG, the execution
-- feature computes a weak topological ordering to find the loops in
-- the program; the number given by the user selects which of these to
-- install the invariant for.
--
-- At runtime, we will interrupt execution when the loop head is
-- reached; at this point we will record the values of the memory and
-- the incoming local variables. Then, we will begin a series of
-- "hypothetical" executions of the loop body and track how the memory
-- and local variables are modified by the loop body. On each
-- iteration where we find a difference, we replace the local or
-- memory region with a fresh "join variable" which represents the
-- unknown value of a loop-carried dependency. We continue this process
-- until we reach a fixpoint; then we will have captured all the locations
-- that are potentially of interest for the loop invariant.
--
-- Once we have found all the loop-carried dependencies, we assert
-- that the loop invariant holds on the initial values upon entry to the
-- loop. Then, we set up another execution starting from the loop head
-- where we first assume the loop invariant over the join variables
-- invented earlier, and begin execution again.  In this mode, when we
-- reach the loop head once more, we assert the loop invariant on the
-- computed values and abort execution along that path. Paths exiting
-- the loop continue as normal.
--
-- Provided the user suppiles an appropriate loop invarant function
-- and can discharge all the generated proof obligations, this procedure
-- should result in a sound proof of partial correctness for the function
-- in question.
--
-- This whole procedure has some relatively fragile elements that are
-- worth calling out.  First, specifying which loop you want to reason
-- about may require some trial-and-error, the WTO ordering might not
-- directly correspond to what is seen in the source code. The most
-- reliable way to select the right loop is to ensure there is only
-- one loop of interest in a given function, and use loop index 0.
-- The other fragility has to do with the discovery of loop-carried
-- dependencies. The number and order of values that are supplied to
-- the loop invariant depend on the internal details of the compiler
-- and simulator, so the user may have to spend some time and effort
-- to discover what the values appearing in the invariant correspond
-- to. This process may well be quite sensitive to changes in the
-- source code.
--
-- Limitiations: currently, this feature is restricted to 64-bit code.
------------------------------------------------------------------------

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


module Lang.Crucible.LLVM.SimpleLoopInvariant
  ( InvariantEntry(..)
  , InvariantPhase(..)
  , simpleLoopInvariant
  ) where

import           Control.Lens
import           Control.Monad (forM, unless, when)
import           Control.Monad.IO.Class (MonadIO(..))
import           Control.Monad.Except (ExceptT, MonadError(..), runExceptT)
import           Control.Monad.Reader (MonadReader(..), ReaderT, runReaderT)
import           Control.Monad.State (MonadState(..), StateT(..))
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           Prettyprinter (pretty)

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 What4.ProgramLoc 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.CFG.Extension 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


-- | A datatype describing the reason we are building an instance
--   of the loop invariant.
data InvariantPhase
  = InitialInvariant
  | HypotheticalInvariant
  | InductiveInvariant
 deriving (InvariantPhase -> InvariantPhase -> Bool
(InvariantPhase -> InvariantPhase -> Bool)
-> (InvariantPhase -> InvariantPhase -> Bool) -> Eq InvariantPhase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InvariantPhase -> InvariantPhase -> Bool
== :: InvariantPhase -> InvariantPhase -> Bool
$c/= :: InvariantPhase -> InvariantPhase -> Bool
/= :: InvariantPhase -> InvariantPhase -> Bool
Eq, Eq InvariantPhase
Eq InvariantPhase =>
(InvariantPhase -> InvariantPhase -> Ordering)
-> (InvariantPhase -> InvariantPhase -> Bool)
-> (InvariantPhase -> InvariantPhase -> Bool)
-> (InvariantPhase -> InvariantPhase -> Bool)
-> (InvariantPhase -> InvariantPhase -> Bool)
-> (InvariantPhase -> InvariantPhase -> InvariantPhase)
-> (InvariantPhase -> InvariantPhase -> InvariantPhase)
-> Ord InvariantPhase
InvariantPhase -> InvariantPhase -> Bool
InvariantPhase -> InvariantPhase -> Ordering
InvariantPhase -> InvariantPhase -> InvariantPhase
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: InvariantPhase -> InvariantPhase -> Ordering
compare :: InvariantPhase -> InvariantPhase -> Ordering
$c< :: InvariantPhase -> InvariantPhase -> Bool
< :: InvariantPhase -> InvariantPhase -> Bool
$c<= :: InvariantPhase -> InvariantPhase -> Bool
<= :: InvariantPhase -> InvariantPhase -> Bool
$c> :: InvariantPhase -> InvariantPhase -> Bool
> :: InvariantPhase -> InvariantPhase -> Bool
$c>= :: InvariantPhase -> InvariantPhase -> Bool
>= :: InvariantPhase -> InvariantPhase -> Bool
$cmax :: InvariantPhase -> InvariantPhase -> InvariantPhase
max :: InvariantPhase -> InvariantPhase -> InvariantPhase
$cmin :: InvariantPhase -> InvariantPhase -> InvariantPhase
min :: InvariantPhase -> InvariantPhase -> InvariantPhase
Ord, Int -> InvariantPhase -> ShowS
[InvariantPhase] -> ShowS
InvariantPhase -> String
(Int -> InvariantPhase -> ShowS)
-> (InvariantPhase -> String)
-> ([InvariantPhase] -> ShowS)
-> Show InvariantPhase
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InvariantPhase -> ShowS
showsPrec :: Int -> InvariantPhase -> ShowS
$cshow :: InvariantPhase -> String
show :: InvariantPhase -> String
$cshowList :: [InvariantPhase] -> ShowS
showList :: [InvariantPhase] -> ShowS
Show)

-- | 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
--   any more fresh widening variables, and the body values for each
--   variable are stable across iterations.
data InvariantEntry sym tp =
  InvariantEntry
  { forall sym (tp :: BaseType).
InvariantEntry sym tp -> SymExpr sym tp
headerValue :: W4.SymExpr sym tp
  , forall sym (tp :: BaseType).
InvariantEntry sym tp -> SymExpr sym tp
bodyValue :: W4.SymExpr sym tp
  }

instance OrdF (W4.SymExpr sym) => OrdF (InvariantEntry sym) where
  compareF :: forall (x :: BaseType) (y :: BaseType).
InvariantEntry sym x -> InvariantEntry sym y -> OrderingF x y
compareF InvariantEntry sym x
x InvariantEntry 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 (InvariantEntry sym x -> SymExpr sym x
forall sym (tp :: BaseType).
InvariantEntry sym tp -> SymExpr sym tp
headerValue InvariantEntry sym x
x) (InvariantEntry sym y -> SymExpr sym y
forall sym (tp :: BaseType).
InvariantEntry sym tp -> SymExpr sym tp
headerValue InvariantEntry 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 (InvariantEntry sym x -> SymExpr sym x
forall sym (tp :: BaseType).
InvariantEntry sym tp -> SymExpr sym tp
bodyValue InvariantEntry sym x
x) (InvariantEntry sym y -> SymExpr sym y
forall sym (tp :: BaseType).
InvariantEntry sym tp -> SymExpr sym tp
bodyValue InvariantEntry sym y
y)
    OrderingF x y
GTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

instance OrdF (InvariantEntry sym) => W4.TestEquality (InvariantEntry sym) where
  testEquality :: forall (a :: BaseType) (b :: BaseType).
InvariantEntry sym a -> InvariantEntry sym b -> Maybe (a :~: b)
testEquality InvariantEntry sym a
x InvariantEntry sym b
y = OrderingF a b -> Maybe (a :~: b)
forall {k} (x :: k) (y :: k). OrderingF x y -> Maybe (x :~: y)
orderingF_refl (InvariantEntry sym a -> InvariantEntry 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).
InvariantEntry sym x -> InvariantEntry sym y -> OrderingF x y
compareF InvariantEntry sym a
x InvariantEntry sym b
y)

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

    -- | We have found an inductively-strong representation of the live variables
    --   of the loop. We are now executing the from the loop head one final time
    --   to produce the proof obligations arising from the body of the loop,
    --   the main inductive loop invariant obligation, and any obligations arising
    --   from code following the loop exit.
    | CheckFixpoint (FixpointRecord p sym ext rtp blocks)


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

    -- | 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 p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> VariableSubst sym
fixpointSubstitution :: VariableSubst sym

    -- | The memory subsitution describes where the loop-carried dependencies live in the
    --   memory.
  , forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> MemorySubstitution sym
fixpointMemSubstitution :: MemorySubstitution sym

    -- | Prestate values of the Crucible registers when the loop header is first encountered.
  , ()
fixpointRegMap :: C.RegMap sym args

    -- | The sim state of the simulator when we first encounter the loop header.
  , ()
fixpointInitialSimState :: C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args)

    -- | External constants appearing in the expressions computed by the loop. These will be passed
    --   into the loop invariant as additional parameters.
  , forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> [Some (SymExpr sym)]
fixpointImplicitParams :: [Some (W4.SymExpr sym)]

    -- | A special memory region number that does not correspond to any valid block.
    --   This is intended to model values the block portion of bitvector values that
    --   get clobbered by the loop body, but do not represent loop-carried dependencies.
  , forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> SymNat sym
fixpointHavocBlock :: W4.SymNat sym
  }

-- | A variable substitution is used to track metadata regarding the discovered
--   loop-carried dependencies of a loop.
data VariableSubst sym =
  VarSubst
  { forall sym.
VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
varSubst :: MapF (W4.SymExpr sym) (InvariantEntry sym)
    -- ^ The @varSubst@ associates to each "join variable" an @InvariantEntry@,
    --   that descibes the initial value the variable had, and the value computed
    --   for it after a loop iteration.

  , forall sym. VariableSubst sym -> MapF (SymExpr sym) (Const ())
varHavoc :: MapF (W4.SymExpr sym) (Const ())
    -- ^ The @varHavoc@ map is essentially just a set of "join variables" for which
    --   we were not able to compute a coherent value across the loop boundary.
    --   Such variables are considered to be "junk" at the beginning of the loop,
    --   and do not participate in the loop invariant. This usually arises from
    --   temporary scratch space used in the loop body.
  }


-- | A memory region is used to describe a contiguous sequence of bytes
--   which is of known size, and which is at a known, concrete, offset
--   from a "master" offset. In a given regualar memory block, these
--   regions are required to be disjoint.
data MemoryRegion sym =
  forall w. (1 <= w) =>
  MemoryRegion
  { forall sym. MemoryRegion sym -> BV 64
regionOffset  :: BV.BV 64 -- ^ Offset of the region, from the base pointer
  , forall sym. MemoryRegion sym -> Bytes
regionSize    :: C.Bytes  -- ^ Length of the memory region, in bytes
  , forall sym. MemoryRegion sym -> StorageType
regionStorage :: C.StorageType -- ^ The storage type used to write to this region
  , ()
regionJoinVar :: W4.SymBV sym w -- ^ The join variable representing this region
  }

-- | Memory block data are used to describe where in memory
--   loop-carried dependencies are.  They may either be
--   "regular" blocks or "array" blocks. A regular block
--   consists of a collection of regions of known size, each
--   of which is at some concretely-known offset from a single
--   master offset value inside the LLVM memory region.
--   An array block consists of an entire LLVM memory region
--   that is backed by an SMT array.
data MemoryBlockData sym where
  RegularBlock ::
    W4.SymBV sym 64
      {- ^ A potentially symbolic base pointer/offset. All the
           offsets in this region are required to be at a concrete
           distance from this base pointer. -} ->
    Map Natural (MemoryRegion sym)
      {- ^ mapping from offset values to regions -} ->
    MemoryBlockData sym

  ArrayBlock   ::
    W4.SymExpr sym ArrayTp {- ^ array join variable -} ->
    W4.SymBV sym 64 {- ^ length of the allocation -} ->
    MemoryBlockData sym

type ArrayTp = W4.BaseArrayType (C.EmptyCtx C.::> W4.BaseBVType 64) (W4.BaseBVType 8)

-- | A memory substitution gives memory block data for
--   concrete memory region numbers of writes occurring
--   in the loop body. This is used to determine where
--   in memory the relevant values are that need to be
--   passed to the loop invariant.
newtype MemorySubstitution sym =
  MemSubst
  { forall sym.
MemorySubstitution sym -> Map Natural (MemoryBlockData sym)
memSubst :: Map Natural (MemoryBlockData sym)
      {- ^ Mapping from block numbers to block data -}
  }


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


-- The fixpoint monad is used to ease the process of computing variable widenings
-- and such.  The included "SymNat" is a memory region number guaranteed not
-- to be a valid memory region; it is used to implement "havoc" registers that
-- we expect to be junk/scratch space across the loop boundary.
-- The state component tracks the variable substitution we are computing.
newtype FixpointMonad sym a =
  FixpointMonad (ReaderT (W4.SymNat sym) (StateT (VariableSubst sym) IO) a)
 deriving ((forall a b.
 (a -> b) -> FixpointMonad sym a -> FixpointMonad sym b)
-> (forall a b. a -> FixpointMonad sym b -> FixpointMonad sym a)
-> Functor (FixpointMonad sym)
forall a b. a -> FixpointMonad sym b -> FixpointMonad sym a
forall a b. (a -> b) -> FixpointMonad sym a -> FixpointMonad sym b
forall sym a b. a -> FixpointMonad sym b -> FixpointMonad sym a
forall sym a b.
(a -> b) -> FixpointMonad sym a -> FixpointMonad sym b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall sym a b.
(a -> b) -> FixpointMonad sym a -> FixpointMonad sym b
fmap :: forall a b. (a -> b) -> FixpointMonad sym a -> FixpointMonad sym b
$c<$ :: forall sym a b. a -> FixpointMonad sym b -> FixpointMonad sym a
<$ :: forall a b. a -> FixpointMonad sym b -> FixpointMonad sym a
Functor, Functor (FixpointMonad sym)
Functor (FixpointMonad sym) =>
(forall a. a -> FixpointMonad sym a)
-> (forall a b.
    FixpointMonad sym (a -> b)
    -> FixpointMonad sym a -> FixpointMonad sym b)
-> (forall a b c.
    (a -> b -> c)
    -> FixpointMonad sym a
    -> FixpointMonad sym b
    -> FixpointMonad sym c)
-> (forall a b.
    FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym b)
-> (forall a b.
    FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym a)
-> Applicative (FixpointMonad sym)
forall sym. Functor (FixpointMonad sym)
forall a. a -> FixpointMonad sym a
forall sym a. a -> FixpointMonad sym a
forall a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym a
forall a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym b
forall a b.
FixpointMonad sym (a -> b)
-> FixpointMonad sym a -> FixpointMonad sym b
forall sym a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym a
forall sym a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym b
forall sym a b.
FixpointMonad sym (a -> b)
-> FixpointMonad sym a -> FixpointMonad sym b
forall a b c.
(a -> b -> c)
-> FixpointMonad sym a
-> FixpointMonad sym b
-> FixpointMonad sym c
forall sym a b c.
(a -> b -> c)
-> FixpointMonad sym a
-> FixpointMonad sym b
-> FixpointMonad sym c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall sym a. a -> FixpointMonad sym a
pure :: forall a. a -> FixpointMonad sym a
$c<*> :: forall sym a b.
FixpointMonad sym (a -> b)
-> FixpointMonad sym a -> FixpointMonad sym b
<*> :: forall a b.
FixpointMonad sym (a -> b)
-> FixpointMonad sym a -> FixpointMonad sym b
$cliftA2 :: forall sym a b c.
(a -> b -> c)
-> FixpointMonad sym a
-> FixpointMonad sym b
-> FixpointMonad sym c
liftA2 :: forall a b c.
(a -> b -> c)
-> FixpointMonad sym a
-> FixpointMonad sym b
-> FixpointMonad sym c
$c*> :: forall sym a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym b
*> :: forall a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym b
$c<* :: forall sym a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym a
<* :: forall a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym a
Applicative, Applicative (FixpointMonad sym)
Applicative (FixpointMonad sym) =>
(forall a b.
 FixpointMonad sym a
 -> (a -> FixpointMonad sym b) -> FixpointMonad sym b)
-> (forall a b.
    FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym b)
-> (forall a. a -> FixpointMonad sym a)
-> Monad (FixpointMonad sym)
forall sym. Applicative (FixpointMonad sym)
forall a. a -> FixpointMonad sym a
forall sym a. a -> FixpointMonad sym a
forall a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym b
forall a b.
FixpointMonad sym a
-> (a -> FixpointMonad sym b) -> FixpointMonad sym b
forall sym a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym b
forall sym a b.
FixpointMonad sym a
-> (a -> FixpointMonad sym b) -> FixpointMonad sym b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall sym a b.
FixpointMonad sym a
-> (a -> FixpointMonad sym b) -> FixpointMonad sym b
>>= :: forall a b.
FixpointMonad sym a
-> (a -> FixpointMonad sym b) -> FixpointMonad sym b
$c>> :: forall sym a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym b
>> :: forall a b.
FixpointMonad sym a -> FixpointMonad sym b -> FixpointMonad sym b
$creturn :: forall sym a. a -> FixpointMonad sym a
return :: forall a. a -> FixpointMonad sym a
Monad, Monad (FixpointMonad sym)
Monad (FixpointMonad sym) =>
(forall a. IO a -> FixpointMonad sym a)
-> MonadIO (FixpointMonad sym)
forall sym. Monad (FixpointMonad sym)
forall a. IO a -> FixpointMonad sym a
forall sym a. IO a -> FixpointMonad sym a
forall (m :: Type -> Type).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall sym a. IO a -> FixpointMonad sym a
liftIO :: forall a. IO a -> FixpointMonad sym a
MonadIO, Monad (FixpointMonad sym)
Monad (FixpointMonad sym) =>
(forall a. String -> FixpointMonad sym a)
-> MonadFail (FixpointMonad sym)
forall sym. Monad (FixpointMonad sym)
forall a. String -> FixpointMonad sym a
forall sym a. String -> FixpointMonad sym a
forall (m :: Type -> Type).
Monad m =>
(forall a. String -> m a) -> MonadFail m
$cfail :: forall sym a. String -> FixpointMonad sym a
fail :: forall a. String -> FixpointMonad sym a
MonadFail)

deriving instance MonadReader (W4.SymNat sym) (FixpointMonad sym)
deriving instance MonadState (VariableSubst sym) (FixpointMonad sym)

runFixpointMonad ::
  W4.SymNat sym ->
  VariableSubst sym ->
  FixpointMonad sym a ->
  IO (a, VariableSubst sym)
runFixpointMonad :: forall sym a.
SymNat sym
-> VariableSubst sym
-> FixpointMonad sym a
-> IO (a, VariableSubst sym)
runFixpointMonad SymNat sym
havoc_blk VariableSubst sym
subst (FixpointMonad ReaderT (SymNat sym) (StateT (VariableSubst sym) IO) a
m) =
  StateT (VariableSubst sym) IO a
-> VariableSubst sym -> IO (a, VariableSubst sym)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT (ReaderT (SymNat sym) (StateT (VariableSubst sym) IO) a
-> SymNat sym -> StateT (VariableSubst sym) IO a
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT ReaderT (SymNat sym) (StateT (VariableSubst sym) IO) a
m SymNat sym
havoc_blk) VariableSubst sym
subst

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 -> FixpointMonad sym (RegEntry sym x))
-> Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx
-> FixpointMonad sym (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
-> FixpointMonad sym (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 = do
 VariableSubst sym
subst <- FixpointMonad sym (VariableSubst sym)
forall s (m :: Type -> Type). MonadState s m => m s
get
 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

      -- TODO! This is a "particularly guesome hack" it would be nice to find some better
      --  way to handle this situation.
      -- 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
      -- liftIO $ ?logMessage "SimpleLoopInvariant.joinRegEntry: cmacaw_reg"
      RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> FixpointMonad sym 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)
    , Maybe (Const () (BaseBVType w))
Nothing <- SymExpr sym (BaseBVType w)
-> MapF (SymExpr sym) (Const ()) -> Maybe (Const () (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)) (VariableSubst sym -> MapF (SymExpr sym) (Const ())
forall sym. VariableSubst sym -> MapF (SymExpr sym) (Const ())
varHavoc VariableSubst sym
subst) -> do
      -- liftIO $ ?logMessage "SimpleLoopInvariant.joinRegEntry: LLVMPointerRepr"
      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
        -- liftIO $ ?logMessage "SimpleLoopInvariant.joinRegEntry: LLVMPointerRepr: left == right"
        RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> FixpointMonad sym 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) (InvariantEntry sym)
-> Maybe (InvariantEntry 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)) (VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
forall sym.
VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
varSubst VariableSubst sym
subst) of
        Just InvariantEntry sym (BaseBVType w)
join_entry -> do
          -- liftIO $ ?logMessage $
          --   "SimpleLoopInvariant.joinRegEntry: LLVMPointerRepr: Just: "
          --   ++ show (W4.printSymExpr $ bodyValue join_entry)
          --   ++ " -> "
          --   ++ show (W4.printSymExpr $ C.llvmPointerOffset (C.regValue right))
          VariableSubst sym -> FixpointMonad sym ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put (VariableSubst sym -> FixpointMonad sym ())
-> VariableSubst sym -> FixpointMonad sym ()
forall a b. (a -> b) -> a -> b
$ VariableSubst sym
subst{ varSubst =
            MapF.insert
              (C.llvmPointerOffset (C.regValue left))
              (join_entry { bodyValue = C.llvmPointerOffset (C.regValue right) })
              (varSubst subst) }
          RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> FixpointMonad sym a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RegEntry sym tp
left
        Maybe (InvariantEntry sym (BaseBVType w))
Nothing -> do
          IO () -> FixpointMonad sym ()
forall a. IO a -> FixpointMonad sym a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> FixpointMonad sym ()) -> IO () -> FixpointMonad sym ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage String
"SimpleLoopInvariant.joinRegEntry: LLVMPointerRepr: Nothing"
          SymExpr sym (BaseBVType w)
join_variable <- IO (SymExpr sym (BaseBVType w))
-> FixpointMonad sym (SymExpr sym (BaseBVType w))
forall a. IO a -> FixpointMonad sym a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType w))
 -> FixpointMonad sym (SymExpr sym (BaseBVType w)))
-> IO (SymExpr sym (BaseBVType w))
-> FixpointMonad sym (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
W4.safeSymbol 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 :: InvariantEntry sym (BaseBVType w)
join_entry = InvariantEntry
                { 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)
                }
          VariableSubst sym -> FixpointMonad sym ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put (VariableSubst sym -> FixpointMonad sym ())
-> VariableSubst sym -> FixpointMonad sym ()
forall a b. (a -> b) -> a -> b
$ VariableSubst sym
subst{ varSubst = MapF.insert join_variable join_entry (varSubst subst) }
          RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> FixpointMonad sym 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_variable

    | Bool
otherwise -> do
      IO () -> FixpointMonad sym ()
forall a. IO a -> FixpointMonad sym a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> FixpointMonad sym ()) -> IO () -> FixpointMonad sym ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage String
"SimpleLoopInvariant.joinRegEntry: LLVMPointerRepr, unequal blocks!"
      SymNat sym
havoc_blk <- FixpointMonad sym (SymNat sym)
forall r (m :: Type -> Type). MonadReader r m => m r
ask
      case SymExpr sym (BaseBVType w)
-> MapF (SymExpr sym) (InvariantEntry sym)
-> Maybe (InvariantEntry 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)) (VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
forall sym.
VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
varSubst VariableSubst sym
subst) of
        Just InvariantEntry sym (BaseBVType w)
_ -> do
          -- widening varible already present in the var substitition.
          -- we need to remove it, and add it to the havoc map instead
          VariableSubst sym -> FixpointMonad sym ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put VariableSubst sym
subst { varSubst = MapF.delete (C.llvmPointerOffset (C.regValue left)) (varSubst subst)
                    , varHavoc = MapF.insert (C.llvmPointerOffset (C.regValue left)) (Const ()) (varHavoc subst)
                    }
          RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> FixpointMonad sym 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 SymNat sym
havoc_blk (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))

        Maybe (InvariantEntry sym (BaseBVType w))
Nothing -> do
          SymExpr sym (BaseBVType w)
havoc_var <- IO (SymExpr sym (BaseBVType w))
-> FixpointMonad sym (SymExpr sym (BaseBVType w))
forall a. IO a -> FixpointMonad sym a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType w))
 -> FixpointMonad sym (SymExpr sym (BaseBVType w)))
-> IO (SymExpr sym (BaseBVType w))
-> FixpointMonad sym (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
W4.safeSymbol String
"havoc_var") (NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr NatRepr w
w)
          VariableSubst sym -> FixpointMonad sym ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put VariableSubst sym
subst{ varHavoc = MapF.insert havoc_var (Const ()) (varHavoc subst) }
          RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> FixpointMonad sym 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 SymNat sym
havoc_blk SymExpr sym (BaseBVType w)
havoc_var

  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 () -> FixpointMonad sym ()
forall a. IO a -> FixpointMonad sym a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> FixpointMonad sym ()) -> IO () -> FixpointMonad sym ()
forall a b. (a -> b) -> a -> b
$ ?logMessage::String -> IO ()
String -> IO ()
?logMessage String
"SimpleLoopInvariant.joinRegEntry: cmacaw_reg"
      RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> FixpointMonad sym a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RegEntry sym tp
left
    | Bool
otherwise -> do
      -- liftIO $ ?logMessage $
      --   "SimpleLoopInvariant.joinRegEntry: BoolRepr:"
      --   ++ show (W4.printSymExpr $ C.regValue left)
      --   ++ " \\/ "
      --   ++ show (W4.printSymExpr $ C.regValue right)
      SymExpr sym BaseBoolType
join_varaible <- IO (SymExpr sym BaseBoolType)
-> FixpointMonad sym (SymExpr sym BaseBoolType)
forall a. IO a -> FixpointMonad sym a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> FixpointMonad sym (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> FixpointMonad sym (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
W4.safeSymbol String
"reg_join_var") BaseTypeRepr BaseBoolType
W4.BaseBoolRepr
      RegEntry sym tp -> FixpointMonad sym (RegEntry sym tp)
forall a. a -> FixpointMonad sym 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
    -- liftIO $ ?logMessage "SimpleLoopInvariant.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)
-> FixpointMonad sym (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
-> FixpointMonad sym (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 -> FixpointMonad sym 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
"SimpleLoopInvariant.joinRegEntry: unsupported type: " String -> ShowS
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 -> RegEntry sym tp
forall a. HasCallStack => String -> a
error (String -> RegEntry sym tp) -> String -> RegEntry sym tp
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"SimpleLoopInvariant.applySubstitutionRegEntry"
                       , String
"unsupported type: " String -> ShowS
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)
                       ]


loadMemJoinVariables ::
  (C.IsSymBackend sym bak, C.HasPtrWidth 64, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) =>
  bak ->
  C.MemImpl sym ->
  MemorySubstitution sym ->
  IO (MapF (W4.SymExpr sym) (W4.SymExpr sym))
loadMemJoinVariables :: forall sym bak.
(IsSymBackend sym bak, HasPtrWidth 64, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> MemorySubstitution sym
-> IO (MapF (SymExpr sym) (SymExpr sym))
loadMemJoinVariables bak
bak MemImpl sym
mem (MemSubst Map Natural (MemoryBlockData sym)
subst) = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
C.backendGetSym bak
bak

  [[Pair (SymExpr sym) (SymExpr sym)]]
vars <- [(Natural, MemoryBlockData sym)]
-> ((Natural, MemoryBlockData sym)
    -> IO [Pair (SymExpr sym) (SymExpr sym)])
-> IO [[Pair (SymExpr sym) (SymExpr sym)]]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map Natural (MemoryBlockData sym)
-> [(Natural, MemoryBlockData sym)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map Natural (MemoryBlockData sym)
subst) (((Natural, MemoryBlockData sym)
  -> IO [Pair (SymExpr sym) (SymExpr sym)])
 -> IO [[Pair (SymExpr sym) (SymExpr sym)]])
-> ((Natural, MemoryBlockData sym)
    -> IO [Pair (SymExpr sym) (SymExpr sym)])
-> IO [[Pair (SymExpr sym) (SymExpr sym)]]
forall a b. (a -> b) -> a -> b
$ \ (Natural
blk, MemoryBlockData sym
blkData) ->
            case MemoryBlockData sym
blkData of
              ArrayBlock SymExpr sym ArrayTp
arr_var SymBV sym 64
_sz ->
                do LLVMPointer sym 64
base_ptr <- SymNat sym -> SymBV sym 64 -> LLVMPointer sym 64
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
C.LLVMPointer (SymNat sym -> SymBV sym 64 -> LLVMPointer sym 64)
-> IO (SymNat sym) -> IO (SymBV sym 64 -> LLVMPointer sym 64)
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 64 -> LLVMPointer sym 64)
-> IO (SymBV sym 64) -> IO (LLVMPointer sym 64)
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 64 -> BV 64 -> IO (SymBV sym 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 (NatRepr 64 -> Integer -> BV 64
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr 64
NatRepr 64
?ptrWidth Integer
0)
                   Maybe (SymExpr sym BaseBoolType, SymExpr sym ArrayTp, SymBV sym 64)
res <- sym
-> NatRepr 64
-> LLVMPtr sym 64
-> Mem sym
-> IO
     (Maybe
        (SymExpr sym BaseBoolType, SymExpr sym ArrayTp, SymBV sym 64))
forall sym (w :: Natural).
(IsSymInterface sym, 1 <= w) =>
sym
-> NatRepr w
-> LLVMPtr sym w
-> Mem sym
-> IO
     (Maybe
        (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8),
         SymBV sym w))
C.asMemAllocationArrayStore sym
sym ?ptrWidth::NatRepr 64
NatRepr 64
?ptrWidth LLVMPtr sym 64
LLVMPointer sym 64
base_ptr (MemImpl sym -> Mem sym
forall sym. MemImpl sym -> Mem sym
C.memImplHeap MemImpl sym
mem)
                   case Maybe (SymExpr sym BaseBoolType, SymExpr sym ArrayTp, SymBV sym 64)
res of
                     Maybe (SymExpr sym BaseBoolType, SymExpr sym ArrayTp, SymBV sym 64)
Nothing -> 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
"Expected SMT array in memory image for block number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
blk
                     Just (SymExpr sym BaseBoolType
_ok, SymExpr sym ArrayTp
arr, SymBV sym 64
_len2) ->
                       -- TODO: we need to assert the load condition...
                       -- TODO? Should we assert the lengths match?

                       [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 [SymExpr sym ArrayTp
-> SymExpr sym ArrayTp -> Pair (SymExpr sym) (SymExpr sym)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
MapF.Pair SymExpr sym ArrayTp
arr_var SymExpr sym ArrayTp
arr]

              RegularBlock SymBV sym 64
basePtr Map Natural (MemoryRegion sym)
offsetMap ->
                [(Natural, MemoryRegion sym)]
-> ((Natural, MemoryRegion sym)
    -> IO (Pair (SymExpr sym) (SymExpr sym)))
-> IO [Pair (SymExpr sym) (SymExpr sym)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map Natural (MemoryRegion sym) -> [(Natural, MemoryRegion sym)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map Natural (MemoryRegion sym)
offsetMap) (((Natural, MemoryRegion sym)
  -> IO (Pair (SymExpr sym) (SymExpr sym)))
 -> IO [Pair (SymExpr sym) (SymExpr sym)])
-> ((Natural, MemoryRegion sym)
    -> IO (Pair (SymExpr sym) (SymExpr sym)))
-> IO [Pair (SymExpr sym) (SymExpr sym)]
forall a b. (a -> b) -> a -> b
$
                  \ (Natural
_off , MemoryRegion{ regionJoinVar :: ()
regionJoinVar = SymBV sym w
join_var, regionStorage :: forall sym. MemoryRegion sym -> StorageType
regionStorage = StorageType
storage_type, regionOffset :: forall sym. MemoryRegion sym -> BV 64
regionOffset = BV 64
offBV }) ->
                    do SymNat sym
blk' <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
W4.natLit sym
sym Natural
blk
                       SymBV sym 64
off' <- sym -> SymBV sym 64 -> SymBV sym 64 -> IO (SymBV sym 64)
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.bvAdd sym
sym SymBV sym 64
basePtr (SymBV sym 64 -> IO (SymBV sym 64))
-> IO (SymBV sym 64) -> IO (SymBV sym 64)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr 64 -> BV 64 -> IO (SymBV sym 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
offBV
                       let ptr :: LLVMPointer sym 64
ptr = SymNat sym -> SymBV sym 64 -> LLVMPointer sym 64
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
C.LLVMPointer SymNat sym
blk' SymBV sym 64
off'
                       SymBV sym w
val <- sym
-> MemImpl sym
-> LLVMPtr sym 64
-> StorageType
-> SymBV sym w
-> Alignment
-> IO (RegValue sym (BVType w))
forall sym (wptr :: Natural) (w :: Natural).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, 1 <= w) =>
sym
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> SymBV sym w
-> Alignment
-> IO (RegValue sym (BVType w))
safeBVLoad sym
sym MemImpl sym
mem LLVMPtr sym 64
LLVMPointer sym 64
ptr StorageType
storage_type SymBV sym w
join_var Alignment
C.noAlignment
                       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 (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_var SymBV sym w
val)

  MapF (SymExpr sym) (SymExpr sym)
-> IO (MapF (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)]
-> 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)]]
-> [Pair (SymExpr sym) (SymExpr sym)]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [[Pair (SymExpr sym) (SymExpr sym)]]
vars))


safeBVLoad ::
  ( C.IsSymInterface sym, C.HasPtrWidth wptr, C.HasLLVMAnn sym
  , ?memOpts :: C.MemOptions, 1 <= w ) =>
  sym ->
  C.MemImpl sym ->
  C.LLVMPtr sym wptr {- ^ pointer to load from      -} ->
  C.StorageType      {- ^ type of value to load     -} ->
  W4.SymBV sym w     {- ^ default value to return -} ->
  C.Alignment        {- ^ assumed pointer alignment -} ->
  IO (C.RegValue sym (C.BVType w))
safeBVLoad :: forall sym (wptr :: Natural) (w :: Natural).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, 1 <= w) =>
sym
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> SymBV sym w
-> Alignment
-> IO (RegValue sym (BVType w))
safeBVLoad sym
sym MemImpl sym
mem LLVMPtr sym wptr
ptr StorageType
st SymBV sym w
def Alignment
align =
  do let w :: NatRepr w
w = 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
def
     PartLLVMVal sym
pval <- sym
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> Alignment
-> IO (PartLLVMVal sym)
forall sym (wptr :: Natural).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
sym
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> Alignment
-> IO (PartLLVMVal sym)
C.loadRaw sym
sym MemImpl sym
mem LLVMPtr sym wptr
ptr StorageType
st Alignment
align
     case PartLLVMVal sym
pval of
       C.Err Pred sym
_ -> SymBV sym w -> IO (SymBV sym w)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymBV sym w
def
       C.NoErr Pred sym
p LLVMVal sym
v ->
         do RegValue sym (LLVMPointerType w)
v' <- sym
-> TypeRepr (LLVMPointerType w)
-> LLVMVal sym
-> IO (RegValue sym (LLVMPointerType w))
forall sym (tp :: CrucibleType).
(HasCallStack, IsSymInterface sym) =>
sym -> TypeRepr tp -> LLVMVal sym -> IO (RegValue sym tp)
C.unpackMemValue sym
sym (NatRepr w -> TypeRepr (LLVMPointerType w)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
C.LLVMPointerRepr NatRepr w
w) LLVMVal sym
v
            Pred sym
p0 <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
W4.natEq sym
sym (RegValue sym (LLVMPointerType w) -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
C.llvmPointerBlock RegValue sym (LLVMPointerType w)
v') (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
W4.natLit sym
sym Natural
0
            Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred sym
sym Pred sym
p Pred sym
p0
            sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvIte sym
sym Pred sym
p' (RegValue sym (LLVMPointerType w) -> SymBV sym w
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset RegValue sym (LLVMPointerType w)
v') SymBV sym w
def

storeMemJoinVariables ::
  (C.IsSymBackend sym bak, C.HasPtrWidth 64, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) =>
  bak ->
  C.MemImpl sym ->
  MemorySubstitution sym ->
  MapF (W4.SymExpr sym) (W4.SymExpr sym) ->
  IO (C.MemImpl sym)
storeMemJoinVariables :: forall sym bak.
(IsSymBackend sym bak, HasPtrWidth 64, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> MemorySubstitution sym
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
storeMemJoinVariables bak
bak MemImpl sym
mem (MemSubst Map Natural (MemoryBlockData sym)
mem_subst) MapF (SymExpr sym) (SymExpr sym)
eq_subst =
  (MemImpl sym -> (Natural, MemoryBlockData sym) -> IO (MemImpl sym))
-> MemImpl sym
-> [(Natural, MemoryBlockData sym)]
-> 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, MemoryBlockData sym
blk_data) ->
        case MemoryBlockData sym
blk_data of
          RegularBlock SymBV sym 64
basePtr Map Natural (MemoryRegion sym)
off_map ->
            (MemImpl sym -> (Natural, MemoryRegion sym) -> IO (MemImpl sym))
-> MemImpl sym -> [(Natural, MemoryRegion sym)] -> 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 (Natural
-> SymBV sym 64
-> MemImpl sym
-> (Natural, MemoryRegion sym)
-> IO (MemImpl sym)
writeMemRegion Natural
blk SymBV sym 64
basePtr) MemImpl sym
mem_acc (Map Natural (MemoryRegion sym) -> [(Natural, MemoryRegion sym)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map Natural (MemoryRegion sym)
off_map)
          ArrayBlock SymExpr sym ArrayTp
arr SymBV sym 64
len ->
            do LLVMPointer sym 64
base_ptr <- SymNat sym -> SymBV sym 64 -> LLVMPointer sym 64
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
C.LLVMPointer (SymNat sym -> SymBV sym 64 -> LLVMPointer sym 64)
-> IO (SymNat sym) -> IO (SymBV sym 64 -> LLVMPointer sym 64)
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 64 -> LLVMPointer sym 64)
-> IO (SymBV sym 64) -> IO (LLVMPointer sym 64)
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 64 -> BV 64 -> IO (SymBV sym 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 (NatRepr 64 -> Integer -> BV 64
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr 64
NatRepr 64
?ptrWidth Integer
0)
               let arr' :: SymExpr sym ArrayTp
arr' = SymExpr sym ArrayTp
-> SymExpr sym ArrayTp
-> MapF (SymExpr sym) (SymExpr sym)
-> SymExpr sym ArrayTp
forall {v} (k :: v -> Type) (a :: v -> Type) (tp :: v).
OrdF k =>
a tp -> k tp -> MapF k a -> a tp
MapF.findWithDefault SymExpr sym ArrayTp
arr SymExpr sym ArrayTp
arr MapF (SymExpr sym) (SymExpr sym)
eq_subst
               bak
-> MemImpl sym
-> LLVMPtr sym 64
-> Alignment
-> SymExpr sym ArrayTp
-> SymBV sym 64
-> IO (MemImpl sym)
forall sym bak (w :: Natural).
(IsSymBackend sym bak, HasPtrWidth w, HasLLVMAnn sym) =>
bak
-> MemImpl sym
-> LLVMPtr sym w
-> Alignment
-> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
-> SymBV sym w
-> IO (MemImpl sym)
C.doArrayStore bak
bak MemImpl sym
mem_acc LLVMPtr sym 64
LLVMPointer sym 64
base_ptr Alignment
C.noAlignment SymExpr sym ArrayTp
arr' SymBV sym 64
len)
     MemImpl sym
mem
     (Map Natural (MemoryBlockData sym)
-> [(Natural, MemoryBlockData sym)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map Natural (MemoryBlockData sym)
mem_subst)

 where
  sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
C.backendGetSym bak
bak

  writeMemRegion :: Natural
-> SymBV sym 64
-> MemImpl sym
-> (Natural, MemoryRegion sym)
-> IO (MemImpl sym)
writeMemRegion Natural
blk SymBV sym 64
basePtr MemImpl sym
mem_acc (Natural
_off, MemoryRegion{ regionJoinVar :: ()
regionJoinVar = SymBV sym w
join_var, regionStorage :: forall sym. MemoryRegion sym -> StorageType
regionStorage = StorageType
storage_type, regionOffset :: forall sym. MemoryRegion sym -> BV 64
regionOffset = BV 64
offBV }) =
    do SymNat sym
blk' <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
W4.natLit sym
sym Natural
blk
       SymBV sym 64
off' <- sym -> SymBV sym 64 -> SymBV sym 64 -> IO (SymBV sym 64)
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.bvAdd sym
sym SymBV sym 64
basePtr (SymBV sym 64 -> IO (SymBV sym 64))
-> IO (SymBV sym 64) -> IO (SymBV sym 64)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr 64 -> BV 64 -> IO (SymBV sym 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
offBV
       let ptr :: LLVMPointer sym 64
ptr = SymNat sym -> SymBV sym 64 -> LLVMPointer sym 64
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
C.LLVMPointer SymNat sym
blk' SymBV sym 64
off'
       bak
-> MemImpl sym
-> LLVMPtr sym 64
-> 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 64
LLVMPointer sym 64
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_var) StorageType
storage_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_var SymBV sym w
join_var MapF (SymExpr sym) (SymExpr sym)
eq_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
"SimpleLoopInvariant.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 ->
  VariableSubst sym ->
  VariableSubst sym
filterSubstitution :: forall sym.
IsSymInterface sym =>
sym -> VariableSubst sym -> VariableSubst sym
filterSubstitution sym
sym (VarSubst MapF (SymExpr sym) (InvariantEntry sym)
substitution MapF (SymExpr sym) (Const ())
havoc) =
  -- TODO: fixpoint
  let uninterp_constants :: Set (Some (SymExpr sym))
uninterp_constants = (forall (s :: BaseType).
 InvariantEntry sym s -> Set (Some (SymExpr sym)))
-> MapF (SymExpr sym) (InvariantEntry 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)))
-> (InvariantEntry sym s -> Set (Some (BoundVar sym)))
-> InvariantEntry 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)))
-> (InvariantEntry sym s -> SymExpr sym s)
-> InvariantEntry sym s
-> Set (Some (BoundVar sym))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InvariantEntry sym s -> SymExpr sym s
forall sym (tp :: BaseType).
InvariantEntry sym tp -> SymExpr sym tp
bodyValue)
        MapF (SymExpr sym) (InvariantEntry sym)
substitution
  in
  MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (Const ()) -> VariableSubst sym
forall sym.
MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (Const ()) -> VariableSubst sym
VarSubst
    ((forall (tp :: BaseType).
 SymExpr sym tp -> InvariantEntry sym tp -> Bool)
-> MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (InvariantEntry 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 InvariantEntry 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) (InvariantEntry sym)
substitution)
    MapF (SymExpr sym) (Const ())
havoc

-- 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 ->
  VariableSubst sym ->
  (VariableSubst sym, MapF (W4.SymExpr sym) (W4.SymExpr sym))
uninterpretedConstantEqualitySubstitution :: forall sym.
IsSymInterface sym =>
sym
-> VariableSubst sym
-> (VariableSubst sym, MapF (SymExpr sym) (SymExpr sym))
uninterpretedConstantEqualitySubstitution sym
_sym (VarSubst MapF (SymExpr sym) (InvariantEntry sym)
substitution MapF (SymExpr sym) (Const ())
havoc) =
  let reverse_substitution :: MapF (InvariantEntry sym) (SymExpr sym)
reverse_substitution = (forall (s :: BaseType).
 MapF (InvariantEntry sym) (SymExpr sym)
 -> SymExpr sym s
 -> InvariantEntry sym s
 -> MapF (InvariantEntry sym) (SymExpr sym))
-> MapF (InvariantEntry sym) (SymExpr sym)
-> MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (InvariantEntry 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 (InvariantEntry sym) (SymExpr sym)
accumulator SymExpr sym s
variable InvariantEntry sym s
entry -> InvariantEntry sym s
-> SymExpr sym s
-> MapF (InvariantEntry sym) (SymExpr sym)
-> MapF (InvariantEntry 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 InvariantEntry sym s
entry SymExpr sym s
variable MapF (InvariantEntry sym) (SymExpr sym)
accumulator)
        MapF (InvariantEntry sym) (SymExpr sym)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
        MapF (SymExpr sym) (InvariantEntry sym)
substitution
      uninterpreted_constant_substitution :: MapF (SymExpr sym) (SymExpr sym)
uninterpreted_constant_substitution = (forall (x :: BaseType). InvariantEntry sym x -> SymExpr sym x)
-> MapF (SymExpr sym) (InvariantEntry 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
        (\InvariantEntry 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
$ InvariantEntry sym x
-> MapF (InvariantEntry 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 InvariantEntry sym x
entry MapF (InvariantEntry sym) (SymExpr sym)
reverse_substitution)
        MapF (SymExpr sym) (InvariantEntry sym)
substitution
      normal_substitution :: MapF (SymExpr sym) (InvariantEntry sym)
normal_substitution = (forall (tp :: BaseType).
 SymExpr sym tp -> InvariantEntry sym tp -> Bool)
-> MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (InvariantEntry 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 InvariantEntry 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) (InvariantEntry sym)
substitution
  in
  (MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (Const ()) -> VariableSubst sym
forall sym.
MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (Const ()) -> VariableSubst sym
VarSubst MapF (SymExpr sym) (InvariantEntry sym)
normal_substitution MapF (SymExpr sym) (Const ())
havoc, MapF (SymExpr sym) (SymExpr sym)
uninterpreted_constant_substitution)


-- | Given the WTO analysis results, find the nth loop.
--   Return the identifier of the loop header, and a list of all the blocks
--   that are part of the loop body. It is at this point that we check
--   that the loop has the necessary properties; there must be a single
--   entry point to the loop, and it must have a single back-edge. Otherwise,
--   the analysis will not work correctly.
computeLoopBlocks :: forall ext blocks init ret k. (k ~ C.Some (C.BlockID blocks)) =>
  C.CFG ext blocks init ret ->
  Integer ->
  IO (k, [k])
computeLoopBlocks :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) k.
(k ~ Some (BlockID blocks)) =>
CFG ext blocks init ret -> Integer -> IO (k, [k])
computeLoopBlocks CFG ext blocks init ret
cfg Integer
loopNum =
  case Integer
-> [(Some (BlockID blocks), [Some (BlockID blocks)])]
-> [(Some (BlockID blocks), [Some (BlockID blocks)])]
forall i a. Integral i => i -> [a] -> [a]
List.genericDrop Integer
loopNum (Map (Some (BlockID blocks)) [Some (BlockID blocks)]
-> [(Some (BlockID blocks), [Some (BlockID blocks)])]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Some (BlockID blocks)) [Some (BlockID blocks)]
loop_map) of
    [] -> String -> IO (k, [k])
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
"Did not find " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
loopNum String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" loop headers")
    ((Some (BlockID blocks), [Some (BlockID blocks)])
p:[(Some (BlockID blocks), [Some (BlockID blocks)])]
_) -> do (k, [k]) -> IO ()
checkSingleEntry (k, [k])
(Some (BlockID blocks), [Some (BlockID blocks)])
p
                (k, [k]) -> IO ()
checkSingleBackedge (k, [k])
(Some (BlockID blocks), [Some (BlockID blocks)])
p
                (k, [k]) -> IO (k, [k])
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (k, [k])
(Some (BlockID blocks), [Some (BlockID blocks)])
p

 where
  -- There should be exactly one block which is not part of the loop body that
  -- can jump to @hd@.
  checkSingleEntry :: (k,[k]) -> IO ()
  checkSingleEntry :: (k, [k]) -> IO ()
checkSingleEntry (k
hd, [k]
body) =
    case (k -> Bool) -> [k] -> [k]
forall a. (a -> Bool) -> [a] -> [a]
filter (\k
x -> Bool -> Bool
not (k -> [k] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
elem k
x [k]
body) Bool -> Bool -> Bool
&& k -> [k] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
elem k
hd (CFG ext blocks init ret
-> Some (BlockID blocks) -> [Some (BlockID blocks)]
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Some (BlockID blocks) -> [Some (BlockID blocks)]
C.cfgSuccessors CFG ext blocks init ret
cfg k
Some (BlockID blocks)
x)) [k]
[Some (BlockID blocks)]
allReachable of
      [k
_] -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
      [k]
_   -> String -> IO ()
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"SimpleLoopInvariant feature requires a single-entry loop!"

  -- There should be exactly on block in the loop body which can jump to @hd@.
  checkSingleBackedge :: (k,[k]) -> IO ()
  checkSingleBackedge :: (k, [k]) -> IO ()
checkSingleBackedge (k
hd, [k]
body) =
    case (Some (BlockID blocks) -> Bool)
-> [Some (BlockID blocks)] -> [Some (BlockID blocks)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Some (BlockID blocks)
x -> k -> [k] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
elem k
hd (CFG ext blocks init ret
-> Some (BlockID blocks) -> [Some (BlockID blocks)]
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Some (BlockID blocks) -> [Some (BlockID blocks)]
C.cfgSuccessors CFG ext blocks init ret
cfg Some (BlockID blocks)
x)) [k]
[Some (BlockID blocks)]
body of
      [Some (BlockID blocks)
_] -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
      [Some (BlockID blocks)]
_   -> String -> IO ()
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"SimpleLoopInvariant feature requires a loop with a single backedge!"

  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]

  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)
    [WTOComponent (Some (BlockID blocks))]
wto

  allReachable :: [Some (BlockID blocks)]
allReachable = (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))]
wto

  wto :: [WTOComponent (Some (BlockID blocks))]
wto = 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


-- | 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 notably, it only really works properly for functions
--   consisting of a single, non-nested loop with a single exit point.
--   Moreover, the loop must have an indexing variable that counts up
--   from a starting point by a fixed stride amount.
--
--   Currently, these assumptions about the loop structure are not
--   checked.
--
--   The basic use case here is for verifying functions that loop
--   through an array of data of symbolic length.  This is done by
--   providing a \"fixpoint function\" which describes how the live
--   values in the loop at an arbitrary iteration are used to compute
--   the final values of those variables before execution leaves the
--   loop. The number and order of these variables depends on
--   internal details of the representation, so is relatively fragile.
simpleLoopInvariant ::
  forall sym ext p rtp blocks init ret .
  (C.IsSymInterface sym, C.IsSyntaxExtension ext, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) =>
  sym ->
  Integer {- ^ which of the discovered loop heads to install a loop invariant onto -}  ->
  C.CFG ext blocks init ret {- ^ The function we want to verify -} ->
  C.GlobalVar C.Mem {- ^ global variable representing memory -} ->
  (InvariantPhase -> [Some (W4.SymExpr sym)] -> MapF (W4.SymExpr sym) (InvariantEntry sym) -> IO (W4.Pred sym)) ->
  IO (C.ExecutionFeature p sym ext rtp)
simpleLoopInvariant :: forall sym ext p rtp (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
sym
-> Integer
-> CFG ext blocks init ret
-> GlobalVar Mem
-> (InvariantPhase
    -> [Some (SymExpr sym)]
    -> MapF (SymExpr sym) (InvariantEntry sym)
    -> IO (Pred sym))
-> IO (ExecutionFeature p sym ext rtp)
simpleLoopInvariant sym
sym Integer
loopNum 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 InvariantPhase
-> [Some (SymExpr sym)]
-> MapF (SymExpr sym) (InvariantEntry sym)
-> IO (Pred sym)
loop_invariant = do
  -- TODO, can we lift this restriction to 64-bits? I don't think there
  -- is anything fundamental about it.
  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

  (Some (BlockID blocks)
loop_header, [Some (BlockID blocks)]
loop_body_blocks) <- CFG ext blocks init ret
-> Integer -> IO (Some (BlockID blocks), [Some (BlockID blocks)])
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) k.
(k ~ Some (BlockID blocks)) =>
CFG ext blocks init ret -> Integer -> IO (k, [k])
computeLoopBlocks CFG ext blocks init ret
cfg Integer
loopNum

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

  --putStrLn "Setting up simple loop fixpoints feature."
  --putStrLn ("WTO: " ++ show (C.cfgWeakTopologicalOrdering cfg))

  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 p sym ext rtp blocks
fixpoint_state <- IORef (FixpointState p sym ext rtp blocks)
-> IO (FixpointState p sym ext rtp blocks)
forall a. IORef a -> IO a
readIORef IORef (FixpointState p sym ext rtp 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)

          -- is this state at thea loop header?
        , BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
C.Some BlockID blocks args
block_id Some (BlockID blocks) -> Some (BlockID blocks) -> Bool
forall a. Eq a => a -> a -> Bool
== Some (BlockID blocks)
Some (BlockID blocks)
loop_header ->

            bak
-> GlobalVar Mem
-> (InvariantPhase
    -> [Some (SymExpr sym)]
    -> MapF (SymExpr sym) (InvariantEntry sym)
    -> IO (Pred sym))
-> BlockID blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> FixpointState p sym ext rtp blocks
-> IORef (FixpointState p sym ext rtp 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
-> (InvariantPhase
    -> [Some (SymExpr sym)]
    -> MapF (SymExpr sym) (InvariantEntry sym)
    -> IO (Pred sym))
-> BlockID blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> FixpointState p sym ext rtp blocks
-> IORef (FixpointState p sym ext rtp blocks)
-> IO (ExecutionFeatureResult p sym ext rtp)
advanceFixpointState bak
bak GlobalVar Mem
mem_var InvariantPhase
-> [Some (SymExpr sym)]
-> MapF (SymExpr sym) (InvariantEntry sym)
-> IO (Pred sym)
loop_invariant BlockID blocks args
block_id SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state FixpointState p sym ext rtp blocks
FixpointState p sym ext rtp blocks
fixpoint_state IORef (FixpointState p sym ext rtp blocks)
IORef (FixpointState p sym ext rtp 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
"SimpleLoopInvariant: RunningState: RunBlockStart: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BlockID blocks args -> String
forall a. Show a => a -> String
show BlockID blocks args
block_id String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SomeHandle -> String
forall a. Show a => a -> String
show (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))
            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

      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 p sym ext rtp blocks
_fixpointRecord <- FixpointState p sym ext rtp blocks
-> Maybe (FixpointRecord p sym ext rtp blocks)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointState p sym ext rtp blocks
-> Maybe (FixpointRecord p sym ext rtp blocks)
fixpointRecord FixpointState p sym ext rtp blocks
fixpoint_state
          , 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_blocks 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_blocks -> do

            (Pred sym
loop_condition, PausedFrame p sym ext rtp f
inside_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_blocks
              then
                (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
branch_condition, PausedFrame p sym ext rtp f
true_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)
-> 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_branch_condition, PausedFrame p sym ext rtp f
false_frame)

            case FixpointState p sym ext rtp blocks
fixpoint_state of
              FixpointState p sym ext rtp blocks
BeforeFixpoint -> String -> [String] -> IO (ExecutionFeatureResult p sym ext rtp)
forall a. HasCallStack => String -> [String] -> a
C.panic String
"SimpleLoopInvariant.simpleLoopInvariant:" [String
"BeforeFixpoint"]

              ComputeFixpoint FrameIdentifier
_assumeIdent FixpointRecord p sym ext rtp 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
"SimpleLoopInvariant: SymbolicBranchState: ComputeFixpoint"

                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
inside_loop_frame) Pred sym
loop_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
inside_loop_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

              CheckFixpoint FixpointRecord p sym ext rtp blocks
_fixpoint_record -> do
                ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopInvariant: SymbolicBranchState: CheckFixpoint"

                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

      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 ->
  (InvariantPhase -> [Some (W4.SymExpr sym)] -> MapF (W4.SymExpr sym) (InvariantEntry sym) -> IO (W4.Pred sym)) ->
  C.BlockID blocks args ->
  C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) ->
  FixpointState p sym ext rtp blocks ->
  IORef (FixpointState p sym ext rtp 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
-> (InvariantPhase
    -> [Some (SymExpr sym)]
    -> MapF (SymExpr sym) (InvariantEntry sym)
    -> IO (Pred sym))
-> BlockID blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> FixpointState p sym ext rtp blocks
-> IORef (FixpointState p sym ext rtp blocks)
-> IO (ExecutionFeatureResult p sym ext rtp)
advanceFixpointState bak
bak GlobalVar Mem
mem_var InvariantPhase
-> [Some (SymExpr sym)]
-> MapF (SymExpr sym) (InvariantEntry sym)
-> IO (Pred sym)
loop_invariant BlockID blocks args
block_id SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state FixpointState p sym ext rtp blocks
fixpoint_state IORef (FixpointState p sym ext rtp blocks)
fixpoint_state_ref = do
  let ?ptrWidth = forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
C.backendGetSym bak
bak
  ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
W4.getCurrentProgramLoc sym
sym
  case FixpointState p sym ext rtp blocks
fixpoint_state of
    FixpointState p sym ext rtp blocks
BeforeFixpoint -> do
      ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopInvariant: RunningState: BeforeFixpoint -> ComputeFixpoint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BlockID blocks args -> String
forall a. Show a => a -> String
show BlockID blocks args
block_id String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Position -> Doc Any
forall ann. Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (ProgramLoc -> Position
W4.plSourceLoc ProgramLoc
loc))
      FrameIdentifier
assumption_frame_identifier <- bak -> IO FrameIdentifier
forall sym bak. IsSymBackend sym bak => bak -> IO FrameIdentifier
C.pushAssumptionFrame bak
bak
      let mem_impl :: RegValue sym Mem
mem_impl = case 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) of
                       Just RegValue sym Mem
m -> RegValue sym Mem
m
                       Maybe (RegValue sym Mem)
Nothing -> String -> [String] -> MemImpl sym
forall a. HasCallStack => String -> [String] -> a
C.panic String
"SimpleLoopInvariant.advanceFixpointState"
                                          [String
"LLVM Memory variable not found!"]
      let res_mem_impl :: MemImpl sym
res_mem_impl = RegValue sym Mem
mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" $ C.memImplHeap mem_impl }

--      ?logMessage $ "SimpleLoopInvariant: start memory\n" ++ (show (C.ppMem (C.memImplHeap mem_impl)))

      -- Get a fresh block value that doesn't correspond to any valid memory region
      SymNat sym
havoc_blk <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
W4.natLit sym
sym (Natural -> IO (SymNat sym)) -> IO Natural -> IO (SymNat sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< BlockSource -> IO Natural
C.nextBlock (MemImpl sym -> BlockSource
forall sym. MemImpl sym -> BlockSource
C.memImplBlockSource RegValue sym Mem
MemImpl sym
mem_impl)

      IORef (FixpointState p sym ext rtp blocks)
-> FixpointState p sym ext rtp blocks -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (FixpointState p sym ext rtp blocks)
fixpoint_state_ref (FixpointState p sym ext rtp blocks -> IO ())
-> FixpointState p sym ext rtp blocks -> IO ()
forall a b. (a -> b) -> a -> b
$ FrameIdentifier
-> FixpointRecord p sym ext rtp blocks
-> FixpointState p sym ext rtp blocks
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FrameIdentifier
-> FixpointRecord p sym ext rtp blocks
-> FixpointState p sym ext rtp blocks
ComputeFixpoint FrameIdentifier
assumption_frame_identifier (FixpointRecord p sym ext rtp blocks
 -> FixpointState p sym ext rtp blocks)
-> FixpointRecord p sym ext rtp blocks
-> FixpointState p sym ext rtp blocks
forall a b. (a -> b) -> a -> b
$
        FixpointRecord
        { fixpointBlockId :: BlockID blocks args
fixpointBlockId = BlockID blocks args
block_id
        , fixpointSubstitution :: VariableSubst sym
fixpointSubstitution = MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (Const ()) -> VariableSubst sym
forall sym.
MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (Const ()) -> VariableSubst sym
VarSubst MapF (SymExpr sym) (InvariantEntry sym)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty MapF (SymExpr sym) (Const ())
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 :: MemorySubstitution sym
fixpointMemSubstitution = Map Natural (MemoryBlockData sym) -> MemorySubstitution sym
forall sym.
Map Natural (MemoryBlockData sym) -> MemorySubstitution sym
MemSubst Map Natural (MemoryBlockData sym)
forall a. Monoid a => a
mempty
        , fixpointInitialSimState :: SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
fixpointInitialSimState = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state
        , fixpointImplicitParams :: [Some (SymExpr sym)]
fixpointImplicitParams = []
        , fixpointHavocBlock :: SymNat sym
fixpointHavocBlock = SymNat sym
havoc_blk
        }
      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 FrameIdentifier
assumeFrame FixpointRecord p sym ext rtp blocks
fixpoint_record
      | FixpointRecord { fixpointRegMap :: ()
fixpointRegMap = RegMap sym args
reg_map
                       , fixpointInitialSimState :: ()
fixpointInitialSimState = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
initSimState
                       , fixpointHavocBlock :: forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> SymNat sym
fixpointHavocBlock = SymNat sym
havoc_blk
                       }
           <- FixpointRecord p sym ext rtp 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
"SimpleLoopInvariant: RunningState: ComputeFixpoint: " String -> ShowS
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
assumeFrame

        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
"SimpleLoopInvariant: unsupported memory allocation in loop body."

        -- widen the inductive condition
        ((Assignment (RegEntry sym) args
join_reg_map,MemorySubstitution sym
mem_substitution), VariableSubst sym
join_substitution) <-
            SymNat sym
-> VariableSubst sym
-> FixpointMonad
     sym (Assignment (RegEntry sym) args, MemorySubstitution sym)
-> IO
     ((Assignment (RegEntry sym) args, MemorySubstitution sym),
      VariableSubst sym)
forall sym a.
SymNat sym
-> VariableSubst sym
-> FixpointMonad sym a
-> IO (a, VariableSubst sym)
runFixpointMonad SymNat sym
havoc_blk (FixpointRecord p sym ext rtp blocks -> VariableSubst sym
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> VariableSubst sym
fixpointSubstitution FixpointRecord p sym ext rtp blocks
fixpoint_record) (FixpointMonad
   sym (Assignment (RegEntry sym) args, MemorySubstitution sym)
 -> IO
      ((Assignment (RegEntry sym) args, MemorySubstitution sym),
       VariableSubst sym))
-> FixpointMonad
     sym (Assignment (RegEntry sym) args, MemorySubstitution sym)
-> IO
     ((Assignment (RegEntry sym) args, MemorySubstitution sym),
      VariableSubst sym)
forall a b. (a -> b) -> a -> b
$
               do Assignment (RegEntry sym) args
join_reg_map <- sym
-> Assignment (RegEntry sym) args
-> Assignment (RegEntry sym) args
-> FixpointMonad sym (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))
                  MemorySubstitution sym
mem_substitution <- sym
-> FixpointRecord p sym ext rtp blocks
-> MemWrites sym
-> FixpointMonad sym (MemorySubstitution sym)
forall sym p ext rtp (blocks :: Ctx (Ctx CrucibleType)).
(?logMessage::String -> IO (), IsSymInterface sym,
 IsSymInterface sym) =>
sym
-> FixpointRecord p sym ext rtp blocks
-> MemWrites sym
-> FixpointMonad sym (MemorySubstitution sym)
computeMemSubstitution sym
sym FixpointRecord p sym ext rtp blocks
fixpoint_record MemWrites sym
mem_writes
                  (Assignment (RegEntry sym) args, MemorySubstitution sym)
-> FixpointMonad
     sym (Assignment (RegEntry sym) args, MemorySubstitution sym)
forall a. a -> FixpointMonad sym a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Assignment (RegEntry sym) args
join_reg_map, MemorySubstitution sym
mem_substitution)

        -- 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) (InvariantEntry sym) -> [Some (SymExpr sym)]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Some k2]
MapF.keys (VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
forall sym.
VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
varSubst VariableSubst sym
join_substitution) [Some (SymExpr sym)] -> [Some (SymExpr sym)] -> Bool
forall a. Eq a => a -> a -> Bool
==
           MapF (SymExpr sym) (InvariantEntry sym) -> [Some (SymExpr sym)]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Some k2]
MapF.keys (VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
forall sym.
VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
varSubst (FixpointRecord p sym ext rtp blocks -> VariableSubst sym
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> VariableSubst sym
fixpointSubstitution FixpointRecord p sym ext rtp 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
"SimpleLoopInvariant: RunningState: ComputeFixpoint -> CheckFixpoint "
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Position -> Doc Any
forall ann. Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (ProgramLoc -> Position
W4.plSourceLoc ProgramLoc
loc))
            -- we have delayed populating the main substitution map with
            --  memory variables, so we have to do that now

            MapF (SymExpr sym) (SymExpr sym)
header_mem_substitution <- bak
-> MemImpl sym
-> MemorySubstitution sym
-> IO (MapF (SymExpr sym) (SymExpr sym))
forall sym bak.
(IsSymBackend sym bak, HasPtrWidth 64, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> MemorySubstitution sym
-> IO (MapF (SymExpr sym) (SymExpr sym))
loadMemJoinVariables bak
bak MemImpl sym
header_mem_impl (MemorySubstitution sym -> IO (MapF (SymExpr sym) (SymExpr sym)))
-> MemorySubstitution sym -> IO (MapF (SymExpr sym) (SymExpr sym))
forall a b. (a -> b) -> a -> b
$
              FixpointRecord p sym ext rtp blocks -> MemorySubstitution sym
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> MemorySubstitution sym
fixpointMemSubstitution FixpointRecord p sym ext rtp blocks
fixpoint_record
            MapF (SymExpr sym) (SymExpr sym)
body_mem_substitution <- bak
-> MemImpl sym
-> MemorySubstitution sym
-> IO (MapF (SymExpr sym) (SymExpr sym))
forall sym bak.
(IsSymBackend sym bak, HasPtrWidth 64, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> MemorySubstitution sym
-> IO (MapF (SymExpr sym) (SymExpr sym))
loadMemJoinVariables bak
bak MemImpl sym
body_mem_impl (MemorySubstitution sym -> IO (MapF (SymExpr sym) (SymExpr sym)))
-> MemorySubstitution sym -> IO (MapF (SymExpr sym) (SymExpr sym))
forall a b. (a -> b) -> a -> b
$
              FixpointRecord p sym ext rtp blocks -> MemorySubstitution sym
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> MemorySubstitution sym
fixpointMemSubstitution FixpointRecord p sym ext rtp blocks
fixpoint_record

            -- try to unify widening variables that have the same values
            let (VariableSubst sym
normal_substitution, MapF (SymExpr sym) (SymExpr sym)
equality_substitution) =
                  sym
-> VariableSubst sym
-> (VariableSubst sym, MapF (SymExpr sym) (SymExpr sym))
forall sym.
IsSymInterface sym =>
sym
-> VariableSubst sym
-> (VariableSubst sym, MapF (SymExpr sym) (SymExpr sym))
uninterpretedConstantEqualitySubstitution sym
sym (VariableSubst sym
 -> (VariableSubst sym, MapF (SymExpr sym) (SymExpr sym)))
-> VariableSubst sym
-> (VariableSubst 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 -> VariableSubst sym -> VariableSubst sym
forall sym.
IsSymInterface sym =>
sym -> VariableSubst sym -> VariableSubst sym
filterSubstitution sym
sym (VariableSubst sym -> VariableSubst sym)
-> VariableSubst sym -> VariableSubst sym
forall a b. (a -> b) -> a -> b
$
                  VariableSubst sym
join_substitution
                  { varSubst =
                    MapF.union (varSubst join_substitution) $
                    -- this implements zip, because the two maps have the same keys
                    MapF.intersectWithKeyMaybe
                      (\SymExpr sym tp
_k SymExpr sym tp
x SymExpr sym tp
y -> InvariantEntry sym tp -> Maybe (InvariantEntry sym tp)
forall a. a -> Maybe a
Just (InvariantEntry sym tp -> Maybe (InvariantEntry sym tp))
-> InvariantEntry sym tp -> Maybe (InvariantEntry sym tp)
forall a b. (a -> b) -> a -> b
$ InvariantEntry{ headerValue :: SymExpr sym tp
headerValue = SymExpr sym tp
x, bodyValue :: SymExpr sym tp
bodyValue = SymExpr sym tp
y })
                      header_mem_substitution
                      body_mem_substitution
                  }
--            ?logMessage $ "normal_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList (varSubst normal_substitution))
--            ?logMessage $ "equality_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList equality_substitution)
--            ?logMessage $ "havoc variables: " ++ show (map (\(MapF.Pair x _) -> W4.printSymExpr x) $ MapF.toList (varHavoc normal_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 variables in the memory subst
            MemImpl sym
res_mem_impl <- bak
-> MemImpl sym
-> MemorySubstitution sym
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
forall sym bak.
(IsSymBackend sym bak, HasPtrWidth 64, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> MemorySubstitution sym
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
storeMemJoinVariables
              bak
bak
              MemImpl sym
header_mem_impl
              MemorySubstitution sym
mem_substitution
              MapF (SymExpr sym) (SymExpr sym)
equality_substitution

            -- == compute the list of "implicit parameters" that are relevant ==
            let implicit_params :: [Some (SymExpr sym)]
implicit_params = Set (Some (SymExpr sym)) -> [Some (SymExpr sym)]
forall a. Set a -> [a]
Set.toList (Set (Some (SymExpr sym)) -> [Some (SymExpr sym)])
-> Set (Some (SymExpr sym)) -> [Some (SymExpr sym)]
forall a b. (a -> b) -> a -> b
$
                  Set (Some (SymExpr sym))
-> Set (Some (SymExpr sym)) -> Set (Some (SymExpr sym))
forall a. Ord a => Set a -> Set a -> Set a
Set.difference
                    ((Pair (SymExpr sym) (InvariantEntry sym)
 -> Set (Some (SymExpr sym)))
-> [Pair (SymExpr sym) (InvariantEntry sym)]
-> Set (Some (SymExpr sym))
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
                       (\ (MapF.Pair SymExpr sym tp
_ InvariantEntry sym tp
e) ->
                            -- filter out the special "noSatisfyingWrite" boolean constants
                            -- that are generated as part of the LLVM memory model
                            (Some (SymExpr sym) -> Bool)
-> Set (Some (SymExpr sym)) -> Set (Some (SymExpr sym))
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ( \ (C.Some SymExpr sym x
x) ->
                                           Bool -> Bool
not (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf String
"cnoSatisfyingWrite"
                                                (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 x -> 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 x
x))) (Set (Some (SymExpr sym)) -> Set (Some (SymExpr sym)))
-> Set (Some (SymExpr sym)) -> Set (Some (SymExpr sym))
forall a b. (a -> b) -> a -> b
$
                            (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 (\ (C.Some BoundVar sym x
x) -> SymExpr sym x -> Some (SymExpr sym)
forall k (f :: k -> Type) (x :: k). f x -> Some f
C.Some (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
x)) (Set (Some (BoundVar sym)) -> Set (Some (SymExpr sym)))
-> Set (Some (BoundVar sym)) -> Set (Some (SymExpr sym))
forall a b. (a -> b) -> a -> b
$
                              (sym -> SymExpr sym tp -> 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 (InvariantEntry sym tp -> SymExpr sym tp
forall sym (tp :: BaseType).
InvariantEntry sym tp -> SymExpr sym tp
bodyValue InvariantEntry sym tp
e)))
                       (MapF (SymExpr sym) (InvariantEntry sym)
-> [Pair (SymExpr sym) (InvariantEntry sym)]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Pair k2 a]
MapF.toList (VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
forall sym.
VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
varSubst VariableSubst sym
normal_substitution)))
                    ([Some (SymExpr sym)] -> Set (Some (SymExpr sym))
forall a. Ord a => [a] -> Set a
Set.fromList (MapF (SymExpr sym) (InvariantEntry sym) -> [Some (SymExpr sym)]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Some k2]
MapF.keys (VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
forall sym.
VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
varSubst VariableSubst sym
normal_substitution)))

            ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
              [String
"Implicit parameters!"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
              (Some (SymExpr sym) -> String) -> [Some (SymExpr sym)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (C.Some SymExpr sym x
x) -> Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym x -> 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 x
x)) [Some (SymExpr sym)]
implicit_params

            -- == assert the loop invariant on the initial values ==

            -- build a map where the current value is equal to the initial value
            let init_state_map :: MapF (SymExpr sym) (InvariantEntry sym)
init_state_map = (forall (tp :: BaseType).
 InvariantEntry sym tp -> InvariantEntry sym tp)
-> MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (InvariantEntry sym)
forall {v} (f :: v -> Type) (g :: v -> Type) (ktp :: v -> Type).
(forall (tp :: v). f tp -> g tp) -> MapF ktp f -> MapF ktp g
MapF.map (\InvariantEntry sym tp
e -> InvariantEntry sym tp
e{ bodyValue = headerValue e })
                                          (VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
forall sym.
VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
varSubst VariableSubst sym
normal_substitution)
            -- construct the loop invariant
            Pred sym
initial_loop_invariant <- InvariantPhase
-> [Some (SymExpr sym)]
-> MapF (SymExpr sym) (InvariantEntry sym)
-> IO (Pred sym)
loop_invariant InvariantPhase
InitialInvariant [Some (SymExpr sym)]
implicit_params MapF (SymExpr sym) (InvariantEntry sym)
init_state_map
            -- assert the loop invariant as an obligation
            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
initial_loop_invariant
               (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
"initial loop invariant"

            -- == assume the loop invariant on the arbitrary state ==

            -- build a map where the current value is equal to the widening variable
            let hyp_state_map :: MapF (SymExpr sym) (InvariantEntry sym)
hyp_state_map = (forall (tp :: BaseType).
 SymExpr sym tp -> InvariantEntry sym tp -> InvariantEntry sym tp)
-> MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (InvariantEntry 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
k InvariantEntry sym tp
e -> InvariantEntry sym tp
e{ bodyValue = k })
                                                (VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
forall sym.
VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
varSubst VariableSubst sym
normal_substitution)
            -- construct the loop invariant to assume at the loop head
            Pred sym
hypothetical_loop_invariant <- InvariantPhase
-> [Some (SymExpr sym)]
-> MapF (SymExpr sym) (InvariantEntry sym)
-> IO (Pred sym)
loop_invariant InvariantPhase
HypotheticalInvariant [Some (SymExpr sym)]
implicit_params MapF (SymExpr sym) (InvariantEntry sym)
hyp_state_map
            -- assume the loop invariant
            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
"loop head invariant"
                Pred sym
hypothetical_loop_invariant

            -- == set up the state with arbitrary values to run the loop body ==

            IORef (FixpointState p sym ext rtp blocks)
-> FixpointState p sym ext rtp blocks -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (FixpointState p sym ext rtp blocks)
fixpoint_state_ref (FixpointState p sym ext rtp blocks -> IO ())
-> FixpointState p sym ext rtp blocks -> IO ()
forall a b. (a -> b) -> a -> b
$
              FixpointRecord p sym ext rtp blocks
-> FixpointState p sym ext rtp blocks
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks
-> FixpointState p sym ext rtp blocks
CheckFixpoint
                FixpointRecord
                { fixpointBlockId :: BlockID blocks args
fixpointBlockId = BlockID blocks args
block_id
                , fixpointSubstitution :: VariableSubst sym
fixpointSubstitution = VariableSubst 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
Assignment (RegEntry sym) args
res_reg_map
                , fixpointMemSubstitution :: MemorySubstitution sym
fixpointMemSubstitution = MemorySubstitution sym
mem_substitution
                , fixpointInitialSimState :: SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
fixpointInitialSimState = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
initSimState
                , fixpointImplicitParams :: [Some (SymExpr sym)]
fixpointImplicitParams = [Some (SymExpr sym)]
implicit_params
                , fixpointHavocBlock :: SymNat sym
fixpointHavocBlock = SymNat sym
havoc_blk
                }

            -- Continue running from the loop header starting from an arbitrary state satisfying
            -- the loop invariant.
            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)
initSimState 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
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))
(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
            -- Otherwise, we are still working on finding all the loop-carried dependencies
            ?logMessage::String -> IO ()
String -> IO ()
?logMessage (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
              String
"SimpleLoopInvariant: RunningState: ComputeFixpoint: -> ComputeFixpoint"
            FrameIdentifier
assumption_frame_identifier <- bak -> IO FrameIdentifier
forall sym bak. IsSymBackend sym bak => bak -> IO FrameIdentifier
C.pushAssumptionFrame bak
bak

            -- write any new widening variables into memory state
            MemImpl sym
res_mem_impl <- bak
-> MemImpl sym
-> MemorySubstitution sym
-> MapF (SymExpr sym) (SymExpr sym)
-> IO (MemImpl sym)
forall sym bak.
(IsSymBackend sym bak, HasPtrWidth 64, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> MemorySubstitution sym
-> 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) })
              MemorySubstitution sym
mem_substitution
              MapF (SymExpr sym) (SymExpr sym)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty

            IORef (FixpointState p sym ext rtp blocks)
-> FixpointState p sym ext rtp blocks -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (FixpointState p sym ext rtp blocks)
fixpoint_state_ref (FixpointState p sym ext rtp blocks -> IO ())
-> FixpointState p sym ext rtp blocks -> IO ()
forall a b. (a -> b) -> a -> b
$
              FrameIdentifier
-> FixpointRecord p sym ext rtp blocks
-> FixpointState p sym ext rtp blocks
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FrameIdentifier
-> FixpointRecord p sym ext rtp blocks
-> FixpointState p sym ext rtp blocks
ComputeFixpoint FrameIdentifier
assumption_frame_identifier (FixpointRecord p sym ext rtp blocks
 -> FixpointState p sym ext rtp blocks)
-> FixpointRecord p sym ext rtp blocks
-> FixpointState p sym ext rtp blocks
forall a b. (a -> b) -> a -> b
$
              FixpointRecord
              { fixpointBlockId :: BlockID blocks args
fixpointBlockId = BlockID blocks args
block_id
              , fixpointSubstitution :: VariableSubst sym
fixpointSubstitution = VariableSubst 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
Assignment (RegEntry sym) args
join_reg_map
              , fixpointMemSubstitution :: MemorySubstitution sym
fixpointMemSubstitution = MemorySubstitution sym
mem_substitution
              , fixpointInitialSimState :: SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
fixpointInitialSimState = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
initSimState
              , fixpointImplicitParams :: [Some (SymExpr sym)]
fixpointImplicitParams = []
              , fixpointHavocBlock :: SymNat sym
fixpointHavocBlock = SymNat sym
havoc_blk
              }
            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)
initSimState 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
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))
(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
"SimpleLoopInvariant.simpleLoopInvariant" [String
"type mismatch: ComputeFixpoint"]

    CheckFixpoint FixpointRecord p sym ext rtp blocks
fixpoint_record
      | FixpointRecord { fixpointRegMap :: ()
fixpointRegMap = RegMap sym args
reg_map } <- FixpointRecord p sym ext rtp 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
"SimpleLoopInvariant: RunningState: "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"CheckFixpoint"
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"AfterFixpoint"
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ BlockID blocks args -> String
forall a. Show a => a -> String
show BlockID blocks args
block_id
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Position -> Doc Any
forall ann. Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (ProgramLoc -> Position
W4.plSourceLoc ProgramLoc
loc))

        -- == assert the loop invariant and abort ==

        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)

        MapF (SymExpr sym) (SymExpr sym)
body_mem_substitution <- bak
-> MemImpl sym
-> MemorySubstitution sym
-> IO (MapF (SymExpr sym) (SymExpr sym))
forall sym bak.
(IsSymBackend sym bak, HasPtrWidth 64, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> MemorySubstitution sym
-> IO (MapF (SymExpr sym) (SymExpr sym))
loadMemJoinVariables bak
bak MemImpl sym
body_mem_impl (MemorySubstitution sym -> IO (MapF (SymExpr sym) (SymExpr sym)))
-> MemorySubstitution sym -> IO (MapF (SymExpr sym) (SymExpr sym))
forall a b. (a -> b) -> a -> b
$ FixpointRecord p sym ext rtp blocks -> MemorySubstitution sym
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> MemorySubstitution sym
fixpointMemSubstitution FixpointRecord p sym ext rtp blocks
fixpoint_record
        let res_substitution :: MapF (SymExpr sym) (InvariantEntry sym)
res_substitution = (forall (tp :: BaseType).
 SymExpr sym tp -> InvariantEntry sym tp -> InvariantEntry sym tp)
-> MapF (SymExpr sym) (InvariantEntry sym)
-> MapF (SymExpr sym) (InvariantEntry 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 InvariantEntry sym tp
fixpoint_entry ->
                InvariantEntry sym tp
fixpoint_entry
                  { bodyValue = MapF.findWithDefault (bodyValue fixpoint_entry) variable body_mem_substitution
                  })
              (VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
forall sym.
VariableSubst sym -> MapF (SymExpr sym) (InvariantEntry sym)
varSubst (FixpointRecord p sym ext rtp blocks -> VariableSubst sym
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> VariableSubst sym
fixpointSubstitution FixpointRecord p sym ext rtp blocks
fixpoint_record))
        -- ?logMessage $ "res_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList res_substitution)

        Pred sym
invariant_pred <- InvariantPhase
-> [Some (SymExpr sym)]
-> MapF (SymExpr sym) (InvariantEntry sym)
-> IO (Pred sym)
loop_invariant InvariantPhase
InductiveInvariant (FixpointRecord p sym ext rtp blocks -> [Some (SymExpr sym)]
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> [Some (SymExpr sym)]
fixpointImplicitParams FixpointRecord p sym ext rtp blocks
fixpoint_record) MapF (SymExpr sym) (InvariantEntry sym)
res_substitution
        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
invariant_pred (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
"loop invariant"
        -- ?logMessage $ "fixpoint_func_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList fixpoint_func_substitution)
        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
$ AbortExecReason
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> SimState p sym ext rtp f a -> ExecState p sym ext rtp
C.AbortState (ProgramLoc -> AbortExecReason
C.InfeasibleBranch ProgramLoc
loc) SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
sim_state

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



constructMemSubstitutionCandidate :: forall sym.
  (?logMessage :: String -> IO (), C.IsSymInterface sym) =>
  C.IsSymInterface sym =>
  sym ->
  C.MemWrites sym ->
  IO (MemorySubstitution sym)
constructMemSubstitutionCandidate :: forall sym.
(?logMessage::String -> IO (), IsSymInterface sym,
 IsSymInterface sym) =>
sym -> MemWrites sym -> IO (MemorySubstitution sym)
constructMemSubstitutionCandidate sym
sym MemWrites sym
mem_writes =
  case MemWrites sym
mem_writes of
    C.MemWrites [C.MemWritesChunkIndexed IntMap [MemWrite sym]
mmm] ->
      Map Natural (MemoryBlockData sym) -> MemorySubstitution sym
forall sym.
Map Natural (MemoryBlockData sym) -> MemorySubstitution sym
MemSubst (Map Natural (MemoryBlockData sym) -> MemorySubstitution sym)
-> IO (Map Natural (MemoryBlockData sym))
-> IO (MemorySubstitution sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Map Natural (MemoryBlockData sym)
 -> MemWrite sym -> IO (Map Natural (MemoryBlockData sym)))
-> Map Natural (MemoryBlockData sym)
-> [MemWrite sym]
-> IO (Map Natural (MemoryBlockData sym))
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Map Natural (MemoryBlockData sym)
-> MemWrite sym -> IO (Map Natural (MemoryBlockData sym))
handleMemWrite Map Natural (MemoryBlockData sym)
forall a. Monoid a => a
mempty ([[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)

    -- no writes occured in the body of the loop
    C.MemWrites [] ->
      MemorySubstitution sym -> IO (MemorySubstitution sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Map Natural (MemoryBlockData sym) -> MemorySubstitution sym
forall sym.
Map Natural (MemoryBlockData sym) -> MemorySubstitution sym
MemSubst Map Natural (MemoryBlockData sym)
forall a. Monoid a => a
mempty)

    MemWrites sym
_ -> String -> IO (MemorySubstitution sym)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (MemorySubstitution sym))
-> String -> IO (MemorySubstitution sym)
forall a b. (a -> b) -> a -> b
$ String
"SimpleLoopInvariant: not MemWritesChunkIndexed: " String -> ShowS
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)

 where
   updateOffsetMap ::
     Natural ->
     W4.SymBV sym 64 ->
     C.LLVMPtr sym 64 ->
     C.StorageType ->
     Map Natural (MemoryRegion sym) ->
     IO (Map Natural (MemoryRegion sym))
   updateOffsetMap :: Natural
-> SymBV sym 64
-> LLVMPtr sym 64
-> StorageType
-> Map Natural (MemoryRegion sym)
-> IO (Map Natural (MemoryRegion sym))
updateOffsetMap Natural
blk SymBV sym 64
basePtr LLVMPtr sym 64
ptr StorageType
storage_type Map Natural (MemoryRegion sym)
off_map =
     do SymBV sym 64
diff <- sym -> SymBV sym 64 -> SymBV sym 64 -> IO (SymBV sym 64)
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 (LLVMPtr sym 64 -> SymBV sym 64
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset LLVMPtr sym 64
ptr) SymBV sym 64
basePtr
        case SymBV sym 64 -> Maybe (BV 64)
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 64
diff of
          Maybe (BV 64)
Nothing ->
            String -> IO (Map Natural (MemoryRegion sym))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (Map Natural (MemoryRegion sym)))
-> String -> IO (Map Natural (MemoryRegion sym))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
              [ String
"SimpleLoopInvariant: incompatible base pointers for writes to a memory region " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
blk
              , Doc Any -> String
forall a. Show a => a -> String
show (SymBV sym 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 SymBV sym 64
basePtr)
              , Doc Any -> String
forall a. Show a => a -> String
show (SymBV sym 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 -> SymBV sym 64
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset LLVMPtr sym 64
ptr))
              ]
          Just BV 64
off ->
            do let sz :: Bytes
sz = Bytes -> StorageType -> Bytes
C.typeEnd Bytes
0 StorageType
storage_type
               case Natural
-> Map Natural (MemoryRegion sym) -> Maybe (MemoryRegion sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (BV 64 -> Natural
forall (w :: Natural). BV w -> Natural
BV.asNatural BV 64
off) Map Natural (MemoryRegion sym)
off_map of
                 Just MemoryRegion sym
rgn
                   | MemoryRegion sym -> Bytes
forall sym. MemoryRegion sym -> Bytes
regionSize MemoryRegion sym
rgn Bytes -> Bytes -> Bool
forall a. Eq a => a -> a -> Bool
== Bytes
sz -> Map Natural (MemoryRegion sym)
-> IO (Map Natural (MemoryRegion sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Map Natural (MemoryRegion sym)
off_map
                   | Bool
otherwise ->
                       String -> IO (Map Natural (MemoryRegion sym))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (Map Natural (MemoryRegion sym)))
-> String -> IO (Map Natural (MemoryRegion sym))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                         [ String
"Memory region written at incompatible storage types"
                         , StorageType -> String
forall a. Show a => a -> String
show (MemoryRegion sym -> StorageType
forall sym. MemoryRegion sym -> StorageType
regionStorage MemoryRegion sym
rgn) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" vs" String -> ShowS
forall a. [a] -> [a] -> [a]
++ StorageType -> String
forall a. Show a => a -> String
show StorageType
storage_type
                         , Doc Any -> String
forall a. Show a => a -> String
show (LLVMPtr sym 64 -> Doc Any
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
C.ppPtr LLVMPtr sym 64
ptr)
                         ]
                 Maybe (MemoryRegion sym)
Nothing ->
                   case Natural -> Some NatRepr
W4.mkNatRepr (Natural -> Some NatRepr) -> Natural -> Some NatRepr
forall a b. (a -> b) -> a -> b
$ Bytes -> Natural
C.bytesToBits Bytes
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_var <- 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
W4.safeSymbol (String
"mem_join_var_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
blk String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show (BV 64 -> Natural
forall (w :: Natural). BV w -> Natural
BV.asNatural BV 64
off)))
                           (NatRepr x -> BaseTypeRepr ('BaseBVType x)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr NatRepr x
bv_width)
                         let rgn :: MemoryRegion sym
rgn = MemoryRegion
                                   { regionOffset :: BV 64
regionOffset  = BV 64
off
                                   , regionSize :: Bytes
regionSize    = Bytes
sz
                                   , regionStorage :: StorageType
regionStorage = StorageType
storage_type
                                   , regionJoinVar :: SymExpr sym ('BaseBVType x)
regionJoinVar = SymExpr sym ('BaseBVType x)
join_var
                                   }
                         Map Natural (MemoryRegion sym)
-> IO (Map Natural (MemoryRegion sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Natural
-> MemoryRegion sym
-> Map Natural (MemoryRegion sym)
-> Map Natural (MemoryRegion sym)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (BV 64 -> Natural
forall (w :: Natural). BV w -> Natural
BV.asNatural BV 64
off) MemoryRegion sym
rgn Map Natural (MemoryRegion sym)
off_map)

                       | Bool
otherwise ->
                         String -> [String] -> IO (Map Natural (MemoryRegion sym))
forall a. HasCallStack => String -> [String] -> a
C.panic
                           String
"SimpleLoopInvariant.simpleLoopInvariant"
                           [String
"unexpected storage type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StorageType -> String
forall a. Show a => a -> String
show StorageType
storage_type String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" of size " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bytes -> String
forall a. Show a => a -> String
show Bytes
sz]


   handleMemWrite :: Map Natural (MemoryBlockData sym)
-> MemWrite sym -> IO (Map Natural (MemoryBlockData sym))
handleMemWrite Map Natural (MemoryBlockData sym)
mem_subst MemWrite sym
wr =
     case MemWrite sym
wr of
       C.MemWrite LLVMPtr sym w
ptr (C.MemArrayStore SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
_arr (Just SymBV sym w
len))
         | 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)
testEquality (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64) (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
len)
         -> case Natural
-> Map Natural (MemoryBlockData sym) -> Maybe (MemoryBlockData sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Natural
blk Map Natural (MemoryBlockData sym)
mem_subst of
              Just (ArrayBlock SymExpr sym ArrayTp
_ SymBV sym 64
_) -> Map Natural (MemoryBlockData sym)
-> IO (Map Natural (MemoryBlockData sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Map Natural (MemoryBlockData sym)
mem_subst
              Just (RegularBlock SymBV sym 64
_ Map Natural (MemoryRegion sym)
_) ->
                String -> IO (Map Natural (MemoryBlockData sym))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (Map Natural (MemoryBlockData sym)))
-> String -> IO (Map Natural (MemoryBlockData sym))
forall a b. (a -> b) -> a -> b
$
                  String
"SimpleLoopInvariant: incompatible writes detected for block " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
blk
              Maybe (MemoryBlockData sym)
Nothing ->
                do SymExpr sym ArrayTp
join_var <- IO (SymExpr sym ArrayTp) -> IO (SymExpr sym ArrayTp)
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ArrayTp) -> IO (SymExpr sym ArrayTp))
-> IO (SymExpr sym ArrayTp) -> IO (SymExpr sym ArrayTp)
forall a b. (a -> b) -> a -> b
$
                       sym
-> SolverSymbol -> BaseTypeRepr ArrayTp -> IO (SymExpr sym ArrayTp)
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
W4.safeSymbol (String
"smt_array_join_var_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
blk))
                         BaseTypeRepr ArrayTp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
                   Map Natural (MemoryBlockData sym)
-> IO (Map Natural (MemoryBlockData sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Natural
-> MemoryBlockData sym
-> Map Natural (MemoryBlockData sym)
-> Map Natural (MemoryBlockData sym)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Natural
blk (SymExpr sym ArrayTp -> SymBV sym 64 -> MemoryBlockData sym
forall sym.
SymExpr sym ArrayTp -> SymBV sym 64 -> MemoryBlockData sym
ArrayBlock SymExpr sym ArrayTp
join_var SymBV sym w
SymBV sym 64
len) Map Natural (MemoryBlockData sym)
mem_subst)

       C.MemWrite LLVMPtr sym w
ptr (C.MemStore LLVMVal sym
_val StorageType
storage_type Alignment
_align)
        | 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)
testEquality (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64) (SymExpr sym (BaseBVType 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 (LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset LLVMPtr sym w
ptr))
        -> do (SymBV sym 64
basePtr, Map Natural (MemoryRegion sym)
off_map) <-
                case Natural
-> Map Natural (MemoryBlockData sym) -> Maybe (MemoryBlockData sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Natural
blk Map Natural (MemoryBlockData sym)
mem_subst of
                  Just (ArrayBlock SymExpr sym ArrayTp
_ SymBV sym 64
_) ->
                     String -> IO (SymBV sym 64, Map Natural (MemoryRegion sym))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (SymBV sym 64, Map Natural (MemoryRegion sym)))
-> String -> IO (SymBV sym 64, Map Natural (MemoryRegion sym))
forall a b. (a -> b) -> a -> b
$
                       String
"SimpleLoopInvariant: incompatible writes detected for block " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                       Natural -> String
forall a. Show a => a -> String
show Natural
blk
                  Just (RegularBlock SymBV sym 64
basePtr Map Natural (MemoryRegion sym)
off_map) -> (SymBV sym 64, Map Natural (MemoryRegion sym))
-> IO (SymBV sym 64, Map Natural (MemoryRegion sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymBV sym 64
basePtr, Map Natural (MemoryRegion sym)
off_map)
                  Maybe (MemoryBlockData sym)
Nothing -> (SymBV sym 64, Map Natural (MemoryRegion sym))
-> IO (SymBV sym 64, Map Natural (MemoryRegion sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMPtr sym 64 -> SymBV sym 64
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
C.llvmPointerOffset LLVMPtr sym w
LLVMPtr sym 64
ptr, Map Natural (MemoryRegion sym)
forall a. Monoid a => a
mempty)

              Map Natural (MemoryRegion sym)
off_map' <- Natural
-> SymBV sym 64
-> LLVMPtr sym 64
-> StorageType
-> Map Natural (MemoryRegion sym)
-> IO (Map Natural (MemoryRegion sym))
updateOffsetMap Natural
blk SymBV sym 64
basePtr LLVMPtr sym w
LLVMPtr sym 64
ptr StorageType
storage_type Map Natural (MemoryRegion sym)
off_map
              Map Natural (MemoryBlockData sym)
-> IO (Map Natural (MemoryBlockData sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Natural
-> MemoryBlockData sym
-> Map Natural (MemoryBlockData sym)
-> Map Natural (MemoryBlockData sym)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Natural
blk (SymBV sym 64
-> Map Natural (MemoryRegion sym) -> MemoryBlockData sym
forall sym.
SymBV sym 64
-> Map Natural (MemoryRegion sym) -> MemoryBlockData sym
RegularBlock SymBV sym 64
basePtr Map Natural (MemoryRegion sym)
off_map') Map Natural (MemoryBlockData sym)
mem_subst)

       MemWrite sym
w -> String -> IO (Map Natural (MemoryBlockData sym))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (Map Natural (MemoryBlockData sym)))
-> String -> IO (Map Natural (MemoryBlockData sym))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
              [ String
"SimpleLoopInvariant: unable to handle memory write of the form:"
              , Doc Any -> String
forall a. Show a => a -> String
show (MemWrite sym -> Doc Any
forall sym ann. IsExpr (SymExpr sym) => MemWrite sym -> Doc ann
C.ppWrite MemWrite sym
w)
              ]

computeMemSubstitution ::
  (?logMessage :: String -> IO (), C.IsSymInterface sym) =>
  C.IsSymInterface sym =>
  sym ->
  FixpointRecord p sym ext rtp blocks ->
  C.MemWrites sym ->
  FixpointMonad sym (MemorySubstitution sym)
computeMemSubstitution :: forall sym p ext rtp (blocks :: Ctx (Ctx CrucibleType)).
(?logMessage::String -> IO (), IsSymInterface sym,
 IsSymInterface sym) =>
sym
-> FixpointRecord p sym ext rtp blocks
-> MemWrites sym
-> FixpointMonad sym (MemorySubstitution sym)
computeMemSubstitution sym
sym FixpointRecord p sym ext rtp blocks
fixpoint_record MemWrites sym
mem_writes =
 let ?ptrWidth = forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64 in
 do -- widen the memory
    MemorySubstitution sym
mem_subst_candidate <- IO (MemorySubstitution sym)
-> FixpointMonad sym (MemorySubstitution sym)
forall a. IO a -> FixpointMonad sym a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MemorySubstitution sym)
 -> FixpointMonad sym (MemorySubstitution sym))
-> IO (MemorySubstitution sym)
-> FixpointMonad sym (MemorySubstitution sym)
forall a b. (a -> b) -> a -> b
$ sym -> MemWrites sym -> IO (MemorySubstitution sym)
forall sym.
(?logMessage::String -> IO (), IsSymInterface sym,
 IsSymInterface sym) =>
sym -> MemWrites sym -> IO (MemorySubstitution sym)
constructMemSubstitutionCandidate sym
sym MemWrites sym
mem_writes

    -- Check the candidate and raise errors if we cannot handle the resulting widening
    Either String (MemorySubstitution sym)
res <- IO (Either String (MemorySubstitution sym))
-> FixpointMonad sym (Either String (MemorySubstitution sym))
forall a. IO a -> FixpointMonad sym a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (Either String (MemorySubstitution sym))
 -> FixpointMonad sym (Either String (MemorySubstitution sym)))
-> IO (Either String (MemorySubstitution sym))
-> FixpointMonad sym (Either String (MemorySubstitution sym))
forall a b. (a -> b) -> a -> b
$ ExceptT String IO (MemorySubstitution sym)
-> IO (Either String (MemorySubstitution sym))
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT String IO (MemorySubstitution sym)
 -> IO (Either String (MemorySubstitution sym)))
-> ExceptT String IO (MemorySubstitution sym)
-> IO (Either String (MemorySubstitution sym))
forall a b. (a -> b) -> a -> b
$
             sym
-> MemorySubstitution sym
-> MemorySubstitution sym
-> ExceptT String IO (MemorySubstitution sym)
forall sym.
IsSymExprBuilder sym =>
sym
-> MemorySubstitution sym
-> MemorySubstitution sym
-> ExceptT String IO (MemorySubstitution sym)
checkMemSubst sym
sym (FixpointRecord p sym ext rtp blocks -> MemorySubstitution sym
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType)).
FixpointRecord p sym ext rtp blocks -> MemorySubstitution sym
fixpointMemSubstitution FixpointRecord p sym ext rtp blocks
fixpoint_record)
                               MemorySubstitution sym
mem_subst_candidate

    case Either String (MemorySubstitution sym)
res of
      Left String
msg -> String -> FixpointMonad sym (MemorySubstitution sym)
forall a. String -> FixpointMonad sym a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> FixpointMonad sym (MemorySubstitution sym))
-> String -> FixpointMonad sym (MemorySubstitution sym)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
        [ String
"SimpleLoopInvariant: failure constructing memory footprint for loop invariant"
        , String
msg
        ]
      Right MemorySubstitution sym
x  -> MemorySubstitution sym
-> FixpointMonad sym (MemorySubstitution sym)
forall a. a -> FixpointMonad sym a
forall (m :: Type -> Type) a. Monad m => a -> m a
return MemorySubstitution sym
x


-- | This function checks that the computed candidate memory substitution is an acceptable
--   refinement of the original. For the moment, this is a very restrictive test; either
--   we have started with an empty substitution (e.g., on the first iteration), or we have
--   computed a substitution that is exactly compatible with the one we started with.
--
--   At some point, it may be necessary or desirable to allow more.
--
--   Note:, for this check we do not need to compare the identities of the actual join variables
--   found in the substitution, just that the memory regions (positions and sizes) are equal.
checkMemSubst :: forall sym.
  W4.IsSymExprBuilder sym =>
  sym ->
  MemorySubstitution sym ->
  MemorySubstitution sym ->
  ExceptT String IO (MemorySubstitution sym)
checkMemSubst :: forall sym.
IsSymExprBuilder sym =>
sym
-> MemorySubstitution sym
-> MemorySubstitution sym
-> ExceptT String IO (MemorySubstitution sym)
checkMemSubst sym
sym MemorySubstitution sym
orig MemorySubstitution sym
candidate =
  if Map Natural (MemoryBlockData sym) -> Bool
forall k a. Map k a -> Bool
Map.null (MemorySubstitution sym -> Map Natural (MemoryBlockData sym)
forall sym.
MemorySubstitution sym -> Map Natural (MemoryBlockData sym)
memSubst MemorySubstitution sym
orig)
    then MemorySubstitution sym
-> ExceptT String IO (MemorySubstitution sym)
forall a. a -> ExceptT String IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return MemorySubstitution sym
candidate
    else do ExceptT String IO ()
checkCandidateEqual
            MemorySubstitution sym
-> ExceptT String IO (MemorySubstitution sym)
forall a. a -> ExceptT String IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return MemorySubstitution sym
orig

 where
   checkEqualMaps :: String -> (t -> t -> t -> m b) -> Map t t -> Map t t -> m ()
checkEqualMaps String
str t -> t -> t -> m b
f Map t t
m1 Map t t
m2 =
     do Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (Map t t -> Set t
forall k a. Map k a -> Set k
Map.keysSet Map t t
m1 Set t -> Set t -> Bool
forall a. Eq a => a -> a -> Bool
== Map t t -> Set t
forall k a. Map k a -> Set k
Map.keysSet Map t t
m2)
               (String -> m ()
forall a. String -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String
"Key sets differ when checking " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str))
        [(t, t)] -> ((t, t) -> m b) -> m ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map t t -> [(t, t)]
forall k a. Map k a -> [(k, a)]
Map.assocs Map t t
m1) (((t, t) -> m b) -> m ()) -> ((t, t) -> m b) -> m ()
forall a b. (a -> b) -> a -> b
$ \ (t
k,t
e1) ->
               case t -> Map t t -> Maybe t
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup t
k Map t t
m2 of
                 Just t
e2 -> t -> t -> t -> m b
f t
k t
e1 t
e2
                 Maybe t
Nothing -> String -> m b
forall a. String -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String
"Key sets differ when checking " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str)

   checkCandidateEqual :: ExceptT String IO ()
checkCandidateEqual =
     String
-> (Natural
    -> MemoryBlockData sym
    -> MemoryBlockData sym
    -> ExceptT String IO ())
-> Map Natural (MemoryBlockData sym)
-> Map Natural (MemoryBlockData sym)
-> ExceptT String IO ()
forall {t} {m :: Type -> Type} {t} {t} {b}.
(MonadError String m, Ord t) =>
String -> (t -> t -> t -> m b) -> Map t t -> Map t t -> m ()
checkEqualMaps String
"memory substitution" Natural
-> MemoryBlockData sym
-> MemoryBlockData sym
-> ExceptT String IO ()
checkMBD
       (MemorySubstitution sym -> Map Natural (MemoryBlockData sym)
forall sym.
MemorySubstitution sym -> Map Natural (MemoryBlockData sym)
memSubst MemorySubstitution sym
orig) (MemorySubstitution sym -> Map Natural (MemoryBlockData sym)
forall sym.
MemorySubstitution sym -> Map Natural (MemoryBlockData sym)
memSubst MemorySubstitution sym
candidate)

   checkBVEq :: (1 <= w) => W4.SymBV sym w -> W4.SymBV sym w -> IO Bool
   checkBVEq :: forall (w :: Natural).
(1 <= w) =>
SymBV sym w -> SymBV sym w -> IO Bool
checkBVEq SymBV sym w
x SymBV sym w
y =
      do SymBV sym w
diff <- 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.bvSub sym
sym SymBV sym w
x SymBV sym w
y
         case BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned (BV w -> Integer) -> Maybe (BV w) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym 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 SymBV sym w
diff of
           Just Integer
0 -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
True
           Maybe Integer
_      -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
False

   checkMBD :: Natural
-> MemoryBlockData sym
-> MemoryBlockData sym
-> ExceptT String IO ()
checkMBD Natural
n (RegularBlock SymBV sym 64
b1 Map Natural (MemoryRegion sym)
rmap1) (RegularBlock SymBV sym 64
b2 Map Natural (MemoryRegion sym)
rmap2) =
      do Bool
ok <- IO Bool -> ExceptT String IO Bool
forall a. IO a -> ExceptT String IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> ExceptT String IO Bool)
-> IO Bool -> ExceptT String IO Bool
forall a b. (a -> b) -> a -> b
$ SymBV sym 64 -> SymBV sym 64 -> IO Bool
forall (w :: Natural).
(1 <= w) =>
SymBV sym w -> SymBV sym w -> IO Bool
checkBVEq SymBV sym 64
b1 SymBV sym 64
b2
         Bool -> ExceptT String IO () -> ExceptT String IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless Bool
ok (ExceptT String IO () -> ExceptT String IO ())
-> ExceptT String IO () -> ExceptT String IO ()
forall a b. (a -> b) -> a -> b
$ String -> ExceptT String IO ()
forall a. String -> ExceptT String IO a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO ()) -> String -> ExceptT String IO ()
forall a b. (a -> b) -> a -> b
$
               [String] -> String
unlines  [String
"base pointers differ for region " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n
                        , Doc Any -> String
forall a. Show a => a -> String
show (SymBV sym 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 SymBV sym 64
b1)
                        , Doc Any -> String
forall a. Show a => a -> String
show (SymBV sym 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 SymBV sym 64
b2)
                        ]
         String
-> (Natural
    -> MemoryRegion sym -> MemoryRegion sym -> ExceptT String IO ())
-> Map Natural (MemoryRegion sym)
-> Map Natural (MemoryRegion sym)
-> ExceptT String IO ()
forall {t} {m :: Type -> Type} {t} {t} {b}.
(MonadError String m, Ord t) =>
String -> (t -> t -> t -> m b) -> Map t t -> Map t t -> m ()
checkEqualMaps (String
"region map for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n) (Natural
-> Natural
-> MemoryRegion sym
-> MemoryRegion sym
-> ExceptT String IO ()
checkMemRegion Natural
n) Map Natural (MemoryRegion sym)
rmap1 Map Natural (MemoryRegion sym)
rmap2
   checkMBD Natural
n (ArrayBlock SymExpr sym ArrayTp
_a1 SymBV sym 64
l1) (ArrayBlock SymExpr sym ArrayTp
_a2 SymBV sym 64
l2) =
      do Bool
ok <- IO Bool -> ExceptT String IO Bool
forall a. IO a -> ExceptT String IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> ExceptT String IO Bool)
-> IO Bool -> ExceptT String IO Bool
forall a b. (a -> b) -> a -> b
$ SymBV sym 64 -> SymBV sym 64 -> IO Bool
forall (w :: Natural).
(1 <= w) =>
SymBV sym w -> SymBV sym w -> IO Bool
checkBVEq SymBV sym 64
l1 SymBV sym 64
l2
         Bool -> ExceptT String IO () -> ExceptT String IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless Bool
ok (ExceptT String IO () -> ExceptT String IO ())
-> ExceptT String IO () -> ExceptT String IO ()
forall a b. (a -> b) -> a -> b
$ String -> ExceptT String IO ()
forall a. String -> ExceptT String IO a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO ()) -> String -> ExceptT String IO ()
forall a b. (a -> b) -> a -> b
$
             [String] -> String
unlines [ String
"array lengths differ for region " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n
                     , Doc Any -> String
forall a. Show a => a -> String
show (SymBV sym 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 SymBV sym 64
l1)
                     , Doc Any -> String
forall a. Show a => a -> String
show (SymBV sym 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 SymBV sym 64
l2)
                     ]
   checkMBD Natural
n MemoryBlockData sym
_ MemoryBlockData sym
_ =
      String -> ExceptT String IO ()
forall a. String -> ExceptT String IO a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String
"Regular block incompatible with array block in region " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n)

   checkMemRegion :: Natural -> Natural -> MemoryRegion sym -> MemoryRegion sym -> ExceptT String IO ()
   checkMemRegion :: Natural
-> Natural
-> MemoryRegion sym
-> MemoryRegion sym
-> ExceptT String IO ()
checkMemRegion Natural
n Natural
o MemoryRegion sym
r1 MemoryRegion sym
r2 =
     do Bool -> ExceptT String IO () -> ExceptT String IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (MemoryRegion sym -> BV 64
forall sym. MemoryRegion sym -> BV 64
regionOffset MemoryRegion sym
r1 BV 64 -> BV 64 -> Bool
forall a. Eq a => a -> a -> Bool
== MemoryRegion sym -> BV 64
forall sym. MemoryRegion sym -> BV 64
regionOffset MemoryRegion sym
r2)
               (String -> ExceptT String IO ()
forall a. String -> ExceptT String IO a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String
"region offsets differ in region " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
o))
        Bool -> ExceptT String IO () -> ExceptT String IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (MemoryRegion sym -> Bytes
forall sym. MemoryRegion sym -> Bytes
regionSize MemoryRegion sym
r1 Bytes -> Bytes -> Bool
forall a. Eq a => a -> a -> Bool
== MemoryRegion sym -> Bytes
forall sym. MemoryRegion sym -> Bytes
regionSize MemoryRegion sym
r2)
               (String -> ExceptT String IO ()
forall a. String -> ExceptT String IO a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String
"region sizes differ in region " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
o))
        Bool -> ExceptT String IO () -> ExceptT String IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (MemoryRegion sym -> StorageType
forall sym. MemoryRegion sym -> StorageType
regionStorage MemoryRegion sym
r1 StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== MemoryRegion sym -> StorageType
forall sym. MemoryRegion sym -> StorageType
regionStorage MemoryRegion sym
r2)
               (String -> ExceptT String IO ()
forall a. String -> ExceptT String IO a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String
"region storage types differ in region " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
o))

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