Remove the use of the WithAssertions expression former in crucible-…

…llvm.

Instead, a language-extension expression former `LLVM_SideConditions` has
been added that directly references the `LLVM_SafetyCondition` type.

crucible-llvm/src/Lang/Crucible/LLVM/Arch.hs

@@ -1,20 +1,30 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 module Lang.Crucible.LLVM.Arch
  ( llvmExtensionEval
  ) where
 
+import Control.Lens ( (^.), to )
+import Control.Monad (forM_)
+import qualified Data.List.NonEmpty as NE
+import Data.Parameterized.TraversableF
+
 import What4.Interface
 
 import Lang.Crucible.Backend
 import Lang.Crucible.Simulator.Intrinsics
 import Lang.Crucible.Simulator.Evaluation
+import Lang.Crucible.Simulator.RegValue
+import Lang.Crucible.Simulator.SimError
 
 import qualified Lang.Crucible.LLVM.Arch.X86 as X86
 import Lang.Crucible.LLVM.Extension
+import Lang.Crucible.LLVM.Extension.Safety
 import Lang.Crucible.LLVM.MemModel.Pointer
 
-llvmExtensionEval ::
+llvmExtensionEval :: forall sym arch.
  IsSymInterface sym =>
  sym ->
  IntrinsicTypes sym ->
@@ -25,6 +35,14 @@ llvmExtensionEval sym _iTypes _logFn eval e =
  case e of
  X86Expr ex -> X86.eval sym eval ex
 
+ LLVM_SideConditions _tp conds val ->
+ do conds' <- traverse (traverseF (\x -> RV @sym <$> eval x)) (NE.toList conds)
+ forM_ conds' $ \c ->
+ do let bb = c^.classifier
+ let err = AssertFailureSimError (show (explainBB bb)) (show (detailBB bb))
+ assert sym (c^.predicate.to unRV) err
+ eval val
+
  LLVM_PointerExpr _w blk off ->
  do blk' <- eval blk
  off' <- eval off

crucible-llvm/src/Lang/Crucible/LLVM/Extension.hs

@@ -38,10 +38,8 @@ import Lang.Crucible.CFG.Extension.Safety
 import Lang.Crucible.Types
 
 import Lang.Crucible.LLVM.Extension.Arch
-import Lang.Crucible.LLVM.Extension.Safety (BadBehavior(..), LLVMSafetyAssertion)
+import Lang.Crucible.LLVM.Extension.Safety (LLVMSafetyAssertion)
 import qualified Lang.Crucible.LLVM.Extension.Safety as LLVMSafe
-import qualified Lang.Crucible.LLVM.Extension.Safety.Poison as Poison
-import qualified Lang.Crucible.LLVM.Extension.Safety.UndefinedBehavior as UB
 import Lang.Crucible.LLVM.Extension.Syntax
 
 -- | The Crucible extension type marker for LLVM.
@@ -65,13 +63,7 @@ instance HasStructuredAssertions (LLVM arch) where
  toPredicate _proxy _sym cls = cls ^. LLVMSafe.predicate & pure . unRV
 
  explain _proxyExt assertion =
- case assertion ^. LLVMSafe.classifier of
- BBUndefinedBehavior ub -> UB.explain ub
- BBPoison poison -> Poison.explain poison
- BBSafe -> "A value that's always safe"
+ LLVMSafe.explainBB (assertion ^. LLVMSafe.classifier)
 
- detail _proxyExt proxySym assertion =
- case assertion ^. LLVMSafe.classifier of
- BBUndefinedBehavior ub -> UB.ppReg proxySym ub
- BBPoison poison -> Poison.ppReg proxySym poison
- BBSafe -> "A value that's always safe"
+ detail _proxyExt _proxySym assertion =
+ LLVMSafe.detailBB (assertion ^. LLVMSafe.classifier)

crucible-llvm/src/Lang/Crucible/LLVM/Extension/Safety.hs

@@ -11,6 +11,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
@@ -29,6 +30,8 @@ module Lang.Crucible.LLVM.Extension.Safety
  , poison
  , poison'
  , safe
+ , detailBB
+ , explainBB
  -- ** Lenses
  , classifier
  , predicate
@@ -43,6 +46,7 @@ import Data.Text (Text)
 import Data.Maybe (isJust)
 import Data.Typeable (Typeable)
 import GHC.Generics (Generic)
+import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
 import qualified What4.Interface as W4I
 import What4.Partial.AssertionTree
@@ -248,3 +252,17 @@ predicate = lens _predicate (\s v -> s { _predicate = v})
 
 extra :: Simple Lens (LLVMSafetyAssertion e) (Maybe Text)
 extra = lens _extra (\s v -> s { _extra = v})
+
+
+
+explainBB :: BadBehavior e -> Doc
+explainBB = \case
+ BBUndefinedBehavior ub -> UB.explain ub
+ BBPoison p -> Poison.explain p
+ BBSafe -> text "A value that's always safe"
+
+detailBB :: W4I.IsExpr (W4I.SymExpr sym) => BadBehavior (RegValue' sym) -> Doc
+detailBB = \case
+ BBUndefinedBehavior ub -> UB.ppReg ub
+ BBPoison p -> Poison.ppReg p
+ BBSafe -> text "A value that's always safe"

crucible-llvm/src/Lang/Crucible/LLVM/Extension/Safety/Poison.hs

@@ -48,9 +48,8 @@ import Data.Parameterized.ClassesC (TestEqualityC(..), OrdC(..))
 import Data.Parameterized.Classes (OrderingF(..), toOrdering)
 
 import Lang.Crucible.LLVM.Extension.Safety.Standards
-import Lang.Crucible.Simulator.RegValue (RegValue'(..))
 import Lang.Crucible.Types
-import qualified What4.Interface as W4I
+--import qualified What4.Interface as W4I
 
 data Poison (e :: CrucibleType -> Type) where
  -- | Arguments: @op1@, @op2@
@@ -231,12 +230,9 @@ explain =
  , "flag set."
  ]
 
-detailsReg :: W4I.IsExpr (W4I.SymExpr sym)
- => proxy sym
- -- ^ Not really used, prevents ambiguous types. Can use "Data.Proxy".
- -> Poison (RegValue' sym)
- -> [Doc]
-detailsReg _proxySym = const [] -- TODO: details
+detailsReg ::
+ Poison e -> [Doc]
+detailsReg = const [] -- TODO: details
  -- \case
  -- AddNoUnsignedWrap _ _ -> _
  -- AddNoSignedWrap _ _ -> _
@@ -270,12 +266,8 @@ pp extra poison = vcat $
  Just url -> ["Document URL:" <+> text (unpack url)]
  Nothing -> []
 
-ppReg :: W4I.IsExpr (W4I.SymExpr sym)
- => proxy sym
- -- ^ Not really used, prevents ambiguous types. Can use "Data.Proxy".
- -> Poison (RegValue' sym)
- -> Doc
-ppReg proxySym = pp (detailsReg proxySym)
+ppReg :: Poison e -> Doc
+ppReg = pp detailsReg
 
 -- -----------------------------------------------------------------------
 -- ** Instances

crucible-llvm/src/Lang/Crucible/LLVM/Extension/Safety/UndefinedBehavior.hs

@@ -356,11 +356,9 @@ explain =
 -- | Pretty-print the additional information held by the constructors
 -- (for symbolic expressions)
 detailsReg :: W4I.IsExpr (W4I.SymExpr sym)
- => proxy sym
- -- ^ Not really used, prevents ambiguous types. Can use "Data.Proxy".
- -> UndefinedBehavior (RegValue' sym)
+ => UndefinedBehavior (RegValue' sym)
  -> [Doc]
-detailsReg proxySym =
+detailsReg =
  \case
 
  -------------------------------- Memory management
@@ -382,7 +380,7 @@ detailsReg proxySym =
 
  PtrAddOffsetOutOfBounds ptr offset ->
  [ ppPtr1 ptr
- , ppOffset proxySym (unRV offset)
+ , ppOffset (unRV offset)
  ]
  CompareInvalidPointer comparison invalid other ->
  [ "Comparison: " <+> ppPtrComparison comparison
@@ -426,9 +424,8 @@ detailsReg proxySym =
  , "Pointer 2:" <+> ppPointerPair ptr2
  ]
 
- ppOffset :: W4I.IsExpr (W4I.SymExpr sym)
- => proxy sym -> W4I.SymExpr sym (BaseBVType w) -> Doc
- ppOffset _ = ("Offset:" <+>) . W4I.printSymExpr
+ ppOffset :: W4I.IsExpr e => e (BaseBVType w) -> Doc
+ ppOffset = ("Offset:" <+>) . W4I.printSymExpr
 
 pp :: (UndefinedBehavior e -> [Doc]) -- ^ Printer for constructor data
  -> UndefinedBehavior e
@@ -446,12 +443,11 @@ pp extra ub = vcat $
  Nothing -> []
 
 -- | Pretty-printer for symbolic backends
-ppReg :: W4I.IsExpr (W4I.SymExpr sym)
- => proxy sym
- -- ^ Not really used, prevents ambiguous types. Can use "Data.Proxy".
- -> UndefinedBehavior (RegValue' sym)
- -> Doc
-ppReg proxySym = pp (detailsReg proxySym)
+ppReg ::
+ W4I.IsExpr (W4I.SymExpr sym) =>
+ UndefinedBehavior (RegValue' sym) ->
+ Doc
+ppReg = pp (detailsReg)
 
 -- -----------------------------------------------------------------------
 -- ** Instances

crucible-llvm/src/Lang/Crucible/LLVM/Extension/Syntax.hs

@@ -14,18 +14,23 @@
 {-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 
 module Lang.Crucible.LLVM.Extension.Syntax where
 
 import Data.Kind
+import Data.List.NonEmpty (NonEmpty)
 import GHC.TypeLits
 import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
+import Data.Functor.Classes (Eq1(..), Ord1(..))
 import Data.Parameterized.Classes
+import Data.Parameterized.ClassesC (TestEqualityC(..), OrdC(..))
 import qualified Data.Parameterized.TH.GADT as U
+import Data.Parameterized.TraversableF
 import Data.Parameterized.TraversableFC
 
 import Lang.Crucible.CFG.Common
@@ -36,14 +41,20 @@ import Lang.Crucible.LLVM.Arch.X86 as X86
 import Lang.Crucible.LLVM.Bytes
 import Lang.Crucible.LLVM.DataLayout
 import Lang.Crucible.LLVM.Extension.Arch
-import Lang.Crucible.LLVM.Extension.Safety ()
+import Lang.Crucible.LLVM.Extension.Safety( LLVMSafetyAssertion )
 import Lang.Crucible.LLVM.MemModel.Pointer
 import Lang.Crucible.LLVM.MemModel.Type
 import Lang.Crucible.LLVM.Types
 
 data LLVMExtensionExpr (arch :: LLVMArch) :: (CrucibleType -> Type) -> (CrucibleType -> Type) where
  X86Expr :: !(X86.ExtX86 f t) -> LLVMExtensionExpr (X86 wptr) f t
 
+ LLVM_SideConditions ::
+ !(TypeRepr tp) ->
+ !(NonEmpty (LLVMSafetyAssertion f)) ->
+ !(f tp) ->
+ LLVMExtensionExpr arch f tp
+
  LLVM_PointerExpr ::
  (1 <= w) => !(NatRepr w) -> !(f NatType) -> !(f (BVType w)) ->
  LLVMExtensionExpr arch f (LLVMPointerType w)
@@ -187,6 +198,7 @@ instance TypeApp (LLVMExtensionExpr arch) where
  appType e =
  case e of
  X86Expr ex -> appType ex
+ LLVM_SideConditions tpr _ _ -> tpr
  LLVM_PointerExpr w _ _ -> LLVMPointerRepr w
  LLVM_PointerBlock _ _ -> NatRepr
  LLVM_PointerOffset w _ -> BVRepr w
@@ -196,6 +208,8 @@ instance PrettyApp (LLVMExtensionExpr arch) where
  ppApp pp e =
  case e of
  X86Expr ex -> ppApp pp ex
+ LLVM_SideConditions _ _conds ex ->
+ text "sideConditions" <+> pp ex -- TODO? Print the conditions?
  LLVM_PointerExpr _ blk off ->
  text "pointerExpr" <+> pp blk <+> pp off
  LLVM_PointerBlock _ ptr ->
@@ -210,15 +224,23 @@ instance TestEqualityFC (LLVMExtensionExpr arch) where
  $(U.structuralTypeEquality [t|LLVMExtensionExpr|]
  [ (U.DataArg 1 `U.TypeApp` U.AnyType, [|testSubterm|])
  , (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
+ , (U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
  , (U.ConType [t|X86.ExtX86|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|testEqualityFC testSubterm|])
+ , (U.ConType [t|NonEmpty|] `U.TypeApp` (U.ConType [t|LLVMSafetyAssertion|] `U.TypeApp` U.AnyType)
+ , [| \x y -> if liftEq (testEqualityC testSubterm) x y then Just Refl else Nothing |]
+ )
  ])
 
 instance OrdFC (LLVMExtensionExpr arch) where
  compareFC testSubterm =
  $(U.structuralTypeOrd [t|LLVMExtensionExpr|]
  [ (U.DataArg 1 `U.TypeApp` U.AnyType, [|testSubterm|])
  , (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
+ , (U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
  , (U.ConType [t|X86.ExtX86|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|compareFC testSubterm|])
+ , (U.ConType [t|NonEmpty|] `U.TypeApp` (U.ConType [t|LLVMSafetyAssertion|] `U.TypeApp` U.AnyType)
+ , [| \x y -> fromOrdering (liftCompare (compareC testSubterm) x y) |]
+ )
  ])
 
 instance FunctorFC (LLVMExtensionExpr arch) where
@@ -227,12 +249,22 @@ instance FunctorFC (LLVMExtensionExpr arch) where
 instance FoldableFC (LLVMExtensionExpr arch) where
  foldMapFC = foldMapFCDefault
 
+
+traverseConds ::
+ Applicative m =>
+ (forall s. f s -> m (g s)) ->
+ NonEmpty (LLVMSafetyAssertion f) ->
+ m (NonEmpty (LLVMSafetyAssertion g))
+traverseConds f = traverse (traverseF f)
+
 instance TraversableFC (LLVMExtensionExpr arch) where
  traverseFC = $(U.structuralTraversal [t|LLVMExtensionExpr|]
  [(U.ConType [t|X86.ExtX86|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|traverseFC|])
+ ,(U.ConType [t|NonEmpty|] `U.TypeApp` (U.ConType [t|LLVMSafetyAssertion|] `U.TypeApp` U.AnyType)
+ , [| traverseConds |]
+ )
  ])
 
-
 instance (1 <= wptr) => TypeApp (LLVMStmt wptr) where
  appType = \case
  LLVM_PushFrame{} -> knownRepr

crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

@@ -288,7 +288,7 @@ assertUndefined :: (IsSymInterface sym, HasPtrWidth wptr)
 assertUndefined sym p ub = assert sym p $ AssertFailureSimError msg details
  where
  msg = show (UB.explain ub)
- details = show (UB.ppReg (Just sym) ub)
+ details = show (UB.ppReg ub)
 
 instance IntrinsicClass sym "LLVM_memory" where
  type Intrinsic sym "LLVM_memory" ctx = MemImpl sym

crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs

@@ -61,12 +61,10 @@ import qualified Data.Parameterized.Context as Ctx
 import Data.Parameterized.NatRepr as NatRepr
 import Data.Parameterized.Some
 
-import qualified What4.Partial.AssertionTree as W4P
 import What4.Utils.StringLiteral
 
 import Lang.Crucible.CFG.Expr
 import Lang.Crucible.CFG.Generator
-import Lang.Crucible.CFG.Extension.Safety (pattern PartialExp)
 
 import qualified Lang.Crucible.LLVM.Bytes as G
 import Lang.Crucible.LLVM.DataLayout
@@ -117,9 +115,7 @@ sideConditionsA tyRepr expr conds =
  in flip fmap conds' $
  \case
  [] -> expr -- No assertions left, nothing to do.
- (x:xs) ->
- let assertion = W4P.And (fmap W4P.Leaf (x :| xs))
- in App $ WithAssertion tyRepr (PartialExp assertion expr)
+ (x:xs) -> App $ ExtensionApp $ LLVM_SideConditions tyRepr (x :| xs) expr
 
 -- | Assert that evaluation doesn't result in a poison value
 poisonSideCondition :: TypeRepr ty