From 5235ceaf5cef85362bbddf198d73d9eca6ca5bb1 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 4 Jun 2024 15:59:02 -0400 Subject: [PATCH 1/8] Concretization: Getting concrete `RegValue`s from a model What4 has the capacity to turn symbolic values into plausible "concrete" (/"ground") values, given a model from the SMT solver (`GroundEvalFn`). This commit builds on this feature to enable concretizing more complex Crucible types. A possible use-case is to present concrete instances where safety assertions fail, e.g. when symbolically executing the following function: int f(int x, int y) { return x / (y - 2); } it would be nice to say which particular values of `x` and `y` would cause either signed underflow (`y < INT_MIN + 2`) or division by zero (`y == 2`). This particular case could be handled by existing What4 functionality, but the same motivation applies to more complex cases involving Crucible-specific types. --- .../Lang/Crucible/LLVM/MemModel/Pointer.hs | 68 +++- crucible/crucible.cabal | 1 + crucible/src/Lang/Crucible/Concretize.hs | 380 ++++++++++++++++++ 3 files changed, 444 insertions(+), 5 deletions(-) create mode 100644 crucible/src/Lang/Crucible/Concretize.hs diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs index 3cdfe0076..a8020a2d2 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs @@ -20,6 +20,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} @@ -51,9 +52,13 @@ module Lang.Crucible.LLVM.MemModel.Pointer , mkNullPointer -- * Concretization + , ConcLLVMPtr(..) + , concLLVMPtr + , concLLVMPtrToSymbolic , concBV , concPtr , concPtr' + , concPtrFn -- * Operations on valid pointers , constOffset @@ -74,7 +79,7 @@ module Lang.Crucible.LLVM.MemModel.Pointer , annotatePointerOffset ) where -import Control.Monad (guard) +import Control.Monad ((<=<), guard) import Data.Map (Map) import qualified Data.Map as Map (lookup) import Numeric.Natural @@ -89,17 +94,21 @@ import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.NatRepr import qualified Text.LLVM.AST as L +import qualified What4.Expr.GroundEval as W4GE import What4.Interface import What4.InterpretedFloatingPoint import What4.Expr (GroundValue) import Lang.Crucible.Backend +import qualified Lang.Crucible.Concretize as Conc import Lang.Crucible.Simulator.RegMap import Lang.Crucible.Simulator.Intrinsics import Lang.Crucible.Types import qualified Lang.Crucible.LLVM.Bytes as G import Lang.Crucible.LLVM.Types import Lang.Crucible.LLVM.MemModel.Options +import What4.Expr.App (Expr) +import Lang.Crucible.Panic (panic) @@ -154,6 +163,38 @@ llvmPointer_bv sym bv = mkNullPointer :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> IO (LLVMPtr sym w) mkNullPointer sym w = llvmPointer_bv sym =<< bvZero sym w +-- | A concrete LLVM pointer +data ConcLLVMPtr w + = ConcLLVMPtr + { -- | Concrete block number + concBlock :: Integer + -- | Concrete offset + , concOffset :: BV.BV w + , concWidth :: NatRepr w + } + +-- | Concretize a symbolic pointer to a particular 'ConcLLVMPtr' that is +-- feasible in a model. +concLLVMPtr :: + IsExprBuilder sym => + -- | Model from SMT solver + (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> + RegValue sym (LLVMPointerType w) -> + IO (ConcLLVMPtr w) +concLLVMPtr conc (LLVMPointer blk off) = + do concBlk <- conc (natToIntegerPure blk) + concOff <- conc off + pure (ConcLLVMPtr concBlk concOff (bvWidth off)) + +concLLVMPtrToSymbolic :: + (IsExprBuilder sym, 1 <= w) => + sym -> + ConcLLVMPtr w -> + IO (RegValue sym (LLVMPointerType w)) +concLLVMPtrToSymbolic sym (ConcLLVMPtr concBlk concOff w) = do + symBlk <- integerToNat sym =<< intLit sym concBlk + symOff <- bvLit sym w concOff + pure (LLVMPointer symBlk symOff) concBV :: (IsExprBuilder sym, 1 <= w) => @@ -170,10 +211,7 @@ concPtr :: (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> RegValue sym (LLVMPointerType w) -> IO (RegValue sym (LLVMPointerType w)) -concPtr sym conc (LLVMPointer blk off) = - do blk' <- integerToNat sym =<< intLit sym =<< conc =<< natToInteger sym blk - off' <- concBV sym conc off - pure (LLVMPointer blk' off') +concPtr sym conc = concLLVMPtrToSymbolic sym <=< concLLVMPtr conc concPtr' :: (IsExprBuilder sym, 1 <= w) => @@ -183,6 +221,26 @@ concPtr' :: IO (RegValue' sym (LLVMPointerType w)) concPtr' sym conc (RV ptr) = RV <$> concPtr sym conc ptr +type instance Conc.ConcIntrinsic "LLVM_pointer" (EmptyCtx ::> BVType w) = ConcLLVMPtr w + +concPtrFn :: + forall sym. + ( IsExprBuilder sym + , SymExpr sym ~ Expr sym + ) => + Conc.IntrinsicConcFn sym "LLVM_pointer" +concPtrFn = Conc.IntrinsicConcFn $ \ctx tyCtx ptr -> + case Ctx.viewAssign tyCtx of + Ctx.AssignExtend (Ctx.viewAssign -> Ctx.AssignEmpty) (BVRepr _) -> + let W4GE.GroundEvalFn ge = Conc.model ctx + in concLLVMPtr ge ptr + -- These are impossible by the definition of LLVMPointerImpl + Ctx.AssignEmpty -> + panic "LLVM.MemModel.Pointer.concPtrFn" + [ "Impossible: LLVMPointerType empty context" ] + Ctx.AssignExtend _ _ -> + panic "LLVM.MemModel.Pointer.concPtrFn" + [ "Impossible: LLVMPointerType ill-formed context" ] -- | Mux function specialized to LLVM pointer values. muxLLVMPtr :: diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal index d1f853645..4540ec190 100644 --- a/crucible/crucible.cabal +++ b/crucible/crucible.cabal @@ -84,6 +84,7 @@ library Lang.Crucible.Backend.ProofGoals Lang.Crucible.Backend.Online Lang.Crucible.Backend.Simple + Lang.Crucible.Concretize Lang.Crucible.CFG.Common Lang.Crucible.CFG.Core Lang.Crucible.CFG.Expr diff --git a/crucible/src/Lang/Crucible/Concretize.hs b/crucible/src/Lang/Crucible/Concretize.hs new file mode 100644 index 000000000..2148d2471 --- /dev/null +++ b/crucible/src/Lang/Crucible/Concretize.hs @@ -0,0 +1,380 @@ +----------------------------------------------------------------------- +-- | +-- Module : Lang.Crucible.Concretize +-- Description : Get feasible concrete values from a model +-- Copyright : (c) Galois, Inc 2024 +-- License : BSD3 +-- Maintainer : Langston Barrett +-- Stability : provisional +-- +-- This module defines 'concRegValue', a function that takes a 'RegValue' (i.e., +-- a symbolic value), and a model from the SMT solver ('W4GE.GroundEvalFn'), and +-- returns the concrete value that the symbolic value takes in the model. +-- +-- This can be used to report specific values that lead to violations of +-- assertions, including safety assertions. +------------------------------------------------------------------------ + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Lang.Crucible.Concretize + ( ConcRegValue + , ConcRegValue'(..) + , ConcAnyValue(..) + , ConcIntrinsic + , IntrinsicConcFn(..) + , ConcCtx(..) + , concRegValue + ) where + +import Data.Kind (Type) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Text (Text) +import qualified Data.Vector as V +import Data.Word (Word16) + +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Map (MapF) +import qualified Data.Parameterized.Map as MapF + +import What4.Expr (Expr) +import qualified What4.Expr.GroundEval as W4GE +import What4.Interface (SymExpr) +import qualified What4.Interface as W4I +import qualified What4.Partial as W4P + +import Lang.Crucible.FunctionHandle (FnHandle, RefCell) +import Lang.Crucible.Simulator.Intrinsics (Intrinsic) +import Lang.Crucible.Simulator.RegValue (RegValue, FnVal) +import qualified Lang.Crucible.Simulator.RegValue as RV +import qualified Lang.Crucible.Simulator.SymSequence as SymSeq +import qualified Lang.Crucible.Utils.MuxTree as MuxTree +import Lang.Crucible.Types + +-- | Newtype to allow partial application of 'ConcRegValue'. +-- +-- Type families cannot appear partially applied. +type ConcRegValue' :: Type -> CrucibleType -> Type +newtype ConcRegValue' sym tp = ConcRegValue' { getConcRegValue' :: ConcRegValue sym tp } + +-- | Defines the \"concrete\" interpretations of 'CrucibleType' (as opposed +-- to the \"symbolic\" interpretations, which are defined by 'RegValue'), as +-- returned by 'concRegValue'. +type ConcRegValue :: Type -> CrucibleType -> Type +type family ConcRegValue sym tp where + ConcRegValue sym (BaseToType bt) = W4GE.GroundValue bt + ConcRegValue sym (FloatType fi) = W4GE.GroundValue (SymInterpretedFloatType sym fi) + ConcRegValue sym AnyType = ConcAnyValue sym + ConcRegValue sym UnitType = () + ConcRegValue sym NatType = Integer + ConcRegValue sym CharType = Word16 + ConcRegValue sym (FunctionHandleType a r) = ConcFnVal sym a r + ConcRegValue sym (MaybeType tp) = Maybe (ConcRegValue sym tp) + ConcRegValue sym (VectorType tp) = V.Vector (ConcRegValue' sym tp) + ConcRegValue sym (SequenceType tp) = [ConcRegValue' sym tp] + ConcRegValue sym (StructType ctx) = Ctx.Assignment (ConcRegValue' sym) ctx + ConcRegValue sym (VariantType ctx) = Ctx.Assignment (ConcVariantBranch sym) ctx + ConcRegValue sym (ReferenceType tp) = [RefCell tp] + ConcRegValue sym (WordMapType w tp) = () -- TODO: possible to do something meaningful? + ConcRegValue sym (RecursiveType nm ctx) = ConcRegValue sym (UnrollType nm ctx) + ConcRegValue sym (IntrinsicType nm ctx) = ConcIntrinsic nm ctx + ConcRegValue sym (StringMapType tp) = Map Text (ConcRegValue' sym tp) + +--------------------------------------------------------------------- +-- * ConcCtx + +-- | Context needed for 'concRegValue' +data ConcCtx sym = + ConcCtx + { -- | Model returned from SMT solver + model :: W4GE.GroundEvalFn sym + -- | How to ground intrinsics + , intrinsicConcFuns :: MapF SymbolRepr (IntrinsicConcFn sym) + } + +-- | Helper, not exported +ground :: + ConcCtx sym -> + Expr sym tp -> + IO (ConcRegValue sym (BaseToType tp)) +ground (ConcCtx (W4GE.GroundEvalFn ge) _) = ge + +--------------------------------------------------------------------- +-- * Helpers + +-- | Helper, not exported +ite :: + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + W4I.Pred sym -> + a -> + a -> + IO a +ite ctx p t f = do + b <- ground ctx p + pure (if b then t else f) + +-- | Helper, not exported +iteIO :: + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + W4I.Pred sym -> + IO a -> + IO a -> + IO a +iteIO ctx p t f = do + b <- ground ctx p + if b then t else f + +-- | Helper, not exported +concPartial :: + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + TypeRepr tp -> + W4P.Partial (W4I.Pred sym) (RegValue sym tp) -> + IO (Maybe (ConcRegValue sym tp)) +concPartial ctx tp (W4P.Partial p v) = + iteIO ctx p (Just <$> concRegValue ctx tp v) (pure Nothing) + +-- | Helper, not exported +concPartialWithErr :: + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + TypeRepr tp -> + W4P.PartialWithErr e (W4I.Pred sym) (RegValue sym tp) -> + IO (Maybe (ConcRegValue sym tp)) +concPartialWithErr ctx tp = + \case + W4P.Err _ -> pure Nothing + W4P.NoErr pv -> concPartial ctx tp pv + +--------------------------------------------------------------------- +-- * Intrinsics + +-- | Open type family for defining how intrinsics are concretized +type ConcIntrinsic :: Symbol -> Ctx CrucibleType -> Type +type family ConcIntrinsic nm ctx + +-- | Function for concretizing an intrinsic type +type IntrinsicConcFn :: Type -> Symbol -> Type +newtype IntrinsicConcFn sym nm + = IntrinsicConcFn + (forall ctx. + ConcCtx sym -> + Ctx.Assignment TypeRepr ctx -> + Intrinsic sym nm ctx -> + IO (ConcRegValue sym (IntrinsicType nm ctx))) + +-- | Helper, not exported +tryConcIntrinsic :: + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + SymbolRepr nm -> + Ctx.Assignment TypeRepr ctx -> + RegValue sym (IntrinsicType nm ctx) -> + Maybe (IO (ConcRegValue sym (IntrinsicType nm ctx))) +tryConcIntrinsic ctx nm tyCtx v = do + case MapF.lookup nm (intrinsicConcFuns ctx) of + Nothing -> Nothing + Just (IntrinsicConcFn f) -> Just (f ctx tyCtx v) + +--------------------------------------------------------------------- +-- * Any + +-- | An 'AnyValue' concretized by 'concRegValue' +data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRegValue' sym tp) + +--------------------------------------------------------------------- +-- * FnVal + +-- | A 'FnVal' concretized by 'concRegValue' +data ConcFnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where + ConcClosureFnVal :: + !(ConcFnVal sym (args ::> tp) ret) -> + !(TypeRepr tp) -> + !(ConcRegValue' sym tp) -> + ConcFnVal sym args ret + + ConcVarargsFnVal :: + !(FnHandle (args ::> VectorType AnyType) ret) -> + !(CtxRepr addlArgs) -> + ConcFnVal sym (args <+> addlArgs) ret + + ConcHandleFnVal :: + !(FnHandle a r) -> + ConcFnVal sym a r + +-- | Helper, not exported +concFnVal :: + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + CtxRepr args -> + TypeRepr ret -> + FnVal sym args ret -> + IO (ConcFnVal sym args ret) +concFnVal ctx args ret = + \case + RV.ClosureFnVal fv t v -> do + concV <- concFnVal ctx (args Ctx.:> t) ret fv + v' <- concRegValue ctx t v + pure (ConcClosureFnVal concV t (ConcRegValue' v')) + RV.VarargsFnVal hdl extra -> + pure (ConcVarargsFnVal hdl extra) + RV.HandleFnVal hdl -> + pure (ConcHandleFnVal hdl) + +--------------------------------------------------------------------- +-- * Reference + +-- | Helper, not exported +concMux :: + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + MuxTree.MuxTree sym a -> + IO [a] +concMux ctx = go . MuxTree.viewMuxTree + where + go [] = pure [] + go ((val, p):xs) = do + f <- ite ctx p (val:) id + f <$> go xs + +--------------------------------------------------------------------- +-- * Sequence + +-- | Helper, not exported +concSymSequence :: + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + TypeRepr tp -> + SymSeq.SymSequence sym (RegValue sym tp) -> + IO [ConcRegValue' sym tp] +concSymSequence ctx tp = + \case + SymSeq.SymSequenceNil -> pure [] + SymSeq.SymSequenceCons _nonce v rest -> do + v' <- concRegValue ctx tp v + (ConcRegValue' v' :) <$> concSymSequence ctx tp rest + SymSeq.SymSequenceAppend _nonce xs ys -> + (++) <$> concSymSequence ctx tp xs <*> concSymSequence ctx tp ys + SymSeq.SymSequenceMerge _nonce p ts fs -> + concSymSequence ctx tp =<< ite ctx p ts fs + +--------------------------------------------------------------------- +-- * StringMap + +-- | Helper, not exported +concStringMap :: + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + TypeRepr tp -> + RegValue sym (StringMapType tp) -> + IO (Map Text (ConcRegValue' sym tp)) +concStringMap ctx tp v = Map.fromList <$> go (Map.toList v) + where + go [] = pure [] + go ((t, v'):xs) = + concPartialWithErr ctx tp v' >>= + \case + Nothing -> go xs + Just v'' -> ((t, ConcRegValue' v''):) <$> go xs + +--------------------------------------------------------------------- +-- * Variant + +-- | Note that we do not attempt to \"normalize\" variants in 'concRegValue' +-- in any way. If the model reports that multiple branches of a variant are +-- plausible, then multiple branches might be included as 'Just's. +newtype ConcVariantBranch sym tp + = ConcVariantBranch (Maybe (ConcRegValue' sym tp)) + +-- | Helper, not exported +concVariant :: + forall sym variants. + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + Ctx.Assignment TypeRepr variants -> + RegValue sym (VariantType variants) -> + IO (ConcRegValue sym (VariantType variants)) +concVariant ctx tps vs = Ctx.zipWithM concBranch tps vs + where + concBranch :: forall tp. TypeRepr tp -> RV.VariantBranch sym tp -> IO (ConcVariantBranch sym tp) + concBranch tp (RV.VB v) = do + v' <- concPartialWithErr ctx tp v + case v' of + Just v'' -> pure (ConcVariantBranch (Just (ConcRegValue' v''))) + Nothing -> pure (ConcVariantBranch Nothing) + +--------------------------------------------------------------------- +-- * 'concRegValue' + +-- | Pick a feasible concrete value from the model +-- +-- This function does not attempt to \"normalize\" variants nor mux trees in any +-- way. If the model reports that multiple branches of a variant or mux tree are +-- plausible, then multiple branches might be included in the result. +concRegValue :: + (SymExpr sym ~ Expr sym) => + ConcCtx sym -> + TypeRepr tp -> + RegValue sym tp -> + IO (ConcRegValue sym tp) +concRegValue ctx tp v = + case (tp, v) of + -- Base types + (BoolRepr, _) -> ground ctx v + (BVRepr _width, _) -> ground ctx v + (ComplexRealRepr, _) -> ground ctx v + (FloatRepr _fpp, _) -> ground ctx v + (IEEEFloatRepr _fpp, _) -> ground ctx v + (IntegerRepr, _) -> ground ctx v + (NatRepr, _) -> ground ctx (W4I.natToIntegerPure v) + (RealValRepr, _) -> ground ctx v + (StringRepr _, _) -> ground ctx v + (SymbolicArrayRepr _idxs _tp', _) -> ground ctx v + (SymbolicStructRepr _tys, _) -> ground ctx v + + -- Trivial cases + (UnitRepr, ()) -> pure () + (CharRepr, _) -> pure v + + -- Simple recursive cases + (AnyRepr, RV.AnyValue tp' v') -> + ConcAnyValue tp' . ConcRegValue' <$> concRegValue ctx tp' v' + (RecursiveRepr symb tyCtx, RV.RolledType v') -> + concRegValue ctx (unrollType symb tyCtx) v' + (StructRepr tps, _) -> + Ctx.zipWithM (\tp' (RV.RV v') -> ConcRegValue' <$> concRegValue ctx tp' v') tps v + (VectorRepr tp', _) -> + traverse (fmap ConcRegValue' . concRegValue ctx tp') v + + -- Cases with helper functions + (MaybeRepr tp', _) -> + concPartialWithErr ctx tp' v + (FunctionHandleRepr args ret, _) -> + concFnVal ctx args ret v + (IntrinsicRepr nm tyCtx, _) -> + case tryConcIntrinsic ctx nm tyCtx v of + Nothing -> fail "Missing concretization function for intrinsic!" + Just r -> r + (ReferenceRepr _, _) -> + concMux ctx v + (SequenceRepr tp', _) -> + concSymSequence ctx tp' v + (StringMapRepr tp', _) -> + concStringMap ctx tp' v + (VariantRepr tps, _) -> + concVariant ctx tps v + + -- Incomplete clases + (WordMapRepr _ _, _) -> pure () From f6aa5619bf285c94808fb9f8fcc3ba39b240da9f Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 5 Jun 2024 14:58:39 -0400 Subject: [PATCH 2/8] Sort imports --- crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs index a8020a2d2..f672a477d 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs @@ -98,17 +98,17 @@ import qualified What4.Expr.GroundEval as W4GE import What4.Interface import What4.InterpretedFloatingPoint import What4.Expr (GroundValue) +import What4.Expr.App (Expr) import Lang.Crucible.Backend import qualified Lang.Crucible.Concretize as Conc +import Lang.Crucible.Panic (panic) import Lang.Crucible.Simulator.RegMap import Lang.Crucible.Simulator.Intrinsics import Lang.Crucible.Types import qualified Lang.Crucible.LLVM.Bytes as G import Lang.Crucible.LLVM.Types import Lang.Crucible.LLVM.MemModel.Options -import What4.Expr.App (Expr) -import Lang.Crucible.Panic (panic) From 9cc276c6c4cd387ad0743319088ebb8fbb892d3a Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 5 Jun 2024 14:59:47 -0400 Subject: [PATCH 3/8] Haddocks --- crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs index f672a477d..96d52696e 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs @@ -186,6 +186,7 @@ concLLVMPtr conc (LLVMPointer blk off) = concOff <- conc off pure (ConcLLVMPtr concBlk concOff (bvWidth off)) +-- | Create a symbolic pointer from a concrete one concLLVMPtrToSymbolic :: (IsExprBuilder sym, 1 <= w) => sym -> @@ -223,6 +224,7 @@ concPtr' sym conc (RV ptr) = RV <$> concPtr sym conc ptr type instance Conc.ConcIntrinsic "LLVM_pointer" (EmptyCtx ::> BVType w) = ConcLLVMPtr w +-- | An 'Conc.IntrinsicConcFn' for LLVM pointers concPtrFn :: forall sym. ( IsExprBuilder sym From 4e1573382203fab776ab36155318c3477cfbf597 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 5 Jun 2024 16:27:06 -0400 Subject: [PATCH 4/8] llvm: Include `concPtrFnMap` for easy use of concretization --- .../src/Lang/Crucible/LLVM/MemModel/Pointer.hs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs index 96d52696e..68a4fe4b9 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs @@ -59,6 +59,7 @@ module Lang.Crucible.LLVM.MemModel.Pointer , concPtr , concPtr' , concPtrFn + , concPtrFnMap -- * Operations on valid pointers , constOffset @@ -91,6 +92,7 @@ import GHC.TypeNats 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.NatRepr import qualified Text.LLVM.AST as L @@ -244,6 +246,16 @@ concPtrFn = Conc.IntrinsicConcFn $ \ctx tyCtx ptr -> panic "LLVM.MemModel.Pointer.concPtrFn" [ "Impossible: LLVMPointerType ill-formed context" ] +-- | A singleton map suitable for use in a 'Conc.ConcCtx' if LLVM pointers are +-- the only intrinsic type in use +concPtrFnMap :: + forall sym. + ( IsExprBuilder sym + , SymExpr sym ~ Expr sym + ) => + MapF.MapF SymbolRepr (Conc.IntrinsicConcFn sym) +concPtrFnMap = MapF.singleton (knownSymbol @"LLVM_pointer") concPtrFn + -- | Mux function specialized to LLVM pointer values. muxLLVMPtr :: (1 <= w) => From 896f4b7402a990deead224f0ae879f758e0eb7be Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 5 Jun 2024 17:10:13 -0400 Subject: [PATCH 5/8] Clean up confused type variables in concretization --- crucible/src/Lang/Crucible/Concretize.hs | 84 ++++++++++++++---------- 1 file changed, 51 insertions(+), 33 deletions(-) diff --git a/crucible/src/Lang/Crucible/Concretize.hs b/crucible/src/Lang/Crucible/Concretize.hs index 2148d2471..cb9cbdd01 100644 --- a/crucible/src/Lang/Crucible/Concretize.hs +++ b/crucible/src/Lang/Crucible/Concretize.hs @@ -25,6 +25,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} module Lang.Crucible.Concretize ( ConcRegValue @@ -94,18 +95,23 @@ type family ConcRegValue sym tp where -- * ConcCtx -- | Context needed for 'concRegValue' -data ConcCtx sym = - ConcCtx +-- +-- The @t@ parameter matches that on 'W4GE.GroundEvalFn' and 'Expr', namely, it +-- is a phantom type brand used to relate nonces to a specific nonce generator +-- (similar to the @s@ parameter of the @ST@ monad). It also appears as the +-- first argument to 'ExprBuilder'. +data ConcCtx sym t + = ConcCtx { -- | Model returned from SMT solver - model :: W4GE.GroundEvalFn sym + model :: W4GE.GroundEvalFn t -- | How to ground intrinsics - , intrinsicConcFuns :: MapF SymbolRepr (IntrinsicConcFn sym) + , intrinsicConcFuns :: MapF SymbolRepr (IntrinsicConcFn t) } -- | Helper, not exported ground :: - ConcCtx sym -> - Expr sym tp -> + ConcCtx sym t -> + Expr t tp -> IO (ConcRegValue sym (BaseToType tp)) ground (ConcCtx (W4GE.GroundEvalFn ge) _) = ge @@ -114,8 +120,8 @@ ground (ConcCtx (W4GE.GroundEvalFn ge) _) = ge -- | Helper, not exported ite :: - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + (SymExpr sym ~ Expr t) => + ConcCtx sym t -> W4I.Pred sym -> a -> a -> @@ -126,8 +132,8 @@ ite ctx p t f = do -- | Helper, not exported iteIO :: - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + (SymExpr sym ~ Expr t) => + ConcCtx sym t -> W4I.Pred sym -> IO a -> IO a -> @@ -138,8 +144,9 @@ iteIO ctx p t f = do -- | Helper, not exported concPartial :: - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + (SymExpr sym ~ Expr t) => + W4I.IsExprBuilder sym => + ConcCtx sym t -> TypeRepr tp -> W4P.Partial (W4I.Pred sym) (RegValue sym tp) -> IO (Maybe (ConcRegValue sym tp)) @@ -148,8 +155,9 @@ concPartial ctx tp (W4P.Partial p v) = -- | Helper, not exported concPartialWithErr :: - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + (SymExpr sym ~ Expr t) => + W4I.IsExprBuilder sym => + ConcCtx sym t -> TypeRepr tp -> W4P.PartialWithErr e (W4I.Pred sym) (RegValue sym tp) -> IO (Maybe (ConcRegValue sym tp)) @@ -167,18 +175,22 @@ type family ConcIntrinsic nm ctx -- | Function for concretizing an intrinsic type type IntrinsicConcFn :: Type -> Symbol -> Type -newtype IntrinsicConcFn sym nm +newtype IntrinsicConcFn t nm = IntrinsicConcFn - (forall ctx. - ConcCtx sym -> + (forall sym ctx. + SymExpr sym ~ Expr t => + W4I.IsExprBuilder sym => + ConcCtx sym t -> Ctx.Assignment TypeRepr ctx -> Intrinsic sym nm ctx -> IO (ConcRegValue sym (IntrinsicType nm ctx))) -- | Helper, not exported tryConcIntrinsic :: - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + forall sym nm ctx t. + SymExpr sym ~ Expr t => + W4I.IsExprBuilder sym => + ConcCtx sym t -> SymbolRepr nm -> Ctx.Assignment TypeRepr ctx -> RegValue sym (IntrinsicType nm ctx) -> @@ -186,7 +198,7 @@ tryConcIntrinsic :: tryConcIntrinsic ctx nm tyCtx v = do case MapF.lookup nm (intrinsicConcFuns ctx) of Nothing -> Nothing - Just (IntrinsicConcFn f) -> Just (f ctx tyCtx v) + Just (IntrinsicConcFn f) -> Just (f @sym @ctx ctx tyCtx v) --------------------------------------------------------------------- -- * Any @@ -216,8 +228,9 @@ data ConcFnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) wh -- | Helper, not exported concFnVal :: - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + (SymExpr sym ~ Expr t) => + W4I.IsExprBuilder sym => + ConcCtx sym t -> CtxRepr args -> TypeRepr ret -> FnVal sym args ret -> @@ -238,8 +251,9 @@ concFnVal ctx args ret = -- | Helper, not exported concMux :: - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + (SymExpr sym ~ Expr t) => + W4I.IsExprBuilder sym => + ConcCtx sym t -> MuxTree.MuxTree sym a -> IO [a] concMux ctx = go . MuxTree.viewMuxTree @@ -254,8 +268,9 @@ concMux ctx = go . MuxTree.viewMuxTree -- | Helper, not exported concSymSequence :: - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + (SymExpr sym ~ Expr t) => + W4I.IsExprBuilder sym => + ConcCtx sym t -> TypeRepr tp -> SymSeq.SymSequence sym (RegValue sym tp) -> IO [ConcRegValue' sym tp] @@ -275,8 +290,9 @@ concSymSequence ctx tp = -- | Helper, not exported concStringMap :: - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + (SymExpr sym ~ Expr t) => + W4I.IsExprBuilder sym => + ConcCtx sym t -> TypeRepr tp -> RegValue sym (StringMapType tp) -> IO (Map Text (ConcRegValue' sym tp)) @@ -300,9 +316,10 @@ newtype ConcVariantBranch sym tp -- | Helper, not exported concVariant :: - forall sym variants. - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + forall sym variants t. + (SymExpr sym ~ Expr t) => + W4I.IsExprBuilder sym => + ConcCtx sym t -> Ctx.Assignment TypeRepr variants -> RegValue sym (VariantType variants) -> IO (ConcRegValue sym (VariantType variants)) @@ -324,8 +341,9 @@ concVariant ctx tps vs = Ctx.zipWithM concBranch tps vs -- way. If the model reports that multiple branches of a variant or mux tree are -- plausible, then multiple branches might be included in the result. concRegValue :: - (SymExpr sym ~ Expr sym) => - ConcCtx sym -> + (SymExpr sym ~ Expr t) => + W4I.IsExprBuilder sym => + ConcCtx sym t -> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp) From 74f56f5f59f77e76de0a83c0432cb086259224b9 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 5 Jun 2024 17:12:43 -0400 Subject: [PATCH 6/8] Fix typo --- crucible/src/Lang/Crucible/Concretize.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crucible/src/Lang/Crucible/Concretize.hs b/crucible/src/Lang/Crucible/Concretize.hs index cb9cbdd01..5df56191a 100644 --- a/crucible/src/Lang/Crucible/Concretize.hs +++ b/crucible/src/Lang/Crucible/Concretize.hs @@ -394,5 +394,5 @@ concRegValue ctx tp v = (VariantRepr tps, _) -> concVariant ctx tps v - -- Incomplete clases + -- Incomplete cases (WordMapRepr _ _, _) -> pure () From 7e26cf28009f035e77894b3778ac172f10077a3a Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 6 Jun 2024 11:08:28 -0400 Subject: [PATCH 7/8] Review comments: naming, error mesages, haddocks --- crucible/src/Lang/Crucible/Concretize.hs | 50 ++++++++++++++---------- 1 file changed, 30 insertions(+), 20 deletions(-) diff --git a/crucible/src/Lang/Crucible/Concretize.hs b/crucible/src/Lang/Crucible/Concretize.hs index 5df56191a..8197b9218 100644 --- a/crucible/src/Lang/Crucible/Concretize.hs +++ b/crucible/src/Lang/Crucible/Concretize.hs @@ -29,7 +29,7 @@ module Lang.Crucible.Concretize ( ConcRegValue - , ConcRegValue'(..) + , ConcRV'(..) , ConcAnyValue(..) , ConcIntrinsic , IntrinsicConcFn(..) @@ -41,6 +41,7 @@ import Data.Kind (Type) import Data.Map (Map) import qualified Data.Map as Map import Data.Text (Text) +import qualified Data.Text as Text import qualified Data.Vector as V import Data.Word (Word16) @@ -65,12 +66,19 @@ import Lang.Crucible.Types -- | Newtype to allow partial application of 'ConcRegValue'. -- -- Type families cannot appear partially applied. -type ConcRegValue' :: Type -> CrucibleType -> Type -newtype ConcRegValue' sym tp = ConcRegValue' { getConcRegValue' :: ConcRegValue sym tp } +type ConcRV' :: Type -> CrucibleType -> Type +newtype ConcRV' sym tp = ConcRV' { unConcRV' :: ConcRegValue sym tp } -- | Defines the \"concrete\" interpretations of 'CrucibleType' (as opposed -- to the \"symbolic\" interpretations, which are defined by 'RegValue'), as -- returned by 'concRegValue'. +-- +-- Unlike What4\'s 'W4GE.GroundValue', this type family is parameterized +-- by @sym@, the symbolic backend. This is because Crucible makes use of +-- \"interpreted\" floating point numbers ('SymInterpretedFloatType'). What4\'s +-- @SymFloat@ always uses an IEEE-754 interpretation of symbolic floats, whereas +-- 'SymInterpretedFloatType' can use IEEE-754, real numbers, or uninterpreted +-- functions depending on how the symbolic backend is configured. type ConcRegValue :: Type -> CrucibleType -> Type type family ConcRegValue sym tp where ConcRegValue sym (BaseToType bt) = W4GE.GroundValue bt @@ -81,15 +89,15 @@ type family ConcRegValue sym tp where ConcRegValue sym CharType = Word16 ConcRegValue sym (FunctionHandleType a r) = ConcFnVal sym a r ConcRegValue sym (MaybeType tp) = Maybe (ConcRegValue sym tp) - ConcRegValue sym (VectorType tp) = V.Vector (ConcRegValue' sym tp) - ConcRegValue sym (SequenceType tp) = [ConcRegValue' sym tp] - ConcRegValue sym (StructType ctx) = Ctx.Assignment (ConcRegValue' sym) ctx + ConcRegValue sym (VectorType tp) = V.Vector (ConcRV' sym tp) + ConcRegValue sym (SequenceType tp) = [ConcRV' sym tp] + ConcRegValue sym (StructType ctx) = Ctx.Assignment (ConcRV' sym) ctx ConcRegValue sym (VariantType ctx) = Ctx.Assignment (ConcVariantBranch sym) ctx ConcRegValue sym (ReferenceType tp) = [RefCell tp] ConcRegValue sym (WordMapType w tp) = () -- TODO: possible to do something meaningful? ConcRegValue sym (RecursiveType nm ctx) = ConcRegValue sym (UnrollType nm ctx) ConcRegValue sym (IntrinsicType nm ctx) = ConcIntrinsic nm ctx - ConcRegValue sym (StringMapType tp) = Map Text (ConcRegValue' sym tp) + ConcRegValue sym (StringMapType tp) = Map Text (ConcRV' sym tp) --------------------------------------------------------------------- -- * ConcCtx @@ -204,7 +212,7 @@ tryConcIntrinsic ctx nm tyCtx v = do -- * Any -- | An 'AnyValue' concretized by 'concRegValue' -data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRegValue' sym tp) +data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRV' sym tp) --------------------------------------------------------------------- -- * FnVal @@ -214,7 +222,7 @@ data ConcFnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) wh ConcClosureFnVal :: !(ConcFnVal sym (args ::> tp) ret) -> !(TypeRepr tp) -> - !(ConcRegValue' sym tp) -> + !(ConcRV' sym tp) -> ConcFnVal sym args ret ConcVarargsFnVal :: @@ -240,7 +248,7 @@ concFnVal ctx args ret = RV.ClosureFnVal fv t v -> do concV <- concFnVal ctx (args Ctx.:> t) ret fv v' <- concRegValue ctx t v - pure (ConcClosureFnVal concV t (ConcRegValue' v')) + pure (ConcClosureFnVal concV t (ConcRV' v')) RV.VarargsFnVal hdl extra -> pure (ConcVarargsFnVal hdl extra) RV.HandleFnVal hdl -> @@ -273,13 +281,13 @@ concSymSequence :: ConcCtx sym t -> TypeRepr tp -> SymSeq.SymSequence sym (RegValue sym tp) -> - IO [ConcRegValue' sym tp] + IO [ConcRV' sym tp] concSymSequence ctx tp = \case SymSeq.SymSequenceNil -> pure [] SymSeq.SymSequenceCons _nonce v rest -> do v' <- concRegValue ctx tp v - (ConcRegValue' v' :) <$> concSymSequence ctx tp rest + (ConcRV' v' :) <$> concSymSequence ctx tp rest SymSeq.SymSequenceAppend _nonce xs ys -> (++) <$> concSymSequence ctx tp xs <*> concSymSequence ctx tp ys SymSeq.SymSequenceMerge _nonce p ts fs -> @@ -295,7 +303,7 @@ concStringMap :: ConcCtx sym t -> TypeRepr tp -> RegValue sym (StringMapType tp) -> - IO (Map Text (ConcRegValue' sym tp)) + IO (Map Text (ConcRV' sym tp)) concStringMap ctx tp v = Map.fromList <$> go (Map.toList v) where go [] = pure [] @@ -303,7 +311,7 @@ concStringMap ctx tp v = Map.fromList <$> go (Map.toList v) concPartialWithErr ctx tp v' >>= \case Nothing -> go xs - Just v'' -> ((t, ConcRegValue' v''):) <$> go xs + Just v'' -> ((t, ConcRV' v''):) <$> go xs --------------------------------------------------------------------- -- * Variant @@ -312,7 +320,7 @@ concStringMap ctx tp v = Map.fromList <$> go (Map.toList v) -- in any way. If the model reports that multiple branches of a variant are -- plausible, then multiple branches might be included as 'Just's. newtype ConcVariantBranch sym tp - = ConcVariantBranch (Maybe (ConcRegValue' sym tp)) + = ConcVariantBranch (Maybe (ConcRV' sym tp)) -- | Helper, not exported concVariant :: @@ -329,7 +337,7 @@ concVariant ctx tps vs = Ctx.zipWithM concBranch tps vs concBranch tp (RV.VB v) = do v' <- concPartialWithErr ctx tp v case v' of - Just v'' -> pure (ConcVariantBranch (Just (ConcRegValue' v''))) + Just v'' -> pure (ConcVariantBranch (Just (ConcRV' v''))) Nothing -> pure (ConcVariantBranch Nothing) --------------------------------------------------------------------- @@ -368,13 +376,13 @@ concRegValue ctx tp v = -- Simple recursive cases (AnyRepr, RV.AnyValue tp' v') -> - ConcAnyValue tp' . ConcRegValue' <$> concRegValue ctx tp' v' + ConcAnyValue tp' . ConcRV' <$> concRegValue ctx tp' v' (RecursiveRepr symb tyCtx, RV.RolledType v') -> concRegValue ctx (unrollType symb tyCtx) v' (StructRepr tps, _) -> - Ctx.zipWithM (\tp' (RV.RV v') -> ConcRegValue' <$> concRegValue ctx tp' v') tps v + Ctx.zipWithM (\tp' (RV.RV v') -> ConcRV' <$> concRegValue ctx tp' v') tps v (VectorRepr tp', _) -> - traverse (fmap ConcRegValue' . concRegValue ctx tp') v + traverse (fmap ConcRV' . concRegValue ctx tp') v -- Cases with helper functions (MaybeRepr tp', _) -> @@ -383,7 +391,9 @@ concRegValue ctx tp v = concFnVal ctx args ret v (IntrinsicRepr nm tyCtx, _) -> case tryConcIntrinsic ctx nm tyCtx v of - Nothing -> fail "Missing concretization function for intrinsic!" + Nothing -> + let strNm = Text.unpack (symbolRepr nm) in + fail ("Missing concretization function for intrinsic: " ++ strNm) Just r -> r (ReferenceRepr _, _) -> concMux ctx v From eb8c20eb6b9ab685af51aa1de27f19edaeb6cafd Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 6 Jun 2024 11:56:06 -0400 Subject: [PATCH 8/8] Fix more confused type variables --- .../src/Lang/Crucible/LLVM/MemModel/Pointer.hs | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs index 68a4fe4b9..559c97aca 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs @@ -227,12 +227,7 @@ concPtr' sym conc (RV ptr) = RV <$> concPtr sym conc ptr type instance Conc.ConcIntrinsic "LLVM_pointer" (EmptyCtx ::> BVType w) = ConcLLVMPtr w -- | An 'Conc.IntrinsicConcFn' for LLVM pointers -concPtrFn :: - forall sym. - ( IsExprBuilder sym - , SymExpr sym ~ Expr sym - ) => - Conc.IntrinsicConcFn sym "LLVM_pointer" +concPtrFn :: Conc.IntrinsicConcFn t "LLVM_pointer" concPtrFn = Conc.IntrinsicConcFn $ \ctx tyCtx ptr -> case Ctx.viewAssign tyCtx of Ctx.AssignExtend (Ctx.viewAssign -> Ctx.AssignEmpty) (BVRepr _) -> @@ -248,12 +243,7 @@ concPtrFn = Conc.IntrinsicConcFn $ \ctx tyCtx ptr -> -- | A singleton map suitable for use in a 'Conc.ConcCtx' if LLVM pointers are -- the only intrinsic type in use -concPtrFnMap :: - forall sym. - ( IsExprBuilder sym - , SymExpr sym ~ Expr sym - ) => - MapF.MapF SymbolRepr (Conc.IntrinsicConcFn sym) +concPtrFnMap :: MapF.MapF SymbolRepr (Conc.IntrinsicConcFn t) concPtrFnMap = MapF.singleton (knownSymbol @"LLVM_pointer") concPtrFn -- | Mux function specialized to LLVM pointer values.