From 92654db8279a4b29c08b3ba0fd113a6f8888dc92 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 13 Jun 2022 16:01:45 -0400 Subject: [PATCH 01/40] uc-crux-llvm: Serialization for Preconds --- uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs | 1 + uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs | 204 ++++++++++++++++++ uc-crux-llvm/uc-crux-llvm.cabal | 1 + 3 files changed, 206 insertions(+) create mode 100644 uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs index a63763904..14a404aaf 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs @@ -27,6 +27,7 @@ module UCCrux.LLVM.View.Postcond viewClobberArg, clobberArgView, -- * UPostcond + UPostcondView(..), ViewUPostcondError, ppViewUPostcondError, viewUPostcond, diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs new file mode 100644 index 000000000..0aa20474c --- /dev/null +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs @@ -0,0 +1,204 @@ +{- +Module : UCCrux.LLVM.View.Precond +Description : See "UCCrux.LLVM.View". +Copyright : (c) Galois, Inc 2022 +License : BSD3 +Maintainer : Langston Barrett +Stability : provisional +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StrictData #-} +{-# LANGUAGE TemplateHaskell #-} + +module UCCrux.LLVM.View.Precond + ( PrecondsView(..), + ViewPrecondsError, + ppViewPrecondsError, + viewPreconds, + precondsView, + ) +where + +import Control.Lens ((^.)) +import qualified Data.Aeson as Aeson +import qualified Data.Aeson.TH as Aeson.TH +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Data.Text as Text +import Data.Vector (Vector) +import qualified Data.Vector as Vec +import GHC.Generics (Generic) + +import Prettyprinter (Doc) +import qualified Prettyprinter as PP + +import qualified Text.LLVM.AST as L + +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.TraversableFC (toListFC) +import Data.Parameterized.TraversableFC.WithIndex (itraverseFC) +import Data.Parameterized.Some (Some(Some)) + +import UCCrux.LLVM.Constraints (ConstrainedShape) +import UCCrux.LLVM.Context.Module (ModuleContext, llvmModule, moduleTypes, funcTypes) +import UCCrux.LLVM.Precondition (Preconds(..), argPreconds, globalPreconds, postconds) +import UCCrux.LLVM.FullType.FuncSig (FuncSigRepr) +import qualified UCCrux.LLVM.FullType.FuncSig as FS +import UCCrux.LLVM.FullType.Type (FullTypeRepr(..)) +import UCCrux.LLVM.Module (funcSymbolToString, globalSymbolToString, makeFuncSymbol, makeGlobalSymbol, moduleGlobalMap, funcSymbol) +import UCCrux.LLVM.View.Constraint (ViewConstrainedShapeError, ConstrainedShapeView, ConstrainedTypedValueViewError, ConstrainedTypedValueView, constrainedShapeView, viewConstrainedShape, ppViewConstrainedShapeError, viewConstrainedTypedValue, constrainedTypedValueView, ppConstrainedTypedValueViewError) +import UCCrux.LLVM.View.Shape (ViewShapeError, ppViewShapeError) +import UCCrux.LLVM.View.Postcond (UPostcondView(..), uPostcondView, viewUPostcond, ViewUPostcondError, ppViewUPostcondError) +import UCCrux.LLVM.View.Util (FuncName(..), GlobalVarName(..)) + +-- Helper, not exported. Equivalent to Data.Bifunctor.first. +liftError :: (e -> i) -> Either e a -> Either i a +liftError l = + \case + Left e -> Left (l e) + Right v -> Right v + +-- Helper, not exported +liftMaybe :: e -> Maybe a -> Either e a +liftMaybe err = + \case + Nothing -> Left err + Just v -> Right v + +-------------------------------------------------------------------------------- +-- * ClobberValue + +data ViewPrecondsError + = PrecondArgError ArgError + | NonExistentGlobal GlobalVarName + | NonExistentFunc FuncName + | GlobalError GlobalVarName ConstrainedTypedValueViewError + | PostcondError FuncName ViewUPostcondError + +ppViewPrecondsError :: ViewPrecondsError -> Doc ann +ppViewPrecondsError = + \case + PrecondArgError ae -> ppArgError ae + NonExistentGlobal glob -> + "Non-existent global: " <> PP.pretty (getGlobalVarName glob) + NonExistentFunc func -> + "Non-existent function: " <> PP.pretty (getFuncName func) + GlobalError glob err -> + PP.hsep + [ "Error in spec for global" + , "`" <> PP.pretty (getGlobalVarName glob) <> "`:" + , ppConstrainedTypedValueViewError err + ] + PostcondError func err -> + PP.hsep + [ "Error in postcondition for function" + , "`" <> PP.pretty (getFuncName func) <> "`:" + , ppViewUPostcondError err + ] + +data PrecondsView = + PrecondsView + { vArgPreconds :: Vector ConstrainedShapeView, + vGlobalPreconds :: Map GlobalVarName ConstrainedTypedValueView, + vPostconds :: Map FuncName UPostcondView + } + deriving (Eq, Ord, Generic, Show) + +precondsView :: Preconds m argTypes -> PrecondsView +precondsView pres = + PrecondsView + { vArgPreconds = + Vec.fromList (toListFC constrainedShapeView (pres ^. argPreconds)), + vGlobalPreconds = + mapKV viewGSymb constrainedTypedValueView (pres ^. globalPreconds), + vPostconds = + mapKV viewFSymb uPostcondView (pres ^. postconds) + } + where + viewFSymb = FuncName . Text.pack . funcSymbolToString + viewGSymb = GlobalVarName . Text.pack . globalSymbolToString + mapKV k v m = Map.mapKeys k (Map.map v m) + +data ArgError + = NotEnoughArgs Int + | BadArg (ViewShapeError ViewConstrainedShapeError) + +ppArgError :: ArgError -> Doc ann +ppArgError = + \case + NotEnoughArgs i -> + PP.hsep + [ "Not enough argument specs provided for in precondition for function" + , "found:" + , "(" <> PP.viaShow i <> ")" + ] + BadArg err -> + PP.hsep + [ "Problem with specification for argument in precondition:" + , ppViewShapeError ppViewConstrainedShapeError err + ] + +viewPreconds :: + forall m arch fs va ret args. + (fs ~ 'FS.FuncSig va ret args) => + ModuleContext m arch -> + FuncSigRepr m fs -> + PrecondsView -> + Either ViewPrecondsError (Preconds m args) +viewPreconds modCtx fs vpres = + do let genArg :: + forall ft. + Ctx.Index args ft -> + FullTypeRepr m ft -> + Either ArgError (ConstrainedShape m ft) + genArg i ft = + case vArgPreconds vpres Vec.!? Ctx.indexVal i of + Nothing -> Left (NotEnoughArgs (Ctx.indexVal i)) + Just val -> + liftError BadArg (viewConstrainedShape mts ft val) + args <- liftError PrecondArgError (itraverseFC genArg (FS.fsArgTypes fs)) + + globs <- traverse (uncurry viewGlob) (Map.toList (vGlobalPreconds vpres)) + posts <- traverse (uncurry viewPost) (Map.toList (vPostconds vpres)) + return $ + Preconds + { _argPreconds = args, + _globalPreconds = Map.fromList globs, + _postconds = Map.fromList posts, + _relationalPreconds = [] + } + where + m = modCtx ^. llvmModule + mts = modCtx ^. moduleTypes + mkSymbol = L.Symbol . Text.unpack + + viewGlob gn@(GlobalVarName nm) vglob = + do gSymb <- + liftMaybe + (NonExistentGlobal gn) + (makeGlobalSymbol (moduleGlobalMap m) (mkSymbol nm)) + glob <- + liftError (GlobalError gn) (viewConstrainedTypedValue mts vglob) + return (gSymb, glob) + + viewPost fn@(FuncName nm) vpost = + do let funcTys = modCtx ^. funcTypes + fSymb <- + liftMaybe + (NonExistentFunc fn) + (makeFuncSymbol (mkSymbol nm) funcTys) + Some fsRep@FS.FuncSigRepr{} <- return (funcTys ^. funcSymbol fSymb) + post <- + liftError + (PostcondError fn) + (viewUPostcond modCtx fsRep vpost) + return (fSymb, post) + +$(Aeson.TH.deriveJSON Aeson.defaultOptions ''PrecondsView) diff --git a/uc-crux-llvm/uc-crux-llvm.cabal b/uc-crux-llvm/uc-crux-llvm.cabal index daadb14dc..6476cf863 100644 --- a/uc-crux-llvm/uc-crux-llvm.cabal +++ b/uc-crux-llvm/uc-crux-llvm.cabal @@ -99,6 +99,7 @@ library UCCrux.LLVM.View.Cursor UCCrux.LLVM.View.FullType UCCrux.LLVM.View.Postcond + UCCrux.LLVM.View.Precond UCCrux.LLVM.View.Shape UCCrux.LLVM.View.TH UCCrux.LLVM.View.Util From 3d4b203a744c96c60401733bad0903c429df989c Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 14 Jun 2022 09:50:24 -0400 Subject: [PATCH 02/40] uc-crux-llvm: Towards user specs for extern funcs Still needs: - Code-level docs - User-facing docs - Integration with Loop - Integration with the CLI - Ideally, some tests --- uc-crux-llvm/.hlint.yaml | 3 + uc-crux-llvm/src/UCCrux/LLVM/Check.hs | 4 +- .../src/UCCrux/LLVM/Overrides/Spec.hs | 157 +++++++++++++++ .../src/UCCrux/LLVM/Postcondition/Type.hs | 36 ++++ uc-crux-llvm/src/UCCrux/LLVM/Precondition.hs | 3 +- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 177 +++++++++++++++++ uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs | 98 ++++++++++ uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs | 38 ++-- uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs | 185 ++++++++++++++++++ uc-crux-llvm/uc-crux-llvm.cabal | 4 + 10 files changed, 691 insertions(+), 14 deletions(-) create mode 100644 uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs create mode 100644 uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs create mode 100644 uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs create mode 100644 uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs diff --git a/uc-crux-llvm/.hlint.yaml b/uc-crux-llvm/.hlint.yaml index 43f22916f..a924ea95c 100644 --- a/uc-crux-llvm/.hlint.yaml +++ b/uc-crux-llvm/.hlint.yaml @@ -79,6 +79,9 @@ name: "Use void" within: - "UCCrux.LLVM.View.Shape" +- ignore: # "SpecPreconds" should be extensible with more fields + name: "Use newtype instead of data" + within: ["UCCrux.LLVM.Specs.Type"] - ignore: # False positive - Template Haskell name: "Redundant bracket" within: diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Check.hs b/uc-crux-llvm/src/UCCrux/LLVM/Check.hs index 5efd8fab8..5c5f42821 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Check.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Check.hs @@ -9,7 +9,9 @@ Stability : provisional Create predicates that represent whether or not a set of constraints ('ConstrainedShape') hold of some Crucible value ('Crucible.RegValue') in some LLVM memory ('LLVMMem.MemImpl'). These predicates are used in "check overrides" -("UCCrux.LLVM.Overrides.Check"). +("UCCrux.LLVM.Overrides.Check"), and when applying function specs +("UCCrux.LLVM.Specs.Apply"). + -} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs new file mode 100644 index 000000000..e15c259f7 --- /dev/null +++ b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs @@ -0,0 +1,157 @@ +{- +Module : UCCrux.LLVM.Overrides.Spec +Description : Overrides for skipping execution of functions with user-provided specs +Copyright : (c) Galois, Inc 2022 +License : BSD3 +Maintainer : Langston Barrett +Stability : provisional + +TODO(lb): Track which specs actually execute and whether they are over- or +under-approximate. +-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module UCCrux.LLVM.Overrides.Spec + ( specOverrides, + createSpecOverride, + ) +where + +{- ORMOLU_DISABLE -} +import Control.Lens ((^.)) +import Data.IORef (IORef) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Type.Equality ((:~:)(Refl)) + +-- parameterized-utils +import qualified Data.Parameterized.Context as Ctx + +-- what4 + +-- crucible +import Lang.Crucible.Backend (IsSymBackend) +import qualified Lang.Crucible.Simulator as Crucible + +-- crucible-llvm +import Lang.Crucible.LLVM.Extension (LLVM) +import Lang.Crucible.LLVM.MemModel (HasLLVMAnn, Mem, MemOptions) +import Lang.Crucible.LLVM.Translation (ModuleTranslation, transContext, llvmTypeCtx) +import Lang.Crucible.LLVM.TypeContext (TypeContext) +import Lang.Crucible.LLVM.Intrinsics (LLVMOverride(..), basic_llvm_override) + +import Crux.Types (OverM) + +-- crux-llvm +import Crux.LLVM.Overrides (ArchOk) + +-- uc-crux-llvm +import UCCrux.LLVM.Context.Module (ModuleContext, moduleDecls) +import UCCrux.LLVM.FullType.CrucibleType (SomeAssign'(..), assignmentToCrucibleType, toCrucibleReturnType) +import UCCrux.LLVM.ExprTracker (ExprTracker) +import UCCrux.LLVM.FullType.FuncSig (FuncSigRepr(FuncSigRepr)) +import qualified UCCrux.LLVM.FullType.FuncSig as FS +import UCCrux.LLVM.FullType.Type (MapToCrucibleType) +import UCCrux.LLVM.Module (FuncSymbol, funcSymbol) +import UCCrux.LLVM.Overrides.Polymorphic (PolymorphicLLVMOverride, makePolymorphicLLVMOverride) +import qualified UCCrux.LLVM.Specs.Apply as Spec +import UCCrux.LLVM.Specs.Type (SomeSpecs) +import qualified UCCrux.LLVM.Specs.Type as Spec +{- ORMOLU_ENABLE -} + +-- | Additional overrides that are useful for bugfinding, but not for +-- verification. They skip execution of the specified functions. +-- +-- Mostly useful for functions that are declared but not defined. +specOverrides :: + IsSymBackend sym bak => + HasLLVMAnn sym => + ArchOk arch => + (?lc :: TypeContext) => + (?memOpts :: MemOptions) => + ModuleContext m arch -> + bak -> + ModuleTranslation arch -> + -- | Origins of created values + IORef (ExprTracker m sym argTypes) -> + -- | Specs of each override, see 'Specs'. + Map (FuncSymbol m) (SomeSpecs m) -> + OverM personality sym LLVM [PolymorphicLLVMOverride arch (personality sym) sym] +specOverrides modCtx bak mtrans tracker specs = + do + let llvmCtx = mtrans ^. transContext + let ?lc = llvmCtx ^. llvmTypeCtx + let create funcSymb (Spec.SomeSpecs fsRep@FuncSigRepr{} specs') = + createSpecOverride modCtx bak tracker funcSymb fsRep specs' + pure $ map (uncurry create) (Map.toList specs) + +-- | Boilerplate to create an LLVM override +mkOverride :: + IsSymBackend sym bak => + HasLLVMAnn sym => + ArchOk arch => + (fs ~ 'FS.FuncSig va mft args) => + ModuleContext m arch -> + proxy bak -> + -- | Function to be overridden + FuncSymbol m -> + -- | Type of function to be overridden + FS.FuncSigRepr m fs -> + -- | Implementation + (forall rtp a r. + Crucible.GlobalVar Mem -> + Ctx.Assignment (Crucible.RegEntry sym) (MapToCrucibleType arch args) -> + Crucible.OverrideSim (personality sym) sym LLVM rtp a r + (Crucible.RegValue sym (FS.ReturnTypeToCrucibleType arch mft))) -> + PolymorphicLLVMOverride arch (personality sym) sym +mkOverride modCtx _proxy funcSymb (FuncSigRepr _ argFTys retTy) impl = + case assignmentToCrucibleType modCtx argFTys of + SomeAssign' argTys Refl _ -> + makePolymorphicLLVMOverride $ + basic_llvm_override $ + LLVMOverride + { llvmOverride_declare = decl, + llvmOverride_args = argTys, + llvmOverride_ret = toCrucibleReturnType modCtx retTy, + llvmOverride_def = + \mvar _sym args -> impl mvar args + } + where decl = modCtx ^. moduleDecls . funcSymbol funcSymb + +-- | Create an override that takes the place of a given defined or even +-- declared/external function, and instead of executing that function, +-- instead manufactures a fresh symbolic return value and optionally clobbers +-- some parts of its arguments or global variables with fresh symbolic values. +-- +-- Useful for continuing symbolic execution in the presence of external/library +-- functions. +createSpecOverride :: + forall m arch sym bak fs va mft args argTypes personality. + IsSymBackend sym bak => + HasLLVMAnn sym => + ArchOk arch => + (?lc :: TypeContext) => + (?memOpts :: MemOptions) => + (fs ~ 'FS.FuncSig va mft args) => + ModuleContext m arch -> + bak -> + -- | Origins of created values + IORef (ExprTracker m sym argTypes) -> + -- | Function to be overridden + FuncSymbol m -> + -- | Type of function to be overridden + FS.FuncSigRepr m fs -> + -- | Constraints on the return value, clobbered pointer values such as + -- arguments or global variables + Spec.Specs m fs -> + PolymorphicLLVMOverride arch (personality sym) sym +createSpecOverride modCtx bak tracker funcSymb fsRep specs = + mkOverride modCtx (Just bak) funcSymb fsRep $ + \mvar args -> + Spec.applySpecs bak modCtx tracker funcSymb specs fsRep mvar args diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Postcondition/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Postcondition/Type.hs index 1a201c492..d697d08f8 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Postcondition/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Postcondition/Type.hs @@ -50,12 +50,14 @@ module UCCrux.LLVM.Postcondition.Type , uReturnValue , emptyUPostcond , minimalUPostcond + , minimalPostcond , ppUPostcond , Postcond(..) , PostcondTypeError , ppPostcondTypeError , typecheckPostcond , ReturnValue(..) + , toUPostcond ) where @@ -72,9 +74,11 @@ import qualified Prettyprinter as PP import Data.Parameterized.Classes (IxedF'(ixF')) import Data.Parameterized.Context (Assignment) import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.TraversableFC.WithIndex (ifoldrFC) import UCCrux.LLVM.Constraints (ConstrainedShape, ConstrainedTypedValue(ConstrainedTypedValue), minimalConstrainedShape, ppConstrainedShape) import UCCrux.LLVM.Cursor (Cursor, ppCursor) +import UCCrux.LLVM.Errors.Panic (panic) import UCCrux.LLVM.FullType.CrucibleType (SameCrucibleType, sameCrucibleType, makeSameCrucibleType, testSameCrucibleType) import UCCrux.LLVM.FullType.FuncSig (FuncSig, FuncSigRepr, ReturnTypeRepr) import qualified UCCrux.LLVM.FullType.FuncSig as FS @@ -210,6 +214,22 @@ data Postcond m (fs :: FuncSig m) where } -> Postcond m ('FS.FuncSig va mft argTypes) +-- | A postcondition which imposes no constraints and has some +-- minimally-constrained return value. +minimalPostcond :: + (fs ~ 'FS.FuncSig va mft args) => + FuncSigRepr m fs -> + Postcond m fs +minimalPostcond fsRepr@(FS.FuncSigRepr _ _ retRepr) = + case typecheckPostcond (minimalUPostcond retRepr) fsRepr of + Left err -> + panic + "minimalPostcond" + [ "Impossible: type mismatch on fresh postcond!" + , show (ppPostcondTypeError err) + ] + Right val -> val + data RetMismatch = BadRetType | FunctionWasVoid @@ -315,3 +335,19 @@ typecheckPostcond post fs = pGlobalClobbers = _uGlobalClobbers post, pReturnValue = ret } + +-- | Inverse of 'typecheckPostcond' +toUPostcond :: FuncSigRepr m fs -> Postcond m fs -> UPostcond m +toUPostcond (FS.FuncSigRepr _ _ retTy) (Postcond _ argClob globClob ret) = + UPostcond + { _uArgClobbers = ifoldrFC mkArg IntMap.empty argClob, + _uGlobalClobbers = globClob, + _uReturnValue = + case (ret, retTy) of + (ReturnVoid, FS.VoidRepr) -> Nothing + (ReturnValue val, FS.NonVoidRepr retTyRep) -> + Just (ConstrainedTypedValue retTyRep val) + } + where + mkArg idx arg intMap = + IntMap.insert (Ctx.indexVal idx) (SomeClobberArg arg) intMap diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Precondition.hs b/uc-crux-llvm/src/UCCrux/LLVM/Precondition.hs index d5b1592d1..c124ecbb8 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Precondition.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Precondition.hs @@ -21,6 +21,7 @@ module UCCrux.LLVM.Precondition globalPreconds, postconds, relationalPreconds, + emptyArgPreconds, emptyPreconds, ppPreconds, isEmpty, @@ -370,7 +371,7 @@ addPrecond modCtx argTypes constraints = Lens.IxValue c -> Lens.Lens' c (Lens.IxValue c) atDefault idx def = at idx . fromMaybeL def - + addOneConstraint :: Constraint m atTy -> ConstrainedShape m ft -> diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs new file mode 100644 index 000000000..18154e001 --- /dev/null +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -0,0 +1,177 @@ +{- +Module : UCCrux.LLVM.Specs.Apply +Description : Apply collections of specifications for LLVM functions +Copyright : (c) Galois, Inc 2022 +License : BSD3 +Maintainer : Langston Barrett +Stability : provisional + +TODO(lb): Improve tracking + logging of when specs failed to apply, and why. +Should be easy enough given the information in 'CheckedConstraint'. +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} + +module UCCrux.LLVM.Specs.Apply + ( applySpecs + ) +where + +{- ORMOLU_DISABLE -} +import Prelude hiding (zip) + +import qualified Control.Lens as Lens +import Control.Monad.IO.Class (liftIO) +import Data.Maybe (fromMaybe) +import Data.Foldable (toList) +import Data.IORef (IORef) + +-- parameterized-utils +import qualified Data.Parameterized.Context as Ctx + +-- what4 +import qualified What4.Interface as What4 + +-- crucible +import qualified Lang.Crucible.Backend as Crucible +import Lang.Crucible.Backend (IsSymInterface) +import qualified Lang.Crucible.Simulator as Crucible + +-- crucible-llvm +import Lang.Crucible.LLVM.MemModel (HasLLVMAnn, Mem, MemImpl, MemOptions) +import Lang.Crucible.LLVM.TypeContext (TypeContext) + +-- crux-llvm +import Crux.LLVM.Overrides (ArchOk) + +-- uc-crux-llvm +import UCCrux.LLVM.Check (checkConstrainedShapes, SomeCheckedConstraint(..), CheckedConstraint(checkedPred)) +import UCCrux.LLVM.Context.Module (ModuleContext) +import UCCrux.LLVM.ExprTracker (ExprTracker) +import qualified UCCrux.LLVM.FullType.FuncSig as FS +import UCCrux.LLVM.FullType.Type (FullTypeRepr, MapToCrucibleType) +import UCCrux.LLVM.Module (FuncSymbol) +import UCCrux.LLVM.Postcondition.Apply (applyPostcond) +import qualified UCCrux.LLVM.Postcondition.Type as Post +import UCCrux.LLVM.Specs.Type (Specs) +import qualified UCCrux.LLVM.Specs.Type as Spec +{- ORMOLU_ENABLE -} + +-- | Collapse all the preconditions of a 'Spec' to a single predicate +matchPreconds :: + IsSymInterface sym => + HasLLVMAnn sym => + ArchOk arch => + (?memOpts :: MemOptions) => + ModuleContext m arch -> + sym -> + MemImpl sym -> + Ctx.Assignment (FullTypeRepr m) argTypes -> + Spec.SpecPreconds m argTypes -> + Ctx.Assignment (Crucible.RegEntry sym) (MapToCrucibleType arch argTypes) -> + IO (What4.Pred sym) +matchPreconds modCtx sym mem argFTys preconds args = + do constraints <- + checkConstrainedShapes modCtx sym mem argFTys (Spec.specArgPreconds preconds) args + What4.andAllOf + sym + (Lens.folding (fmap (\(SomeCheckedConstraint c) -> checkedPred c))) + constraints + +-- | Apply a spec postcondition, modifying memory and creating a return value +-- +-- If the postcondition of the spec is 'Nothing', apply 'Post.minimalPostcond'. +applyPost :: + forall m arch sym bak fs va mft args argTypes p ext r cargs ret. + Crucible.IsSymBackend sym bak => + IsSymInterface sym => + HasLLVMAnn sym => + ArchOk arch => + (?lc :: TypeContext) => + (?memOpts :: MemOptions) => + (fs ~ 'FS.FuncSig va mft args) => + bak -> + ModuleContext m arch -> + -- | Track origins of created values + IORef (ExprTracker m sym argTypes) -> + -- | Function name + FuncSymbol m -> + -- | Function type + FS.FuncSigRepr m fs -> + -- | LLVM memory variable + Crucible.GlobalVar Mem -> + Spec.Spec m fs -> + -- | Arguments to function + Ctx.Assignment (Crucible.RegEntry sym) (MapToCrucibleType arch args) -> + Crucible.OverrideSim p sym ext r cargs ret + (Crucible.RegValue sym (FS.ReturnTypeToCrucibleType arch mft)) +applyPost bak modCtx tracker funcSymb fsRep mvar spec args = + do FS.FuncSigRepr _ _ retTy <- return fsRep + Spec.Spec _ _ specPost _ <- return spec + let post = fromMaybe (Post.minimalPostcond fsRep) specPost + Crucible.modifyGlobal mvar $ \mem -> + liftIO (applyPostcond bak modCtx tracker funcSymb post retTy mem args) + +applySpecs :: + forall m arch sym bak fs va mft args argTypes p ext r cargs ret. + ArchOk arch => + HasLLVMAnn sym => + (?lc :: TypeContext) => + (?memOpts :: MemOptions) => + (fs ~ 'FS.FuncSig va mft args) => + Crucible.IsSymBackend sym bak => + bak -> + ModuleContext m arch -> + -- | Track origins of created values + IORef (ExprTracker m sym argTypes) -> + -- | Function name + FuncSymbol m -> + -- | Function specs + Specs m fs -> + -- | Function type + FS.FuncSigRepr m fs -> + -- | LLVM memory variable + Crucible.GlobalVar Mem -> + -- | Arguments to function + Ctx.Assignment (Crucible.RegEntry sym) (MapToCrucibleType arch args) -> + Crucible.OverrideSim p sym ext r cargs ret + (Crucible.RegValue sym (FS.ReturnTypeToCrucibleType arch mft)) +applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = + do FS.FuncSigRepr _ argTys _ <- return fsRep + let sym = Crucible.backendGetSym bak + + -- Collapse preconditions into predicates + mem <- Crucible.readGlobal mvar + let matchPre (Spec.Spec specPre _ _ _) = + matchPreconds modCtx sym mem argTys specPre args + specs' <- + traverse (\s -> (s,) <$> liftIO (matchPre s)) (Spec.getSpecs specs) + + -- Create one symbolic branch per Spec, conditioned on the preconditions + let specBranches = + [ ( precond + , applyPost bak modCtx tracker funcSymb fsRep mvar spec args + , Nothing + ) + | (spec, precond) <- toList specs' + ] + + -- Add a fallback branch that (depending on the Spec) either fails or + -- applies a minimal postcondition. + let fallbackBranch = + ( What4.truePred sym + , liftIO $ do + -- TODO(lb): this behavior should depend on spec config + Crucible.addFailedAssertion + bak + (Crucible.GenericSimError "No spec applied!") + , Nothing + ) + + let branches = specBranches ++ [fallbackBranch] + Crucible.symbolicBranches Crucible.emptyRegMap branches diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs new file mode 100644 index 000000000..05f450fec --- /dev/null +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs @@ -0,0 +1,98 @@ +{- +Module : UCCrux.LLVM.Specs.Type +Description : Collections of specifications for LLVM functions +Copyright : (c) Galois, Inc 2022 +License : BSD3 +Maintainer : Langston Barrett +Stability : provisional + +* TODO(lb): +* User-provided +* Matching behavior +* Pre- and post- +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} + +module UCCrux.LLVM.Specs.Type + ( SpecPreconds(..), + SpecSoundness(..), + Spec(..), + Specs(..), + SomeSpecs(..), + minimalSpec, + minimalSpecs + ) +where + +import Data.List.NonEmpty (NonEmpty) +import qualified Data.List.NonEmpty as NE + +import Data.Parameterized.Context (Ctx) +import qualified Data.Parameterized.Context as Ctx + +import UCCrux.LLVM.Constraints (ConstrainedShape) +import UCCrux.LLVM.FullType.Type (FullType) +import qualified UCCrux.LLVM.FullType.FuncSig as FS +import UCCrux.LLVM.Precondition (emptyArgPreconds) +import UCCrux.LLVM.Postcondition.Type (Postcond) + +-- TODO(lb): preconds on globals +data SpecPreconds m (args :: Ctx (FullType m)) + = SpecPreconds + { specArgPreconds :: Ctx.Assignment (ConstrainedShape m) args } + +data SpecSoundness + = -- | For preconditions, means that the specified preconditions are more + -- restrictive than the actual implementation. For postconditions, means + -- that the specified postcondition encapsulates all possible effects of + -- the implementation on the program state. + Overapprox + -- | For preconditions, means that the specified preconditions are less + -- restrictive than the actual implementation. For postconditions, means + -- that the specified postcondition encapsulates some definitely possible + -- effects of the implementation on the program state. + | Underapprox + -- | Both over-approximate and under-approximate + | Precise + -- | Neither over-approximate nor under-approximate + | Imprecise + deriving (Bounded, Enum, Eq, Ord, Show) + +-- TODO(lb): docs +data Spec m fs + = forall va ret args. (fs ~ 'FS.FuncSig va ret args) => + Spec + { specPre :: SpecPreconds m args + , specPreSound :: SpecSoundness + , specPost :: Maybe (Postcond m fs) + , specPostSound :: SpecSoundness + } + +-- TODO(lb): docs +newtype Specs m fs + = Specs { getSpecs :: NonEmpty (Spec m fs) } + +-- | This is a bit inefficient, could avoid duplicating all the 'FuncSigRepr's +-- with one of the strategies outlined in +-- https://github.com/GaloisInc/crucible/issues/982. +data SomeSpecs m = forall fs. SomeSpecs (FS.FuncSigRepr m fs) (Specs m fs) + +-- | The minimal spec - one with no preconditions which produces a fresh, +-- minimal, symbolic return value. +minimalSpec :: FS.FuncSigRepr m fs -> Spec m fs +minimalSpec (FS.FuncSigRepr _ args _) = + Spec + { specPre = SpecPreconds (emptyArgPreconds args) + , specPreSound = Underapprox + , specPost = Nothing + , specPostSound = Imprecise + } + +-- | The minimal set of specs - just 'minimalSpec'. +minimalSpecs :: FS.FuncSigRepr m fs -> Specs m fs +minimalSpecs = Specs . NE.singleton . minimalSpec + +-- TODO(lb): views diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs index 0aa20474c..4ee1b9963 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs @@ -21,6 +21,9 @@ module UCCrux.LLVM.View.Precond ( PrecondsView(..), ViewPrecondsError, ppViewPrecondsError, + ArgError(..), + ppArgError, + viewArgPreconds, viewPreconds, precondsView, ) @@ -51,7 +54,7 @@ import UCCrux.LLVM.Context.Module (ModuleContext, llvmModule, moduleTy import UCCrux.LLVM.Precondition (Preconds(..), argPreconds, globalPreconds, postconds) import UCCrux.LLVM.FullType.FuncSig (FuncSigRepr) import qualified UCCrux.LLVM.FullType.FuncSig as FS -import UCCrux.LLVM.FullType.Type (FullTypeRepr(..)) +import UCCrux.LLVM.FullType.Type (FullTypeRepr(..), ModuleTypes) import UCCrux.LLVM.Module (funcSymbolToString, globalSymbolToString, makeFuncSymbol, makeGlobalSymbol, moduleGlobalMap, funcSymbol) import UCCrux.LLVM.View.Constraint (ViewConstrainedShapeError, ConstrainedShapeView, ConstrainedTypedValueViewError, ConstrainedTypedValueView, constrainedShapeView, viewConstrainedShape, ppViewConstrainedShapeError, viewConstrainedTypedValue, constrainedTypedValueView, ppConstrainedTypedValueViewError) import UCCrux.LLVM.View.Shape (ViewShapeError, ppViewShapeError) @@ -145,6 +148,26 @@ ppArgError = , ppViewShapeError ppViewConstrainedShapeError err ] +-- Also used to implement 'SpecPrecondsView' +viewArgPreconds :: + forall m args. + ModuleTypes m -> + Ctx.Assignment (FullTypeRepr m) args -> + Vector ConstrainedShapeView -> + Either ArgError (Ctx.Assignment (ConstrainedShape m) args) +viewArgPreconds mts argTypes preconds = + let genArg :: + forall ft. + Ctx.Index args ft -> + FullTypeRepr m ft -> + Either ArgError (ConstrainedShape m ft) + genArg i ft = + case preconds Vec.!? Ctx.indexVal i of + Nothing -> Left (NotEnoughArgs (Ctx.indexVal i)) + Just val -> + liftError BadArg (viewConstrainedShape mts ft val) + in itraverseFC genArg argTypes + viewPreconds :: forall m arch fs va ret args. (fs ~ 'FS.FuncSig va ret args) => @@ -153,17 +176,8 @@ viewPreconds :: PrecondsView -> Either ViewPrecondsError (Preconds m args) viewPreconds modCtx fs vpres = - do let genArg :: - forall ft. - Ctx.Index args ft -> - FullTypeRepr m ft -> - Either ArgError (ConstrainedShape m ft) - genArg i ft = - case vArgPreconds vpres Vec.!? Ctx.indexVal i of - Nothing -> Left (NotEnoughArgs (Ctx.indexVal i)) - Just val -> - liftError BadArg (viewConstrainedShape mts ft val) - args <- liftError PrecondArgError (itraverseFC genArg (FS.fsArgTypes fs)) + do let viewArgs = viewArgPreconds mts (FS.fsArgTypes fs) (vArgPreconds vpres) + args <- liftError PrecondArgError viewArgs globs <- traverse (uncurry viewGlob) (Map.toList (vGlobalPreconds vpres)) posts <- traverse (uncurry viewPost) (Map.toList (vPostconds vpres)) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs new file mode 100644 index 000000000..1d2b86169 --- /dev/null +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs @@ -0,0 +1,185 @@ +{- +Module : UCCrux.LLVM.View.Specs +Description : See "UCCrux.LLVM.View" and "UCCrux.LLVM.Specs". +Copyright : (c) Galois, Inc 2022 +License : BSD3 +Maintainer : Langston Barrett +Stability : provisional +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StrictData #-} +{-# LANGUAGE TemplateHaskell #-} + +module UCCrux.LLVM.View.Specs + ( -- * SpecPreconds + SpecPrecondsView(..), + specPrecondsView, + viewSpecPreconds, + -- * SpecSoundness + SpecSoundnessView(..), + specSoundnessView, + viewSpecSoundness, + -- * Specs + SpecViewError, + ppSpecViewError, + SpecView(..), + specView, + viewSpec, + ) +where + +import Control.Lens ((^.)) +import qualified Data.Aeson as Aeson +import qualified Data.Aeson.TH as Aeson.TH +import Data.Data (Data) +import Data.Vector (Vector) +import qualified Data.Vector as Vec +import GHC.Generics (Generic) + +import Prettyprinter (Doc) + +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.TraversableFC (toListFC) + +import UCCrux.LLVM.Context.Module (ModuleContext, moduleTypes) +import UCCrux.LLVM.FullType.FuncSig (FuncSigRepr) +import qualified UCCrux.LLVM.FullType.FuncSig as FS +import UCCrux.LLVM.FullType.Type (FullTypeRepr(..), ModuleTypes) +import UCCrux.LLVM.Postcondition.Type (toUPostcond, typecheckPostcond, PostcondTypeError, ppPostcondTypeError) +import UCCrux.LLVM.Specs.Type (SpecPreconds, SpecSoundness(..), Spec (Spec)) +import UCCrux.LLVM.View.Constraint (ConstrainedShapeView, constrainedShapeView) +import UCCrux.LLVM.View.Postcond (UPostcondView, uPostcondView, viewUPostcond, ViewUPostcondError, ppViewUPostcondError) +import UCCrux.LLVM.View.Precond (ArgError, viewArgPreconds, ppArgError) +import qualified UCCrux.LLVM.Specs.Type as Spec + +-- Helper, not exported. Equivalent to Data.Bifunctor.first. +liftError :: (e -> i) -> Either e a -> Either i a +liftError l = + \case + Left e -> Left (l e) + Right v -> Right v + +-------------------------------------------------------------------------------- +-- * SpecPreconds + +newtype SpecPrecondsView + = SpecPrecondsView + { vSpecArgPreconds :: Vector ConstrainedShapeView } + deriving (Eq, Ord, Generic, Show) + +specPrecondsView :: SpecPreconds m args -> SpecPrecondsView +specPrecondsView pres = + SpecPrecondsView $ + Vec.fromList (toListFC constrainedShapeView (Spec.specArgPreconds pres)) + +viewSpecPreconds :: + ModuleTypes m -> + Ctx.Assignment (FullTypeRepr m) args -> + SpecPrecondsView -> + Either ArgError (SpecPreconds m args) +viewSpecPreconds mts argTys = + fmap Spec.SpecPreconds . viewArgPreconds mts argTys . vSpecArgPreconds + +-------------------------------------------------------------------------------- +-- * SpecSoundness + +data SpecSoundnessView + = OverapproxView + | UnderapproxView + | PreciseView + | ImpreciseView + deriving (Bounded, Data, Enum, Eq, Generic, Ord, Show) + +specSoundnessView :: SpecSoundness -> SpecSoundnessView +specSoundnessView = + \case + Overapprox -> OverapproxView + Underapprox -> UnderapproxView + Precise -> PreciseView + Imprecise -> ImpreciseView + +viewSpecSoundness :: SpecSoundnessView -> SpecSoundness +viewSpecSoundness = + \case + OverapproxView -> Overapprox + UnderapproxView -> Underapprox + PreciseView -> Precise + ImpreciseView -> Imprecise + +-------------------------------------------------------------------------------- +-- * Specs + +data SpecViewError + = SpecViewArgError ArgError + | SpecViewUPostcondError ViewUPostcondError + | SpecViewPostcondError PostcondTypeError + +ppSpecViewError :: SpecViewError -> Doc ann +ppSpecViewError = + \case + SpecViewArgError argError -> ppArgError argError + SpecViewUPostcondError uPostError -> ppViewUPostcondError uPostError + SpecViewPostcondError postError -> ppPostcondTypeError postError + +data SpecView + = SpecView + { vSpecPre :: SpecPrecondsView + , vSpecPreSound :: SpecSoundnessView + , vSpecPost :: Maybe UPostcondView + , vSpecPostSound :: SpecSoundnessView + } + deriving (Eq, Generic, Ord, Show) + +specView :: FuncSigRepr m fs -> Spec m fs -> SpecView +specView fsRep (Spec specPre specPreSound specPost specPostSound) = + SpecView + { vSpecPre = specPrecondsView specPre + , vSpecPreSound = specSoundnessView specPreSound + , vSpecPost = uPostcondView . toUPostcond fsRep <$> specPost + , vSpecPostSound = specSoundnessView specPostSound + } + +viewSpec :: + (fs ~ 'FS.FuncSig va ret args) => + ModuleContext m arch -> + FuncSigRepr m fs -> + SpecView -> + Either SpecViewError (Spec m fs) +viewSpec modCtx fsRep@(FS.FuncSigRepr _ args _) vspec = + do pre <- + liftError SpecViewArgError (viewSpecPreconds mts args (vSpecPre vspec)) + + -- Deserialize the postcondition + uPost <- + liftError + SpecViewUPostcondError + (commuteMaybe $ viewUPostcond modCtx fsRep <$> vSpecPost vspec) + -- Typecheck the postcondition + let typeCk p = typecheckPostcond p fsRep + post <- liftError SpecViewPostcondError (commuteMaybe (typeCk <$> uPost)) + + return $ + Spec + { Spec.specPre = pre + , Spec.specPreSound = viewSpecSoundness (vSpecPreSound vspec) + , Spec.specPost = post + , Spec.specPostSound = viewSpecSoundness (vSpecPostSound vspec) + } + where + mts = modCtx ^. moduleTypes + + -- | Commute an applicative with Maybe + commuteMaybe :: Applicative n => Maybe (n a) -> n (Maybe a) + commuteMaybe (Just val) = Just <$> val + commuteMaybe Nothing = pure Nothing + +$(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecPrecondsView) +$(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecSoundnessView) +$(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecView) diff --git a/uc-crux-llvm/uc-crux-llvm.cabal b/uc-crux-llvm/uc-crux-llvm.cabal index 6476cf863..9e7959c33 100644 --- a/uc-crux-llvm/uc-crux-llvm.cabal +++ b/uc-crux-llvm/uc-crux-llvm.cabal @@ -74,6 +74,7 @@ library UCCrux.LLVM.Overrides.Check UCCrux.LLVM.Overrides.Polymorphic UCCrux.LLVM.Overrides.Skip + UCCrux.LLVM.Overrides.Spec UCCrux.LLVM.Overrides.Stack UCCrux.LLVM.Overrides.Unsound UCCrux.LLVM.PP @@ -93,6 +94,8 @@ library UCCrux.LLVM.Setup.Constraints UCCrux.LLVM.Setup.Monad UCCrux.LLVM.Shape + UCCrux.LLVM.Specs.Apply + UCCrux.LLVM.Specs.Type UCCrux.LLVM.Stats UCCrux.LLVM.View UCCrux.LLVM.View.Constraint @@ -101,6 +104,7 @@ library UCCrux.LLVM.View.Postcond UCCrux.LLVM.View.Precond UCCrux.LLVM.View.Shape + UCCrux.LLVM.View.Specs UCCrux.LLVM.View.TH UCCrux.LLVM.View.Util From bcd4b40be4f6def9dac4c6f014510027bc387d9c Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 1 Jun 2022 15:09:02 -0400 Subject: [PATCH 03/40] uc-crux-llvm: Refactor top-level config type Make fields into a record type for extensibility and documentation --- uc-crux-llvm/src/UCCrux/LLVM/Main.hs | 12 ++++++++---- .../src/UCCrux/LLVM/Main/Config/FromEnv.hs | 10 ++++++---- uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs | 14 +++++++++++--- 3 files changed, 25 insertions(+), 11 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs index 4415d0217..35e5ef9af 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs @@ -6,6 +6,7 @@ License : BSD3 Maintainer : Langston Barrett Stability : provisional -} + {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} @@ -168,11 +169,11 @@ mainWithConfigs appCtx cruxOpts topConf = withModulePtrWidth modCtx (explore appCtx modCtx cruxOpts llOpts exConfig halloc) - Config.RunOn ents checkFrom checkFromCallers -> + Config.Analyze analyzeConf -> do entries <- makeEntryPointsOrThrow (modCtx ^. defnTypes) - (NonEmpty.toList ents) + (NonEmpty.toList (Config.entryPoints analyzeConf)) let printResult results = forM_ (Map.toList results) $ \(func, SomeBugfindingResult _types result _trace) -> @@ -189,10 +190,13 @@ mainWithConfigs appCtx cruxOpts topConf = let callers = foldMap (\f -> Set.map mkFunNm (funcCallers callGraph (getFunNm f))) - (NonEmpty.toList ents) + (NonEmpty.toList (Config.entryPoints analyzeConf)) let checkEntryPointNames = - checkFrom ++ if checkFromCallers then Set.toList callers else [] + Config.checkFrom analyzeConf ++ + if Config.checkFromCallers analyzeConf + then Set.toList callers + else [] case checkEntryPointNames of [] -> diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs index ab6c0f47d..2b1d0e71c 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs @@ -125,10 +125,12 @@ processUCCruxLLVMOptions (initCOpts, initUCOpts) = Config.runConfig = case entries of Just ents -> - Config.RunOn - ents - (checkFrom initUCOpts) - (checkFromCallers initUCOpts) + Config.Analyze $ + Config.AnalyzeConfig + { Config.entryPoints = ents + , Config.checkFrom = checkFrom initUCOpts + , Config.checkFromCallers = checkFromCallers initUCOpts + } Nothing -> if doExplore initUCOpts then diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs index 6fadc817f..b380ff15d 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs @@ -14,7 +14,8 @@ of the library outside of the "UCCrux.LLVM.Main" module. -} module UCCrux.LLVM.Main.Config.Type - ( RunConfig (..), + ( AnalyzeConfig(..), + RunConfig (..), TopLevelConfig (..), ) where @@ -27,10 +28,17 @@ import UCCrux.LLVM.Newtypes.FunctionName (FunctionName) import qualified UCCrux.LLVM.Equivalence.Config as EqConfig import qualified UCCrux.LLVM.Run.Explore.Config as ExConfig +data AnalyzeConfig + = AnalyzeConfig + { entryPoints :: NonEmpty FunctionName + , checkFrom :: [FunctionName] + , checkFromCallers :: Bool + } + deriving (Eq, Ord, Show) + data RunConfig = Explore ExConfig.ExploreConfig - -- | The 'Bool' is whether or not to check contracts from callers - | RunOn (NonEmpty FunctionName) [FunctionName] Bool + | Analyze AnalyzeConfig | CrashEquivalence EqConfig.EquivalenceConfig deriving (Eq, Ord, Show) From 6cbd667a3f5975c6aaee8aa4d2b07d3a6a505e49 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 16 Jun 2022 15:45:29 -0400 Subject: [PATCH 04/40] uc-crux-llvm: Serialization of Specs --- uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs | 31 +++++++++++++++++++--- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs index 1d2b86169..5d1e8733c 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs @@ -26,12 +26,16 @@ module UCCrux.LLVM.View.Specs SpecSoundnessView(..), specSoundnessView, viewSpecSoundness, - -- * Specs + -- * Spec SpecViewError, ppSpecViewError, SpecView(..), specView, viewSpec, + -- * Specs + SpecsView(..), + specsView, + viewSpecs, ) where @@ -53,11 +57,12 @@ import UCCrux.LLVM.FullType.FuncSig (FuncSigRepr) import qualified UCCrux.LLVM.FullType.FuncSig as FS import UCCrux.LLVM.FullType.Type (FullTypeRepr(..), ModuleTypes) import UCCrux.LLVM.Postcondition.Type (toUPostcond, typecheckPostcond, PostcondTypeError, ppPostcondTypeError) -import UCCrux.LLVM.Specs.Type (SpecPreconds, SpecSoundness(..), Spec (Spec)) +import UCCrux.LLVM.Specs.Type (SpecPreconds, SpecSoundness(..), Spec (Spec), Specs (Specs)) import UCCrux.LLVM.View.Constraint (ConstrainedShapeView, constrainedShapeView) import UCCrux.LLVM.View.Postcond (UPostcondView, uPostcondView, viewUPostcond, ViewUPostcondError, ppViewUPostcondError) import UCCrux.LLVM.View.Precond (ArgError, viewArgPreconds, ppArgError) import qualified UCCrux.LLVM.Specs.Type as Spec +import Data.List.NonEmpty (NonEmpty) -- Helper, not exported. Equivalent to Data.Bifunctor.first. liftError :: (e -> i) -> Either e a -> Either i a @@ -114,7 +119,7 @@ viewSpecSoundness = ImpreciseView -> Imprecise -------------------------------------------------------------------------------- --- * Specs +-- * Spec data SpecViewError = SpecViewArgError ArgError @@ -180,6 +185,26 @@ viewSpec modCtx fsRep@(FS.FuncSigRepr _ args _) vspec = commuteMaybe (Just val) = Just <$> val commuteMaybe Nothing = pure Nothing +-------------------------------------------------------------------------------- +-- * Specs + +newtype SpecsView = SpecsView { getSpecsView :: NonEmpty SpecView } + deriving (Eq, Generic, Ord, Show) + +specsView :: FuncSigRepr m fs -> Specs m fs -> SpecsView +specsView funcSigRep = + SpecsView . fmap (specView funcSigRep) . Spec.getSpecs + +viewSpecs :: + (fs ~ 'FS.FuncSig va ret args) => + ModuleContext m arch -> + FuncSigRepr m fs -> + SpecsView -> + Either SpecViewError (Specs m fs) +viewSpecs modCtx funcSigRep (SpecsView vspecs) = + Specs <$> traverse (viewSpec modCtx funcSigRep) vspecs + $(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecPrecondsView) $(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecSoundnessView) $(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecView) +$(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecsView) From ef31adf6dbf9ae93c99f7d33b3eb8af754685fd5 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 16 Jun 2022 15:48:24 -0400 Subject: [PATCH 05/40] uc-crux-llvm: JSON instances for FunctionName newtype --- .../src/UCCrux/LLVM/Newtypes/FunctionName.hs | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Newtypes/FunctionName.hs b/uc-crux-llvm/src/UCCrux/LLVM/Newtypes/FunctionName.hs index 1703d3218..a630eaff3 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Newtypes/FunctionName.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Newtypes/FunctionName.hs @@ -7,6 +7,11 @@ Maintainer : Langston Barrett Stability : provisional -} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TemplateHaskell #-} + module UCCrux.LLVM.Newtypes.FunctionName ( FunctionName , functionNameToString @@ -14,9 +19,16 @@ module UCCrux.LLVM.Newtypes.FunctionName ) where +import qualified Data.Aeson as Aeson +import qualified Data.Aeson.TH as Aeson.TH +import Data.Data (Data) +import GHC.Generics (Generic) + newtype FunctionName = FunctionName { functionNameToString :: String } - deriving (Eq, Ord, Show) + deriving (Data, Eq, Aeson.FromJSONKey, Generic, Ord, Show) -- | Inverse of 'functionNameToString' functionNameFromString :: String -> FunctionName functionNameFromString = FunctionName + +$(Aeson.TH.deriveJSON Aeson.defaultOptions ''FunctionName) From db484d74d498c3cc9b505637a77a983c4ceb0c1c Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 16 Jun 2022 15:56:40 -0400 Subject: [PATCH 06/40] uc-crux-llvm: Parse user-provided Specs Still needs to be plumbed through to Loop. --- .../src/UCCrux/LLVM/Main/Config/FromEnv.hs | 29 +++++++++++++++++++ .../src/UCCrux/LLVM/Main/Config/Type.hs | 3 ++ 2 files changed, 32 insertions(+) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs index 2b1d0e71c..85db91716 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs @@ -27,6 +27,9 @@ where import Control.Applicative ((<|>)) import Control.Lens (Lens', lens) import Control.Monad (when) +import qualified Data.Aeson as Aeson (eitherDecode) +import qualified Data.ByteString.Lazy.Char8 as BS (readFile) +import qualified Data.Map as Map import Data.List.NonEmpty (NonEmpty, nonEmpty) import Data.Word (Word64) import Data.Text (Text) @@ -46,6 +49,8 @@ import UCCrux.LLVM.Main.Config.Type (TopLevelConfig) import qualified UCCrux.LLVM.Main.Config.Type as Config import UCCrux.LLVM.Newtypes.FunctionName (FunctionName, functionNameFromString) import UCCrux.LLVM.Newtypes.Seconds (Seconds, secondsFromInt) +import UCCrux.LLVM.View.Specs (SpecsView) +import Data.Map (Map) {- ORMOLU_ENABLE -} -- | Options as obtained from the Crux command-line and config file machinery. @@ -64,6 +69,7 @@ data UCCruxLLVMOptions = UCCruxLLVMOptions exploreParallel :: Bool, entryPoints :: [FunctionName], skipFunctions :: [FunctionName], + specsPath :: FilePath, verbosity :: Int } @@ -119,6 +125,18 @@ processUCCruxLLVMOptions (initCOpts, initUCOpts) = ucLLVMOptions initUCOpts ) + -- Parse JSON of user-provided function specs from file + let noSpecs :: Map FunctionName SpecsView + noSpecs = Map.empty + specs <- + if specsPath initUCOpts /= "" + then Aeson.eitherDecode <$> BS.readFile (specsPath initUCOpts) + else return (Right noSpecs) + specs' <- + case specs of + Left err -> die err + Right s -> return s + let topConf = Config.TopLevelConfig { Config.ucLLVMOptions = finalLLOpts, @@ -130,6 +148,7 @@ processUCCruxLLVMOptions (initCOpts, initUCOpts) = { Config.entryPoints = ents , Config.checkFrom = checkFrom initUCOpts , Config.checkFromCallers = checkFromCallers initUCOpts + , Config.specs = specs' } Nothing -> if doExplore initUCOpts @@ -189,6 +208,9 @@ entryPointsDoc = "Comma-separated list of functions to examine." skipDoc :: Text skipDoc = "List of functions to skip during exploration" +specsPathDoc :: Text +specsPathDoc = "Path to JSON file containing function specs" + verbDoc :: Text verbDoc = "Verbosity of logging. (0: minimal, 1: informational, 2: debug)" @@ -219,6 +241,7 @@ ucCruxLLVMConfig = do <*> (map functionNameFromString <$> Crux.section "skip-functions" (Crux.listSpec Crux.stringSpec) [] skipDoc) + <*> Crux.section "specs-path" Crux.fileSpec "" specsPathDoc <*> Crux.section "verbosity" Crux.numSpec 0 verbDoc, Crux.cfgEnv = Crux.liftEnvDescr ucCruxLLVMOptionsToLLVMOptions <$> Crux.cfgEnv llvmOpts, @@ -311,6 +334,12 @@ ucCruxLLVMConfig = do { skipFunctions = functionNameFromString v : skipFunctions opts }, + Crux.Option + [] + ["specs-path"] + (Text.unpack specsPathDoc) + $ Crux.ReqArg "JSONFILE" $ + \v opts -> Right opts { specsPath = v }, Crux.Option ['v'] ["verbosity"] diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs index b380ff15d..756a034ae 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs @@ -21,18 +21,21 @@ module UCCrux.LLVM.Main.Config.Type where import Data.List.NonEmpty (NonEmpty) +import Data.Map (Map) import Crux.LLVM.Config (LLVMOptions) import UCCrux.LLVM.Newtypes.FunctionName (FunctionName) import qualified UCCrux.LLVM.Equivalence.Config as EqConfig import qualified UCCrux.LLVM.Run.Explore.Config as ExConfig +import UCCrux.LLVM.View.Specs (SpecsView) data AnalyzeConfig = AnalyzeConfig { entryPoints :: NonEmpty FunctionName , checkFrom :: [FunctionName] , checkFromCallers :: Bool + , specs :: Map FunctionName SpecsView } deriving (Eq, Ord, Show) From 28ffb8bf03bfbec9415a3e49b10930190337986c Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 16 Jun 2022 16:29:46 -0400 Subject: [PATCH 07/40] uc-crux-llvm: Give user overrides access to ExprTracker So that these overrides can create new symbolic values that are tracked and understood by classification. --- uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs | 4 +-- uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs | 37 ++++++++++++-------- 2 files changed, 24 insertions(+), 17 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs index 50e5c0576..d096733c9 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs @@ -192,7 +192,7 @@ checkInferredContracts appCtx modCtx funCtx halloc cruxOpts llOpts constraints c overrides :: IsSymBackend sym bak => HasLLVMAnn sym => - IO [ ( Sim.SymCreateOverrideFn sym bak arch + IO [ ( Sim.SymCreateOverrideFn m sym bak arch , SomeCheckedCalls m sym arch ) ] @@ -216,7 +216,7 @@ checkInferredContracts appCtx modCtx funCtx halloc cruxOpts llOpts constraints c do ref <- IORef.newIORef [] return ( Sim.SymCreateOverrideFn $ - \_bak -> + \_bak _tracker -> return $ Check.createCheckOverride appCtx diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs index 289b32012..84221c22d 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs @@ -124,28 +124,34 @@ import UCCrux.LLVM.Setup.Assume (assume) import UCCrux.LLVM.Shape (Shape) {- ORMOLU_ENABLE -} -newtype CreateOverrideFn arch = +newtype CreateOverrideFn m arch = CreateOverrideFn { runCreateOverrideFn :: - forall sym bak. + forall sym bak args. IsSymBackend sym bak => HasLLVMAnn sym => bak -> + -- Origins of created values + IORef (ExprTracker m sym args) -> IO (PolymorphicLLVMOverride arch (Crux.Crux sym) sym) } -- | Used in 'SimulatorHooks' to register caller-specified overrides. -newtype SymCreateOverrideFn sym bak arch = +newtype SymCreateOverrideFn m sym bak arch = SymCreateOverrideFn { runSymCreateOverrideFn :: - bak -> IO (PolymorphicLLVMOverride arch (Crux.Crux sym) sym) + forall args. + bak -> + -- Origins of created values + IORef (ExprTracker m sym args) -> + IO (PolymorphicLLVMOverride arch (Crux.Crux sym) sym) } symCreateOverrideFn :: IsSymBackend sym bak => HasLLVMAnn sym => - CreateOverrideFn arch -> - SymCreateOverrideFn sym bak arch + CreateOverrideFn m arch -> + SymCreateOverrideFn m sym bak arch symCreateOverrideFn ov = SymCreateOverrideFn $ runCreateOverrideFn ov data UCCruxSimulationResult m arch argTypes = UCCruxSimulationResult @@ -156,7 +162,7 @@ data UCCruxSimulationResult m arch argTypes = UCCruxSimulationResult -- | Based on 'Crux.SimulatorHooks' data SimulatorHooks sym bak m arch argTypes r = SimulatorHooks - { createOverrideHooks :: [SymCreateOverrideFn sym bak arch] + { createOverrideHooks :: [SymCreateOverrideFn m sym bak arch] -- | The 'PreSimulationMem sym' parameter is the Pre-simulation memory. -- The 'Assignment' specifies the Arguments passed to the entry point. , resultHook :: @@ -196,7 +202,7 @@ defaultCallbacks = } addOverrides :: - [CreateOverrideFn arch] -> + [CreateOverrideFn m arch] -> SimulatorCallbacks m arch argTypes r -> SimulatorCallbacks m arch argTypes r addOverrides newOverrides cbs = @@ -214,14 +220,14 @@ createUnsoundOverrides :: (?memOpts :: MemOptions) => ArchOk arch => proxy arch -> - IO (IORef (Set UnsoundOverrideName), [CreateOverrideFn arch]) + IO (IORef (Set UnsoundOverrideName), [CreateOverrideFn m arch]) createUnsoundOverrides proxy = do unsoundOverrideRef <- IORef.newIORef Set.empty return ( unsoundOverrideRef , map (\ov -> CreateOverrideFn - (\_sym -> pure (getForAllSymArch ov proxy))) + (\_sym _tracker -> pure (getForAllSymArch ov proxy))) (unsoundOverrides unsoundOverrideRef) ) @@ -334,9 +340,9 @@ mkCallbacks appCtx modCtx funCtx halloc callbacks constraints cfg llvmOpts = HasLLVMAnn sym => bak -> -- | Unsound overrides - [CreateOverrideFn arch] -> + [CreateOverrideFn m arch] -> -- | Overrides that were passed in as arguments - [SymCreateOverrideFn sym bak arch] -> + [SymCreateOverrideFn m sym bak arch] -> IORef (Set SkipOverrideName) -> IORef (Maybe (PreSimulationMem sym)) -> IORef (Maybe (Crucible.RegMap sym (MapToCrucibleType arch argTypes))) -> @@ -411,13 +417,14 @@ mkCallbacks appCtx modCtx funCtx halloc callbacks constraints cfg llvmOpts = -- Crux-LLVM overrides, i.e., crucible_* registerOverrides appCtx modCtx sCruxLLVM (cruxLLVMOverrides proxy#) - overrides <- liftIO $ for overrideFns (($ bak) . runSymCreateOverrideFn) + let apOv f = runSymCreateOverrideFn f bak skipReturnValueAnnotations + overrides <- liftIO $ for overrideFns apOv let overrides' = map (\ov -> getPolymorphicLLVMOverride ov) overrides registerOverrides appCtx modCtx sArg overrides' -- Register unsound overrides, e.g., `getenv` uOverrides <- - liftIO $ traverse (\ov -> runCreateOverrideFn ov bak) uOverrideFns + liftIO $ traverse (\ov -> runCreateOverrideFn ov bak skipReturnValueAnnotations) uOverrideFns let uOverrides' = map (\ov -> getPolymorphicLLVMOverride ov) uOverrides registerOverrides appCtx modCtx sUnsound uOverrides' @@ -622,7 +629,7 @@ runSimulator :: ModuleContext m arch -> FunctionContext m arch argTypes -> Crucible.HandleAllocator -> - [CreateOverrideFn arch] -> + [CreateOverrideFn m arch] -> Preconds m argTypes -> Crucible.CFG LLVM blocks (MapToCrucibleType arch argTypes) ret -> CruxOptions -> From beba2c125a0fdc26f2805a936b9d9eec471f2e5c Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 16 Jun 2022 16:45:24 -0400 Subject: [PATCH 08/40] uc-crux-llvm: Plumb Specs from CLI to symbolic execution --- uc-crux-llvm/src/UCCrux/LLVM/Main.hs | 80 ++++++++++++------- .../src/UCCrux/LLVM/Main/Config/FromEnv.hs | 3 +- .../src/UCCrux/LLVM/Overrides/Spec.hs | 11 ++- uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs | 7 +- uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs | 16 ++-- .../src/UCCrux/LLVM/Run/Explore/Config.hs | 5 +- uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs | 43 ++++++++-- uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs | 41 ++++++++-- 8 files changed, 150 insertions(+), 56 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs index 35e5ef9af..23d6055e1 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs @@ -46,6 +46,7 @@ import Control.Monad (forM_, void) import Data.Aeson (ToJSON) import Data.Foldable (for_) import qualified Data.List.NonEmpty as NonEmpty +import Data.Map (Map) import GHC.Generics (Generic) import System.Exit (ExitCode(..)) import System.IO (Handle) @@ -85,22 +86,26 @@ import Crux.LLVM.Simulate (parseLLVM) import Paths_uc_crux_llvm (version) import UCCrux.LLVM.Callgraph.LLVM (directCalls, funcCallers) -import UCCrux.LLVM.Context.App (AppContext) +import UCCrux.LLVM.Context.App (AppContext, log) import UCCrux.LLVM.Context.Module (ModuleContext, SomeModuleContext(..), makeModuleContext, defnTypes, withModulePtrWidth, llvmModule) import UCCrux.LLVM.Equivalence (checkEquiv) import qualified UCCrux.LLVM.Equivalence.Config as EqConfig import qualified UCCrux.LLVM.Logging as Log +import UCCrux.LLVM.Logging (Verbosity(Hi)) import qualified UCCrux.LLVM.Main.Config.FromEnv as Config.FromEnv import UCCrux.LLVM.Main.Config.Type (TopLevelConfig) import qualified UCCrux.LLVM.Main.Config.Type as Config -import UCCrux.LLVM.Module (defnSymbolToString, getModule) -import UCCrux.LLVM.Newtypes.FunctionName (functionNameFromString, functionNameToString) +import UCCrux.LLVM.Module (defnSymbolToString, getModule, FuncSymbol) +import UCCrux.LLVM.Newtypes.FunctionName (functionNameFromString, functionNameToString, FunctionName) import UCCrux.LLVM.Run.Check (inferThenCheck, ppSomeCheckResult) import UCCrux.LLVM.Run.EntryPoints (makeEntryPointsOrThrow) import UCCrux.LLVM.Run.Explore (explore) +import qualified UCCrux.LLVM.Run.Explore.Config as ExConfig import UCCrux.LLVM.Run.Result (BugfindingResult(..), SomeBugfindingResult(..)) import qualified UCCrux.LLVM.Run.Result as Result import UCCrux.LLVM.Run.Loop (loopOnFunctions) +import UCCrux.LLVM.View.Specs (SpecsView, ppSpecViewError, parseSpecs) +import UCCrux.LLVM.Specs.Type (SomeSpecs) {- ORMOLU_ENABLE -} mainWithOutputTo :: Handle -> IO ExitCode @@ -166,9 +171,9 @@ mainWithConfigs appCtx cruxOpts topConf = SomeModuleContext' modCtx <- translateFile llOpts halloc memVar path case Config.runConfig topConf of Config.Explore exConfig -> - withModulePtrWidth - modCtx - (explore appCtx modCtx cruxOpts llOpts exConfig halloc) + withModulePtrWidth modCtx $ + withSpecs modCtx (ExConfig.exploreSpecs exConfig) $ \specs -> + explore appCtx modCtx cruxOpts llOpts exConfig halloc specs Config.Analyze analyzeConf -> do entries <- makeEntryPointsOrThrow @@ -198,27 +203,28 @@ mainWithConfigs appCtx cruxOpts topConf = then Set.toList callers else [] - case checkEntryPointNames of - [] -> - printResult =<< - loopOnFunctions appCtx modCtx halloc cruxOpts llOpts entries - _ -> - withModulePtrWidth - modCtx - ( do checkFromEntries <- - makeEntryPointsOrThrow - (modCtx ^. defnTypes) - checkEntryPointNames - (result, checkResult) <- - inferThenCheck appCtx modCtx halloc cruxOpts llOpts entries checkFromEntries - printResult result - for_ (Map.toList checkResult) $ - \(checkedFunc, checkedResult) -> - Text.IO.putStrLn . - PP.renderStrict . - PP.layoutPretty PP.defaultLayoutOptions =<< - ppSomeCheckResult appCtx checkedFunc checkedResult - ) + withSpecs modCtx (Config.specs analyzeConf) $ \specs -> + case checkEntryPointNames of + [] -> + printResult =<< + loopOnFunctions appCtx modCtx halloc cruxOpts llOpts specs entries + _ -> + withModulePtrWidth + modCtx + ( do checkFromEntries <- + makeEntryPointsOrThrow + (modCtx ^. defnTypes) + checkEntryPointNames + (result, checkResult) <- + inferThenCheck appCtx modCtx halloc cruxOpts llOpts specs entries checkFromEntries + printResult result + for_ (Map.toList checkResult) $ + \(checkedFunc, checkedResult) -> + Text.IO.putStrLn . + PP.renderStrict . + PP.layoutPretty PP.defaultLayoutOptions =<< + ppSomeCheckResult appCtx checkedFunc checkedResult + ) Config.CrashEquivalence eqConfig -> do path' <- genBitCode @@ -236,7 +242,25 @@ mainWithConfigs appCtx cruxOpts topConf = llOpts (EqConfig.equivOrOrder eqConfig) (EqConfig.equivEntryPoints eqConfig) - return ExitSuccess + return ExitSuccess + where + withSpecs :: + forall m arch a. + ModuleContext m arch -> + Map FunctionName SpecsView -> + (Map (FuncSymbol m) (SomeSpecs m) -> IO a) -> + IO ExitCode + withSpecs modCtx specMap action = + case parseSpecs modCtx specMap of + Left err -> + do print (ppSpecViewError err) + return (ExitFailure 1) + Right (specs, missing) -> + do (appCtx ^. log) Hi "Specs not used, functions not in module:" + for_ missing $ \fnName -> + (appCtx ^. log) Hi (Text.pack (functionNameToString fnName)) + _ <- action specs + return ExitSuccess translateLLVMModule :: LLVMOptions -> diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs index 85db91716..6a56b39ac 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs @@ -159,7 +159,8 @@ processUCCruxLLVMOptions (initCOpts, initUCOpts) = ExConfig.exploreBudget = exploreBudget initUCOpts, ExConfig.exploreTimeout = exploreTimeout initUCOpts, ExConfig.exploreParallel = exploreParallel initUCOpts, - ExConfig.exploreSkipFunctions = skipFunctions initUCOpts + ExConfig.exploreSkipFunctions = skipFunctions initUCOpts, + ExConfig.exploreSpecs = specs' }) else Config.CrashEquivalence diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs index e15c259f7..c641b8928 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs @@ -84,12 +84,11 @@ specOverrides :: Map (FuncSymbol m) (SomeSpecs m) -> OverM personality sym LLVM [PolymorphicLLVMOverride arch (personality sym) sym] specOverrides modCtx bak mtrans tracker specs = - do - let llvmCtx = mtrans ^. transContext - let ?lc = llvmCtx ^. llvmTypeCtx - let create funcSymb (Spec.SomeSpecs fsRep@FuncSigRepr{} specs') = - createSpecOverride modCtx bak tracker funcSymb fsRep specs' - pure $ map (uncurry create) (Map.toList specs) + do let llvmCtx = mtrans ^. transContext + let ?lc = llvmCtx ^. llvmTypeCtx + let create funcSymb (Spec.SomeSpecs fsRep@FuncSigRepr{} specs') = + createSpecOverride modCtx bak tracker funcSymb fsRep specs' + pure $ map (uncurry create) (Map.toList specs) -- | Boilerplate to create an LLVM override mkOverride :: diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs index d096733c9..6f488315b 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs @@ -91,6 +91,7 @@ import UCCrux.LLVM.Run.Result (SomeBugfindingResult) import qualified UCCrux.LLVM.Run.Result as Result import UCCrux.LLVM.Setup (SymValue) import UCCrux.LLVM.Shape (Shape) +import UCCrux.LLVM.Specs.Type (SomeSpecs) {- ORMOLU_ENABLE -} -- | The result of encountering a check override some number of times during @@ -287,6 +288,8 @@ inferThenCheck :: HandleAllocator -> CruxOptions -> LLVMOptions -> + -- | Specifications for (usually external) functions + Map (FuncSymbol m) (SomeSpecs m) -> -- | Functions to infer contracts for EntryPoints m -> -- | Entry points for checking inferred contracts @@ -294,9 +297,9 @@ inferThenCheck :: IO ( Map (DefnSymbol m) (SomeBugfindingResult m arch) , Map (DefnSymbol m) (SomeCheckResult m arch) ) -inferThenCheck appCtx modCtx halloc cruxOpts llOpts toInfer entries = +inferThenCheck appCtx modCtx halloc cruxOpts llOpts specs toInfer entries = do inferResult <- - Loop.loopOnFunctions appCtx modCtx halloc cruxOpts llOpts toInfer + Loop.loopOnFunctions appCtx modCtx halloc cruxOpts llOpts specs toInfer chkResult <- checkInferredContractsFromEntryPoints appCtx modCtx halloc cruxOpts llOpts entries $ Map.mapMaybe getPreconds inferResult diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs index 0eb3c090c..6981d35d8 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs @@ -51,7 +51,7 @@ import UCCrux.LLVM.Newtypes.FunctionName (functionNameToString) import UCCrux.LLVM.Context.App (AppContext, log) import UCCrux.LLVM.Context.Module (ModuleContext, llvmModule, moduleFilePath, defnTypes) import UCCrux.LLVM.Errors.Panic (panic) -import UCCrux.LLVM.Module (DefnSymbol, getDefnSymbol, makeDefnSymbol, getModule) +import UCCrux.LLVM.Module (DefnSymbol, getDefnSymbol, makeDefnSymbol, getModule, FuncSymbol) import UCCrux.LLVM.Logging (Verbosity(Low, Med, Hi)) import UCCrux.LLVM.Newtypes.Seconds (secondsToMicroseconds) import UCCrux.LLVM.Run.Explore.Config (ExploreConfig) @@ -60,6 +60,8 @@ import UCCrux.LLVM.Run.Result (SomeBugfindingResult(..)) import qualified UCCrux.LLVM.Run.Result as Result import UCCrux.LLVM.Run.Loop (loopOnFunction) import UCCrux.LLVM.Stats (Stats(unimplementedFreq), getStats, ppStats) +import Data.Map (Map) +import UCCrux.LLVM.Specs.Type (SomeSpecs) {- ORMOLU_ENABLE -} withTimeout :: Int -> IO a -> IO (Either () a) @@ -75,10 +77,12 @@ exploreOne :: LLVMOptions -> ExploreConfig -> Crucible.HandleAllocator -> + -- | Specifications for (usually external) functions + Map (FuncSymbol m) (SomeSpecs m) -> FilePath -> DefnSymbol m -> IO Stats -exploreOne appCtx modCtx cruxOpts llOpts exOpts halloc dir defnSym = +exploreOne appCtx modCtx cruxOpts llOpts exOpts halloc specs dir defnSym = do let L.Symbol func = getDefnSymbol defnSym let logFilePath = dir func -<.> ".summary.log" @@ -93,7 +97,7 @@ exploreOne appCtx modCtx cruxOpts llOpts exOpts halloc dir defnSym = maybeResult <- withTimeout (secondsToMicroseconds (ExConfig.exploreTimeout exOpts)) - (loopOnFunction appCtx modCtx halloc cruxOpts llOpts defnSym) + (loopOnFunction appCtx modCtx halloc cruxOpts llOpts specs defnSym) case maybeResult of Right (Right (SomeBugfindingResult _types result _trace)) -> do @@ -131,8 +135,10 @@ explore :: LLVMOptions -> ExploreConfig -> Crucible.HandleAllocator -> + -- | Specifications for (usually external) functions + Map (FuncSymbol m) (SomeSpecs m) -> IO () -explore appCtx modCtx cruxOpts llOpts exOpts halloc = +explore appCtx modCtx cruxOpts llOpts exOpts halloc specs = do (appCtx ^. log) Hi $ "Exploring with budget: " <> Text.pack (show (ExConfig.exploreBudget exOpts)) -- TODO choose randomly @@ -157,7 +163,7 @@ explore appCtx modCtx cruxOpts llOpts exOpts halloc = -- taken from the modDefines of this same modCtx just above. panic "explore" ["Function not found in module :" ++ func]) funcsToExplore - let doExplore ac = exploreOne ac modCtx cruxOpts llOpts exOpts halloc dir + let doExplore ac = exploreOne ac modCtx cruxOpts llOpts exOpts halloc specs dir stats <- if ExConfig.exploreParallel exOpts then diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore/Config.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore/Config.hs index d2999c131..72f56c35f 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore/Config.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore/Config.hs @@ -14,6 +14,8 @@ where import UCCrux.LLVM.Newtypes.FunctionName (FunctionName) import UCCrux.LLVM.Newtypes.Seconds (Seconds) +import Data.Map (Map) +import UCCrux.LLVM.View.Specs (SpecsView) data ExploreConfig = ExploreConfig { -- | Explore functions that already have a log present in the log directory @@ -22,6 +24,7 @@ data ExploreConfig = ExploreConfig exploreBudget :: Int, exploreTimeout :: Seconds, exploreParallel :: Bool, - exploreSkipFunctions :: [FunctionName] + exploreSkipFunctions :: [FunctionName], + exploreSpecs :: Map FunctionName SpecsView } deriving (Eq, Ord, Show) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs index 4b9fd990f..6db800239 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE ImplicitParams #-} {- Module : UCCrux.LLVM.Run.Loop Description : Run the simulator in a loop, creating a 'BugfindingResult' @@ -50,7 +51,7 @@ import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator) -- crucible-llvm import Lang.Crucible.LLVM.MemModel (withPtrWidth) import Lang.Crucible.LLVM.Extension( LLVM ) -import Lang.Crucible.LLVM.Translation (llvmPtrWidth, transContext) +import Lang.Crucible.LLVM.Translation (llvmPtrWidth, transContext, llvmTypeCtx) -- crux import Crux.Config.Common (CruxOptions) @@ -77,6 +78,10 @@ import UCCrux.LLVM.Run.Result (BugfindingResult(..), SomeBugfindingRes import qualified UCCrux.LLVM.Run.Result as Result import qualified UCCrux.LLVM.Run.Simulate as Sim import UCCrux.LLVM.Run.Unsoundness (Unsoundness) +import UCCrux.LLVM.Specs.Type (SomeSpecs(SomeSpecs)) +import UCCrux.LLVM.FullType.FuncSig (FuncSigRepr(FuncSigRepr)) +import UCCrux.LLVM.Overrides.Spec (createSpecOverride) +import qualified Crux.LLVM.Config as CruxLLVM {- ORMOLU_ENABLE -} -- | Run the simulator in a loop, creating a 'BugfindingResult' @@ -209,14 +214,30 @@ bugfindingLoop :: CruxOptions -> LLVMOptions -> Crucible.HandleAllocator -> + -- | Specifications for (usually external) functions + Map (FuncSymbol m) (SomeSpecs m) -> IO (BugfindingResult m arch argTypes, Seq (Sim.UCCruxSimulationResult m arch argTypes)) -bugfindingLoop appCtx modCtx funCtx cfg cruxOpts llvmOpts halloc = +bugfindingLoop appCtx modCtx funCtx cfg cruxOpts llvmOpts halloc specs = post <$> - bugfindingLoopWithCallbacks appCtx modCtx funCtx cfg cruxOpts llvmOpts halloc (fmap swap Sim.defaultCallbacks) + bugfindingLoopWithCallbacks appCtx modCtx funCtx cfg cruxOpts llvmOpts halloc callbacks where swap (cruxResult, ucCruxResult) = (ucCruxResult, cruxResult) post (result, results) = (result, fmap fst results) + -- Default (do-nothing) callbacks, except they register overrides for all + -- the provided function specs + callbacks = + Sim.addOverrides + (map (uncurry mkSpecOverride) (Map.toList specs)) + (fmap swap Sim.defaultCallbacks) + + mkSpecOverride funcSymb specs_ = + Sim.CreateOverrideFn $ \bak tracker -> + do SomeSpecs fsRep@FuncSigRepr{} specs' <- return specs_ + let ?lc = modCtx ^. moduleTranslation . transContext . llvmTypeCtx + let ?memOpts = CruxLLVM.memOpts llvmOpts + return (createSpecOverride modCtx bak tracker funcSymb fsRep specs') + loopOnFunction :: Crux.Logs msgs => Crux.SupportsCruxLogMessage msgs => @@ -225,9 +246,12 @@ loopOnFunction :: Crucible.HandleAllocator -> CruxOptions -> LLVMOptions -> + -- | Specifications for (usually external) functions + Map (FuncSymbol m) (SomeSpecs m) -> + -- | Entry point for symbolic execution DefnSymbol m -> IO (Either (Panic Unimplemented) (SomeBugfindingResult m arch)) -loopOnFunction appCtx modCtx halloc cruxOpts llOpts fn = +loopOnFunction appCtx modCtx halloc cruxOpts llOpts specs fn = catchUnimplemented $ llvmPtrWidth (modCtx ^. moduleTranslation . transContext) @@ -249,6 +273,7 @@ loopOnFunction appCtx modCtx halloc cruxOpts llOpts fn = cruxOpts llOpts halloc + specs ) ) @@ -262,9 +287,11 @@ loopOnFunctions :: Crucible.HandleAllocator -> CruxOptions -> LLVMOptions -> + -- | Specifications for (usually external) functions + Map (FuncSymbol m) (SomeSpecs m) -> EntryPoints m -> IO (Map (DefnSymbol m) (SomeBugfindingResult m arch)) -loopOnFunctions appCtx modCtx halloc cruxOpts llOpts entries = +loopOnFunctions appCtx modCtx halloc cruxOpts llOpts specs entries = Map.fromList <$> llvmPtrWidth (modCtx ^. moduleTranslation . transContext) @@ -274,7 +301,7 @@ loopOnFunctions appCtx modCtx halloc cruxOpts llOpts entries = ( for (getEntryPoints entries) $ \entry -> (entry,) . either throw id - <$> loopOnFunction appCtx modCtx halloc cruxOpts llOpts entry + <$> loopOnFunction appCtx modCtx halloc cruxOpts llOpts specs entry ) ) @@ -319,8 +346,8 @@ zipResults appCtx modCtx1 modCtx2 halloc cruxOpts llOpts entries = else map functionNameToString entries) entries1 <- makeEntries modCtx1 entries2 <- makeEntries modCtx2 - results1 <- loopOnFunctions appCtx modCtx1 halloc cruxOpts llOpts entries1 - results2 <- loopOnFunctions appCtx modCtx2 halloc cruxOpts llOpts entries2 + results1 <- loopOnFunctions appCtx modCtx1 halloc cruxOpts llOpts Map.empty entries1 + results2 <- loopOnFunctions appCtx modCtx2 halloc cruxOpts llOpts Map.empty entries2 let mkFunName = functionNameFromString . defnSymbolToString pure $ -- Note: It's a postcondition of loopOnFunctions that these two maps diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs index 5d1e8733c..29175fedb 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs @@ -36,33 +36,43 @@ module UCCrux.LLVM.View.Specs SpecsView(..), specsView, viewSpecs, + -- * Map of specs + parseSpecs, ) where import Control.Lens ((^.)) +import Control.Monad (foldM) import qualified Data.Aeson as Aeson import qualified Data.Aeson.TH as Aeson.TH import Data.Data (Data) +import Data.List.NonEmpty (NonEmpty) +import Data.Map (Map) +import qualified Data.Map as Map import Data.Vector (Vector) import qualified Data.Vector as Vec import GHC.Generics (Generic) import Prettyprinter (Doc) +import qualified Text.LLVM.AST as L + import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Some (Some(Some)) import Data.Parameterized.TraversableFC (toListFC) -import UCCrux.LLVM.Context.Module (ModuleContext, moduleTypes) +import UCCrux.LLVM.Context.Module (ModuleContext, moduleTypes, funcTypes) import UCCrux.LLVM.FullType.FuncSig (FuncSigRepr) import qualified UCCrux.LLVM.FullType.FuncSig as FS import UCCrux.LLVM.FullType.Type (FullTypeRepr(..), ModuleTypes) +import UCCrux.LLVM.Module (FuncSymbol, makeFuncSymbol, funcSymbol) +import UCCrux.LLVM.Newtypes.FunctionName (FunctionName, functionNameToString) import UCCrux.LLVM.Postcondition.Type (toUPostcond, typecheckPostcond, PostcondTypeError, ppPostcondTypeError) -import UCCrux.LLVM.Specs.Type (SpecPreconds, SpecSoundness(..), Spec (Spec), Specs (Specs)) +import qualified UCCrux.LLVM.Specs.Type as Spec +import UCCrux.LLVM.Specs.Type (SpecPreconds, SpecSoundness(..), Spec (Spec), Specs (Specs), SomeSpecs (SomeSpecs)) import UCCrux.LLVM.View.Constraint (ConstrainedShapeView, constrainedShapeView) import UCCrux.LLVM.View.Postcond (UPostcondView, uPostcondView, viewUPostcond, ViewUPostcondError, ppViewUPostcondError) import UCCrux.LLVM.View.Precond (ArgError, viewArgPreconds, ppArgError) -import qualified UCCrux.LLVM.Specs.Type as Spec -import Data.List.NonEmpty (NonEmpty) -- Helper, not exported. Equivalent to Data.Bifunctor.first. liftError :: (e -> i) -> Either e a -> Either i a @@ -123,7 +133,7 @@ viewSpecSoundness = data SpecViewError = SpecViewArgError ArgError - | SpecViewUPostcondError ViewUPostcondError + | SpecViewUPostcondError ViewUPostcondError | SpecViewPostcondError PostcondTypeError ppSpecViewError :: SpecViewError -> Doc ann @@ -204,6 +214,27 @@ viewSpecs :: viewSpecs modCtx funcSigRep (SpecsView vspecs) = Specs <$> traverse (viewSpec modCtx funcSigRep) vspecs +-------------------------------------------------------------------------------- +-- * Map of specs + +-- | Returns map of functions to specs, along with a list of functions that +-- weren't in the module. The list is guaranteed to be duplicate-free. +parseSpecs :: + ModuleContext m arch -> + Map FunctionName SpecsView -> + Either SpecViewError (Map (FuncSymbol m) (SomeSpecs m), [FunctionName]) +parseSpecs modCtx = + foldM go (Map.empty, []) . Map.toList + where + go (mp, missingFuns) (fnName, vspecs) = + case makeFuncSymbol (L.Symbol (functionNameToString fnName)) (modCtx ^. funcTypes) of + Nothing -> Right (mp, fnName : missingFuns) + Just funcSymb -> + do Some fsRepr@FS.FuncSigRepr{} <- + return (modCtx ^. funcTypes . funcSymbol funcSymb) + specs <- viewSpecs modCtx fsRepr vspecs + return (Map.insert funcSymb (SomeSpecs fsRepr specs) mp, missingFuns) + $(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecPrecondsView) $(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecSoundnessView) $(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecView) From e2663c9615ebd1456e5ec57296db92307c6a9086 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 17 Jun 2022 10:03:36 -0400 Subject: [PATCH 09/40] uc-crux-llvm: Fix test compilation, adjust to new function types --- uc-crux-llvm/test/Check.hs | 4 +++- uc-crux-llvm/test/Postcond.hs | 4 ++-- uc-crux-llvm/test/Test.hs | 1 + 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/uc-crux-llvm/test/Check.hs b/uc-crux-llvm/test/Check.hs index 48698615f..31d3a700f 100644 --- a/uc-crux-llvm/test/Check.hs +++ b/uc-crux-llvm/test/Check.hs @@ -100,6 +100,7 @@ checkOverrideTests = cruxOpts llOpts halloc + Map.empty -- Construct override that checks that y is nonnull @@ -116,7 +117,7 @@ checkOverrideTests = Sim.SimulatorHooks { Sim.createOverrideHooks = [ Sim.SymCreateOverrideFn $ - \_sym -> + \_sym _tracker -> return $ fromMaybe (error msg) $ Check.checkOverrideFromResult @@ -183,6 +184,7 @@ checkOverrideTests = halloc cruxOpts llOpts + Map.empty (EntryPoints.makeEntryPoints [f]) (EntryPoints.makeEntryPoints [g, h]) let getResult fun = diff --git a/uc-crux-llvm/test/Postcond.hs b/uc-crux-llvm/test/Postcond.hs index 7af07edaa..38a0a6194 100644 --- a/uc-crux-llvm/test/Postcond.hs +++ b/uc-crux-llvm/test/Postcond.hs @@ -82,7 +82,7 @@ postcondTests = Sim.SimulatorHooks { Sim.createOverrideHooks = [ Sim.SymCreateOverrideFn $ - \bak -> + \bak _tracker -> return $ Skip.createSkipOverride modCtx @@ -136,7 +136,7 @@ postcondTests = Sim.SimulatorHooks { Sim.createOverrideHooks = [ Sim.SymCreateOverrideFn $ - \sym -> + \sym _tracker -> return $ Skip.createSkipOverride modCtx diff --git a/uc-crux-llvm/test/Test.hs b/uc-crux-llvm/test/Test.hs index 3d6181f0b..68e3c8d87 100644 --- a/uc-crux-llvm/test/Test.hs +++ b/uc-crux-llvm/test/Test.hs @@ -129,6 +129,7 @@ findBugs llvmModule file fns = halloc cruxOpts llOpts + Map.empty =<< makeEntryPointsOrThrow (modCtx ^. defnTypes) fns getCrashDiff :: From 387345353fdb7e78d65cf306f9e5f32a64a3dafb Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 17 Jun 2022 10:19:19 -0400 Subject: [PATCH 10/40] uc-crux-llvm: Add space in error message --- uc-crux-llvm/src/UCCrux/LLVM/Bug.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Bug.hs b/uc-crux-llvm/src/UCCrux/LLVM/Bug.hs index 7ce447af2..6cc5043d0 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Bug.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Bug.hs @@ -90,7 +90,7 @@ ppBug :: Bug -> PP.Doc ann ppBug (Bug bb loc callStack) = PP.vsep [ ppBugBehavior bb - , PP.pretty "at" <> PP.pretty (ppProgramLoc loc) + , PP.pretty "at" PP.<+> PP.pretty (ppProgramLoc loc) , PP.pretty "in context:" , PP.indent 2 (ppCallStack callStack) ] From aa86519bd0c36d4cf1199433fd917f879e148e8c Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 17 Jun 2022 11:55:43 -0400 Subject: [PATCH 11/40] uc-crux-llvm: Improve Haddocks related to Specs --- .../src/UCCrux/LLVM/Overrides/Spec.hs | 31 ++++---- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 9 ++- uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs | 72 +++++++++++++------ 3 files changed, 73 insertions(+), 39 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs index c641b8928..7e36e7852 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs @@ -1,12 +1,16 @@ {- Module : UCCrux.LLVM.Overrides.Spec -Description : Overrides for skipping execution of functions with user-provided specs +Description : Overrides for skipping execution of functions with provided specs Copyright : (c) Galois, Inc 2022 License : BSD3 Maintainer : Langston Barrett Stability : provisional -TODO(lb): Track which specs actually execute and whether they are over- or +These overrides are useful for describing the behavior of external/library +functions, or for soundly skipping complex functions even when they happen to be +defined. + +TODO(lb, #932): Track which specs actually execute and whether they are over- or under-approximate. -} {-# LANGUAGE DataKinds #-} @@ -42,7 +46,7 @@ import qualified Lang.Crucible.Simulator as Crucible -- crucible-llvm import Lang.Crucible.LLVM.Extension (LLVM) import Lang.Crucible.LLVM.MemModel (HasLLVMAnn, Mem, MemOptions) -import Lang.Crucible.LLVM.Translation (ModuleTranslation, transContext, llvmTypeCtx) +import Lang.Crucible.LLVM.Translation (transContext, llvmTypeCtx) import Lang.Crucible.LLVM.TypeContext (TypeContext) import Lang.Crucible.LLVM.Intrinsics (LLVMOverride(..), basic_llvm_override) @@ -52,7 +56,8 @@ import Crux.Types (OverM) import Crux.LLVM.Overrides (ArchOk) -- uc-crux-llvm -import UCCrux.LLVM.Context.Module (ModuleContext, moduleDecls) +-- uc-crux-llvm +import UCCrux.LLVM.Context.Module (ModuleContext, moduleDecls, moduleTranslation) import UCCrux.LLVM.FullType.CrucibleType (SomeAssign'(..), assignmentToCrucibleType, toCrucibleReturnType) import UCCrux.LLVM.ExprTracker (ExprTracker) import UCCrux.LLVM.FullType.FuncSig (FuncSigRepr(FuncSigRepr)) @@ -65,10 +70,7 @@ import UCCrux.LLVM.Specs.Type (SomeSpecs) import qualified UCCrux.LLVM.Specs.Type as Spec {- ORMOLU_ENABLE -} --- | Additional overrides that are useful for bugfinding, but not for --- verification. They skip execution of the specified functions. --- --- Mostly useful for functions that are declared but not defined. +-- | Create specification-based overrides for each function in the 'Map'. specOverrides :: IsSymBackend sym bak => HasLLVMAnn sym => @@ -77,14 +79,13 @@ specOverrides :: (?memOpts :: MemOptions) => ModuleContext m arch -> bak -> - ModuleTranslation arch -> -- | Origins of created values IORef (ExprTracker m sym argTypes) -> -- | Specs of each override, see 'Specs'. Map (FuncSymbol m) (SomeSpecs m) -> OverM personality sym LLVM [PolymorphicLLVMOverride arch (personality sym) sym] -specOverrides modCtx bak mtrans tracker specs = - do let llvmCtx = mtrans ^. transContext +specOverrides modCtx bak tracker specs = + do let llvmCtx = modCtx ^. moduleTranslation . transContext let ?lc = llvmCtx ^. llvmTypeCtx let create funcSymb (Spec.SomeSpecs fsRep@FuncSigRepr{} specs') = createSpecOverride modCtx bak tracker funcSymb fsRep specs' @@ -124,12 +125,8 @@ mkOverride modCtx _proxy funcSymb (FuncSigRepr _ argFTys retTy) impl = where decl = modCtx ^. moduleDecls . funcSymbol funcSymb -- | Create an override that takes the place of a given defined or even --- declared/external function, and instead of executing that function, --- instead manufactures a fresh symbolic return value and optionally clobbers --- some parts of its arguments or global variables with fresh symbolic values. --- --- Useful for continuing symbolic execution in the presence of external/library --- functions. +-- declared/external function, and instead of executing that function, applies +-- its specification as described in the documentation for 'Spec.applySpecs'. createSpecOverride :: forall m arch sym bak fs va mft args argTypes personality. IsSymBackend sym bak => diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index 18154e001..a93c55242 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -117,6 +117,11 @@ applyPost bak modCtx tracker funcSymb fsRep mvar spec args = Crucible.modifyGlobal mvar $ \mem -> liftIO (applyPostcond bak modCtx tracker funcSymb post retTy mem args) +-- | Apply a collection of specs (a 'Specs') to the current program state. +-- +-- Creates one symbolic branches per spec, as described on the Haddock for +-- 'Specs' the semantics is that the first spec with a matching precondition has +-- its postcondition applied to mutate memory and supply a return value. applySpecs :: forall m arch sym bak fs va mft args argTypes p ext r cargs ret. ArchOk arch => @@ -125,6 +130,7 @@ applySpecs :: (?memOpts :: MemOptions) => (fs ~ 'FS.FuncSig va mft args) => Crucible.IsSymBackend sym bak => + -- | Symbolic backend bak -> ModuleContext m arch -> -- | Track origins of created values @@ -166,7 +172,8 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = let fallbackBranch = ( What4.truePred sym , liftIO $ do - -- TODO(lb): this behavior should depend on spec config + -- TODO(lb): this behavior should depend on spec config, see TODO + -- on 'Specs' Crucible.addFailedAssertion bak (Crucible.GenericSimError "No spec applied!") diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs index 05f450fec..616199db9 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs @@ -6,10 +6,12 @@ License : BSD3 Maintainer : Langston Barrett Stability : provisional -* TODO(lb): -* User-provided -* Matching behavior -* Pre- and post- +The 'Specs' datatype represents a collection of specifications for a function. +The user can provide these specifications to the UC-Crux CLI using the +@--specs-path@ option, and they will be used to override the function's +behavior (see "UCCrux.LLVM.Overrides.Spec"). + +See also user-facing docs in @doc/specs.md@. -} {-# LANGUAGE DataKinds #-} @@ -39,29 +41,48 @@ import qualified UCCrux.LLVM.FullType.FuncSig as FS import UCCrux.LLVM.Precondition (emptyArgPreconds) import UCCrux.LLVM.Postcondition.Type (Postcond) --- TODO(lb): preconds on globals +-- | Preconditions required to hold for a 'Spec' to execute. data SpecPreconds m (args :: Ctx (FullType m)) = SpecPreconds - { specArgPreconds :: Ctx.Assignment (ConstrainedShape m) args } + { -- | Preconditions on arguments to the specified function + specArgPreconds :: Ctx.Assignment (ConstrainedShape m) args + } +-- | Description of the soundness of spec pre- and post-conditions. +-- +-- This type forms a partial order (of which its 'Ord' instance is one of two +-- compatible total orderings): +-- +-- > Imprecise +-- > / \ +-- > Overapprox Underapprox +-- > \ / +-- > Precise +-- +-- The ordering means: Anything that is 'Precise' can also be counted as either +-- 'Overapprox' or 'Underapprox', and if you're willing to accept 'Imprecise', +-- then you would be willing to accept any degree of precision as well. data SpecSoundness - = -- | For preconditions, means that the specified preconditions are more - -- restrictive than the actual implementation. For postconditions, means - -- that the specified postcondition encapsulates all possible effects of - -- the implementation on the program state. - Overapprox + = -- | Neither over-approximate nor under-approximate + Precise + -- | For preconditions, means that the specified preconditions are more + -- restrictive than the actual implementation. For postconditions, it means + -- that the specified postcondition encapsulates all possible effects of the + -- implementation on the program state. + | Overapprox -- | For preconditions, means that the specified preconditions are less -- restrictive than the actual implementation. For postconditions, means -- that the specified postcondition encapsulates some definitely possible -- effects of the implementation on the program state. | Underapprox -- | Both over-approximate and under-approximate - | Precise - -- | Neither over-approximate nor under-approximate | Imprecise deriving (Bounded, Enum, Eq, Ord, Show) --- TODO(lb): docs +-- | If the precondition ('specPre') holds, then the function will have the +-- effects on program state specified in the postcondition ('specPost') See +-- "UCCrux.LLVM.Specs.Apply" for how preconditions are checked against and +-- postconditions are applied to the state. data Spec m fs = forall va ret args. (fs ~ 'FS.FuncSig va ret args) => Spec @@ -71,13 +92,24 @@ data Spec m fs , specPostSound :: SpecSoundness } --- TODO(lb): docs +-- | A collection of specifications for a function. +-- +-- The semantics are that the specs are tried in order. The first one that has a +-- matching precondition results in its postcondition being applied, just as in +-- 'Lang.Crucible.Simulator.OverrideSim.symbolicBranches'. +-- +-- TODO(lb): Configure whether matching is an error. +-- +-- TODO(lb): A semantics of non-deterministic choice rather than first-wins +-- would probably be superior. newtype Specs m fs = Specs { getSpecs :: NonEmpty (Spec m fs) } --- | This is a bit inefficient, could avoid duplicating all the 'FuncSigRepr's --- with one of the strategies outlined in --- https://github.com/GaloisInc/crucible/issues/982. +-- | Package a spec together with a matching function signature. +-- +-- To hold all of these in a map is bit inefficient, could avoid duplicating all +-- the 'FuncSigRepr's that appear in the @ModuleContext@ with one of the +-- strategies outlined in https://github.com/GaloisInc/crucible/issues/982. data SomeSpecs m = forall fs. SomeSpecs (FS.FuncSigRepr m fs) (Specs m fs) -- | The minimal spec - one with no preconditions which produces a fresh, @@ -91,8 +123,6 @@ minimalSpec (FS.FuncSigRepr _ args _) = , specPostSound = Imprecise } --- | The minimal set of specs - just 'minimalSpec'. +-- | The minimal set of specs - just a single 'minimalSpec'. minimalSpecs :: FS.FuncSigRepr m fs -> Specs m fs minimalSpecs = Specs . NE.singleton . minimalSpec - --- TODO(lb): views From ebb2ffbc378d0a99d25963c1c3b6c8581ecc38eb Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 17 Jun 2022 11:56:07 -0400 Subject: [PATCH 12/40] uc-crux-llvm: Improve concrete syntax of Views Make it a little more user friendly now that users have to write it (see --spec-path). --- .../src/UCCrux/LLVM/View/Constraint.hs | 16 +++++++++-- uc-crux-llvm/src/UCCrux/LLVM/View/FullType.hs | 10 ++++++- uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs | 17 +++++++++-- uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs | 15 +++++++++- uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs | 21 +++++++++++--- uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs | 28 ++++++++++++++----- uc-crux-llvm/test/View.hs | 2 +- 7 files changed, 89 insertions(+), 20 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Constraint.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Constraint.hs index d68c8af6b..c546b2703 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Constraint.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Constraint.hs @@ -243,6 +243,16 @@ viewConstrainedTypedValue mts (ConstrainedTypedValueView vty vval) = liftError ViewConstrainedShapeError (viewConstrainedShape mts ft vval) return (ConstrainedTypedValue ft shape) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''ConstraintView) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''ConstrainedShapeView) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''ConstrainedTypedValueView) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions + { Aeson.constructorTagModifier = + reverse . drop (length ("View" :: String)) . reverse + } + ''ConstraintView) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions { Aeson.unwrapUnaryRecords = True } + ''ConstrainedShapeView) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions + { Aeson.fieldLabelModifier = drop (length ("vConstrained" :: String)) } + ''ConstrainedTypedValueView) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/FullType.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/FullType.hs index e866b5bef..0f9e0fb19 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/FullType.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/FullType.hs @@ -244,4 +244,12 @@ viewPartTypeRepr mts = $(Aeson.TH.deriveJSON Aeson.defaultOptions ''StructPackedReprView) $(Aeson.TH.deriveJSON Aeson.defaultOptions ''VarArgsReprView) $(Aeson.TH.deriveJSON Aeson.defaultOptions ''FloatInfoReprView) -$(deriveMutualJSON Aeson.defaultOptions [''FullTypeReprView, ''PartTypeReprView]) +$(deriveMutualJSON + Aeson.defaultOptions + { Aeson.constructorTagModifier = + reverse . + drop (length ("ReprView" :: String)) . + reverse . + drop (length ("FT" :: String)) -- or "PT" + } + [''FullTypeReprView, ''PartTypeReprView]) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs index 14a404aaf..22b065eda 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs @@ -283,6 +283,17 @@ viewUPostcond modCtx fs vup = cv <- liftError ViewClobberValueError (viewClobberValue mts gTy vcv) return (gSymb, SomeClobberValue cv) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''ClobberValueView) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''ClobberArgView) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''UPostcondView) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions + { Aeson.fieldLabelModifier = drop (length ("vClobber" :: String)) } + ''ClobberValueView) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions + { Aeson.constructorTagModifier = + reverse . drop (length ("View" :: String)) . reverse + } + ''ClobberArgView) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions + { Aeson.fieldLabelModifier = drop (length ("vU" :: String)) } + ''UPostcondView) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs index 121c6aca3..faf99981a 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs @@ -33,6 +33,7 @@ where import Control.Monad (when) import qualified Data.Aeson as Aeson import Data.Foldable (toList) +import Data.List (isPrefixOf) import Data.List.NonEmpty (NonEmpty, nonEmpty) import Data.Sequence (Seq) import Data.Vector (Vector) @@ -268,4 +269,16 @@ viewShape mts tag ft vshape = check cond err = when cond (Left err) getTag vtag = liftErr (tag ft vtag) -$(deriveMutualJSON Aeson.defaultOptions [''PtrShapeView, ''ShapeView]) +$(deriveMutualJSON + Aeson.defaultOptions + { Aeson.constructorTagModifier = + \s -> + reverse $ + drop (length ("View" :: String)) $ + reverse $ + (if "Shape" `isPrefixOf` s + then drop (length ("Shape" :: String)) + else drop (length ("PtrShape" :: String))) $ + s + } + [''PtrShapeView, ''ShapeView]) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs index 29175fedb..e632d51de 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs @@ -235,7 +235,20 @@ parseSpecs modCtx = specs <- viewSpecs modCtx fsRepr vspecs return (Map.insert funcSymb (SomeSpecs fsRepr specs) mp, missingFuns) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecPrecondsView) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecSoundnessView) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecView) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''SpecsView) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions + { Aeson.fieldLabelModifier = drop (length ("vSpec" :: String)) } + ''SpecPrecondsView) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions + { Aeson.constructorTagModifier = + reverse . drop (length ("View" :: String)) . reverse + } + ''SpecSoundnessView) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions + { Aeson.fieldLabelModifier = drop (length ("vSpec" :: String)) } + ''SpecView) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions { Aeson.unwrapUnaryRecords = True } + ''SpecsView) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs index 38039b9c0..e76776cd1 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs @@ -57,10 +57,24 @@ newtype TypeName = TypeName { getTypeName :: Text } deriving (Eq, Ord, Show, Generic, Aeson.FromJSONKey, Aeson.ToJSONKey) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''Alignment) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''Width) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''Unsigned) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''GlobalVarName) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''FuncName) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''TypeName) -$(Aeson.TH.deriveJSON Aeson.defaultOptions ''L.ICmpOp) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions { Aeson.unwrapUnaryRecords = True } + ''Alignment) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions { Aeson.unwrapUnaryRecords = True } + ''Width) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions { Aeson.unwrapUnaryRecords = True } + ''Unsigned) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions { Aeson.unwrapUnaryRecords = True } + ''GlobalVarName) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions { Aeson.unwrapUnaryRecords = True } + ''FuncName) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions { Aeson.unwrapUnaryRecords = True } + ''TypeName) +$(Aeson.TH.deriveJSON + Aeson.defaultOptions { Aeson.unwrapUnaryRecords = True } + ''L.ICmpOp) diff --git a/uc-crux-llvm/test/View.hs b/uc-crux-llvm/test/View.hs index 494d86b66..346a158e5 100644 --- a/uc-crux-llvm/test/View.hs +++ b/uc-crux-llvm/test/View.hs @@ -207,7 +207,7 @@ viewTests = [ TH.testCase "view-encode-FTIntReprView" $ TH.assertEqual "view-encode-FTIntReprView" - "{\"tag\":\"FTIntReprView\",\"contents\":{\"getWidth\":1}}" + "{\"tag\":\"Int\",\"contents\":1}" (Aeson.encode (View.FTIntReprView (View.Width 1))) , prop "view-constraint" $ do vc <- HG.forAll genConstraintView From 2fc10dea1e2f36a39da43fec0fac8201473e35ac Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 17 Jun 2022 12:52:27 -0400 Subject: [PATCH 13/40] uc-crux-llvm: User-facing documentation for Specs --- uc-crux-llvm/README.md | 4 + uc-crux-llvm/doc/specs.md | 127 +++++++++++++++++++++ uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs | 13 ++- 3 files changed, 138 insertions(+), 6 deletions(-) create mode 100644 uc-crux-llvm/doc/specs.md diff --git a/uc-crux-llvm/README.md b/uc-crux-llvm/README.md index 1044f3f02..978157eed 100644 --- a/uc-crux-llvm/README.md +++ b/uc-crux-llvm/README.md @@ -225,6 +225,10 @@ crash-equivalence is an equivalence relation. Use `--entry-points` to check specific functions, or `--explore` to check all functions from both programs that share a name. +### Providing Specifications for External Functions + +See [./doc/specs.md](./doc/specs.md). + ## Developer Documentation See [./doc/developing.md](./doc/developing.md). diff --git a/uc-crux-llvm/doc/specs.md b/uc-crux-llvm/doc/specs.md new file mode 100644 index 000000000..e70bf128e --- /dev/null +++ b/uc-crux-llvm/doc/specs.md @@ -0,0 +1,127 @@ +# Specifying Functions + +Users can provide specifications of functions to UC-Crux (represented as JSON). +This can be used to provide sound and precise descriptions of external or +library functions, to speed up symbolic execution by specifying defined (but +costly) functions, or even to expand the coverage of UC-Crux by approximately +specifying functions that would trigger symbolic execution timeouts or +loop/recursion bounds. + +## Motivation + +Consider the following program: +```c +extern int *f(void); +extern int g(void); + +int main() { + int *x = f(); + *x = 5; + return g(); +} +``` +By default, UC-Crux can't tell if this function is safe or has a bug - it +depends on whether `f` returns a valid pointer. +``` +$ uc-crux-llvm --entry-points main test.c +[UC-Crux-LLVM] Results for main +[UC-Crux-LLVM] Unclear result, errors are either false or true positives (or timeouts were hit): +[UC-Crux-LLVM] Unclassified error: +[UC-Crux-LLVM] The region wasn't allocated, wasn't large enough, or was marked as readonly +[UC-Crux-LLVM] at test.c:6:6 +[UC-Crux-LLVM] in context: +[UC-Crux-LLVM] main +[UC-Crux-LLVM] at test.c:6:6 +``` +However, if the user provides a specification for `f` that says that it always +returns a valid pointer to space for one 32-bit integer, then UC-Crux can tell +that `main` is safe (modulo the behavior of `g`): +```json +{ + "f": [{ + "Pre": { "ArgPreconds": [] }, + "PreSound": "Precise", + "Post": { + "ArgClobbers": [], + "GlobalClobbers": {}, + "ReturnValue": { + "Type": { + "tag": "Ptr", + "contents": { + "tag": "Full", + "contents": { "tag": "Int", "contents": 32 } + } + }, + "Value": { + "tag": "Ptr", + "contents": [ [], { "tag": "Allocated", "contents": 1 } ] + } + } + }, + "PostSound": "Precise" + }] +} +``` +``` +$ uc-crux-llvm --specs-path specs.json --entry-points main test.c + +[UC-Crux-LLVM] Results for main +[UC-Crux-LLVM] Function is always safe. +[UC-Crux-LLVM] In addition to any assumptions listed above, the following sources of unsoundness may invalidate this safety claim: +[UC-Crux-LLVM] Execution of the following functions was skipped: +[UC-Crux-LLVM] - g +``` + +## Soundness of Specifications + +Specifications don't have to exactly describe the behavior of a function in +order to be useful. For instance, for the purposes of verification it's +acceptable to use a specification with a stronger precondition than the actual +implementation. If verification succeeds against this stronger spec, then the +program also must respect the weaker contract of the implementation. Dually, +when hunting for bugs one might use a specification with a weaker +postcondition - e.g., if a function *may* return a null pointer under some +precondition, one could use a spec with a postcondition stating that the +function *always* returns a null pointer when that precondition is met. + +Clearly, the requirements on specifications depend on the use-case. Accordingly, +the pre- and post-conditions of specs are accompanied by *soundness tags* which +indicate whether they over-approximate function behaviors, under-approximate +them, both, or neither. There are four possible tags, the meaning of which +depends on whether they are applied to preconditions or postconditions. + +- `Overapprox`: For preconditions, means that the specified preconditions are + more restrictive than the actual implementation. For postconditions, it means + that the specified postcondition encapsulates all possible effects of the + implementation on the program state under the accompanying precondition. +- `Underapprox`: For preconditions, means that the specified preconditions are + less restrictive than the actual implementation. For postconditions, means + that the specified postcondition encapsulates some definitely possible effects + of the implementation on the program state under the accompanying precondition. +- Precise: Both over-approximate nor under-approximate. +- Imprecise: Neither over-approximate nor under-approximate. + +These tags form a partial order with the following Hasse diagram: + +``` + Imprecise + / \ +Overapprox Underapprox + \ / + Precise +``` + +The ordering means: Anything that is `Precise` can also be counted as either +`Overapprox` or `Underapprox`, and if you're willing to accept `Imprecise`, +then you would be willing to accept any degree of precision as well. + +UC-Crux doesn't yet use the soundness tags internally, but the intention is that +they will be tracked and reported along with the analysis results, and that +users would be able to indicate that they're only interested in results using +over- or under-approximate specs. + +## JSON Format + +The JSON format for writing specifications is not yet stable. In the meantime, +`src/UCCrux/LLVM/Spec` and `src/UCCrux/LLVM/Views/Spec` provide some indication +of how it works. diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs index 616199db9..4e1f6791f 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs @@ -50,8 +50,8 @@ data SpecPreconds m (args :: Ctx (FullType m)) -- | Description of the soundness of spec pre- and post-conditions. -- --- This type forms a partial order (of which its 'Ord' instance is one of two --- compatible total orderings): +-- This type forms a partial order with the following Hasse diagram (of which +-- its 'Ord' instance is one of two compatible total orderings): -- -- > Imprecise -- > / \ @@ -63,19 +63,20 @@ data SpecPreconds m (args :: Ctx (FullType m)) -- 'Overapprox' or 'Underapprox', and if you're willing to accept 'Imprecise', -- then you would be willing to accept any degree of precision as well. data SpecSoundness - = -- | Neither over-approximate nor under-approximate + = -- | Both over-approximate and under-approximate Precise -- | For preconditions, means that the specified preconditions are more -- restrictive than the actual implementation. For postconditions, it means -- that the specified postcondition encapsulates all possible effects of the - -- implementation on the program state. + -- implementation on the program state under the accompanying precondition. | Overapprox -- | For preconditions, means that the specified preconditions are less -- restrictive than the actual implementation. For postconditions, means -- that the specified postcondition encapsulates some definitely possible - -- effects of the implementation on the program state. + -- effects of the implementation on the program state under the accompanying + -- precondition. | Underapprox - -- | Both over-approximate and under-approximate + -- | Neither over-approximate and under-approximate | Imprecise deriving (Bounded, Enum, Eq, Ord, Show) From 861ddf1898034849b3fe839fff64f61547fada5b Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 17 Jun 2022 12:55:28 -0400 Subject: [PATCH 14/40] uc-crux-llvm: Clean up imports, drop redundant parens --- uc-crux-llvm/.hlint.yaml | 3 +++ uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs | 4 ++-- uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs | 2 +- uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs | 4 ++-- uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs | 8 ++++---- uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs | 2 +- 6 files changed, 13 insertions(+), 10 deletions(-) diff --git a/uc-crux-llvm/.hlint.yaml b/uc-crux-llvm/.hlint.yaml index a924ea95c..a45779268 100644 --- a/uc-crux-llvm/.hlint.yaml +++ b/uc-crux-llvm/.hlint.yaml @@ -89,10 +89,13 @@ - "UCCrux.LLVM.FullType.FuncSig" - "UCCrux.LLVM.FullType.Type" - "UCCrux.LLVM.FullType.VarArgs" + - "UCCrux.LLVM.Newtypes.FunctionName" - "UCCrux.LLVM.Shape" - "UCCrux.LLVM.View.Constraint" - "UCCrux.LLVM.View.Cursor" - "UCCrux.LLVM.View.FullType" - "UCCrux.LLVM.View.Postcond" + - "UCCrux.LLVM.View.Precond" - "UCCrux.LLVM.View.Shape" + - "UCCrux.LLVM.View.Specs" - "UCCrux.LLVM.View.Util" diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs index 6a56b39ac..4cfaefba4 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs @@ -30,6 +30,7 @@ import Control.Monad (when) import qualified Data.Aeson as Aeson (eitherDecode) import qualified Data.ByteString.Lazy.Char8 as BS (readFile) import qualified Data.Map as Map +import Data.Map (Map) import Data.List.NonEmpty (NonEmpty, nonEmpty) import Data.Word (Word64) import Data.Text (Text) @@ -49,8 +50,7 @@ import UCCrux.LLVM.Main.Config.Type (TopLevelConfig) import qualified UCCrux.LLVM.Main.Config.Type as Config import UCCrux.LLVM.Newtypes.FunctionName (FunctionName, functionNameFromString) import UCCrux.LLVM.Newtypes.Seconds (Seconds, secondsFromInt) -import UCCrux.LLVM.View.Specs (SpecsView) -import Data.Map (Map) +import UCCrux.LLVM.View.Specs (SpecsView) {- ORMOLU_ENABLE -} -- | Options as obtained from the Crux command-line and config file machinery. diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs index 7e36e7852..63c55d462 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs @@ -13,10 +13,10 @@ defined. TODO(lb, #932): Track which specs actually execute and whether they are over- or under-approximate. -} + {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs index 6981d35d8..edd54cb74 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs @@ -23,6 +23,7 @@ import Control.Concurrent.Async (race) import Control.Scheduler (Comp(Par), traverseConcurrently) import Control.Exception (displayException) import Data.Function ((&)) +import Data.Map (Map) import qualified Data.Map.Strict as Map import Data.Text.IO (writeFile) import qualified Data.Text as Text @@ -59,9 +60,8 @@ import qualified UCCrux.LLVM.Run.Explore.Config as ExConfig import UCCrux.LLVM.Run.Result (SomeBugfindingResult(..)) import qualified UCCrux.LLVM.Run.Result as Result import UCCrux.LLVM.Run.Loop (loopOnFunction) +import UCCrux.LLVM.Specs.Type (SomeSpecs) import UCCrux.LLVM.Stats (Stats(unimplementedFreq), getStats, ppStats) -import Data.Map (Map) -import UCCrux.LLVM.Specs.Type (SomeSpecs) {- ORMOLU_ENABLE -} withTimeout :: Int -> IO a -> IO (Either () a) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs index 6db800239..e1e02468f 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs @@ -59,6 +59,7 @@ import Crux.Log as Crux -- crux-llvm import Crux.LLVM.Config (LLVMOptions, throwCError, CError(MissingFun)) +import qualified Crux.LLVM.Config as CruxLLVM import Crux.LLVM.Overrides -- local @@ -71,17 +72,16 @@ import UCCrux.LLVM.Errors.Panic (panic) import UCCrux.LLVM.Errors.Unimplemented (Unimplemented, catchUnimplemented) import UCCrux.LLVM.Logging (Verbosity(Hi)) import UCCrux.LLVM.FullType (MapToCrucibleType) +import UCCrux.LLVM.FullType.FuncSig (FuncSigRepr(FuncSigRepr)) import UCCrux.LLVM.Module (DefnSymbol, FuncSymbol(..), defnSymbolToString, makeDefnSymbol, getModule) +import UCCrux.LLVM.Overrides.Spec (createSpecOverride) import UCCrux.LLVM.Precondition (Preconds, NewConstraint, ppPreconds, emptyPreconds, addPrecond, ppExpansionError) import UCCrux.LLVM.Run.EntryPoints (EntryPoints, getEntryPoints, makeEntryPoints) import UCCrux.LLVM.Run.Result (BugfindingResult(..), SomeBugfindingResult(..)) import qualified UCCrux.LLVM.Run.Result as Result import qualified UCCrux.LLVM.Run.Simulate as Sim import UCCrux.LLVM.Run.Unsoundness (Unsoundness) -import UCCrux.LLVM.Specs.Type (SomeSpecs(SomeSpecs)) -import UCCrux.LLVM.FullType.FuncSig (FuncSigRepr(FuncSigRepr)) -import UCCrux.LLVM.Overrides.Spec (createSpecOverride) -import qualified Crux.LLVM.Config as CruxLLVM +import UCCrux.LLVM.Specs.Type (SomeSpecs(SomeSpecs)) {- ORMOLU_ENABLE -} -- | Run the simulator in a loop, creating a 'BugfindingResult' diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs index faf99981a..1fdfc19f3 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs @@ -278,7 +278,7 @@ $(deriveMutualJSON reverse $ (if "Shape" `isPrefixOf` s then drop (length ("Shape" :: String)) - else drop (length ("PtrShape" :: String))) $ + else drop (length ("PtrShape" :: String))) s } [''PtrShapeView, ''ShapeView]) From b48d26f25f0f592ce1afbdc908d55e71cd6e363d Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 10:40:03 -0400 Subject: [PATCH 15/40] uc-crux-llvm: Add Note [JSON Instance Tweaks] --- uc-crux-llvm/src/UCCrux/LLVM/View.hs | 15 +++++++++++++++ uc-crux-llvm/src/UCCrux/LLVM/View/Constraint.hs | 1 + uc-crux-llvm/src/UCCrux/LLVM/View/Cursor.hs | 1 + uc-crux-llvm/src/UCCrux/LLVM/View/FullType.hs | 1 + uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs | 1 + uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs | 1 + uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs | 1 + uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs | 1 + uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs | 1 + 9 files changed, 23 insertions(+) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View.hs b/uc-crux-llvm/src/UCCrux/LLVM/View.hs index 69cc184c6..85438a274 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View.hs @@ -25,6 +25,21 @@ number of advantages: The view datatypes are all in modules using the @StrictData@ language extension. This is because their primary use is serialization, which will result in complete evaluation, eliminating the benefits of laziness. + +Note [JSON instance tweaks]: JSON instances for various datatypes are derived +using 'Data.Aeson.TH.deriveJSON', with some tweaks to +'Data.Aeson.defaultOptions'. These tweaks remove unnecessary Haskell idioms from +the JSON representation. For example, it's common in Haskell code for all record +selectors for the same type to share a common prefix, e.g., "pt" in + +> data Point2D = Point2D { ptX :: Int, ptY :: Int } + +This idiom is used in part to avoid name clashes due to the lack of namespacing +for record selectors. There is no need for the JSON representation to reflect +this implementation detail, and removing such prefixes makes the JSON more terse, +hopefully making it use less RAM/disk space and network bandwidth, and making +it easier to write by hand (especially for users not familiar with Haskell +coding conventions). -} module UCCrux.LLVM.View diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Constraint.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Constraint.hs index c546b2703..d8cc1e3ca 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Constraint.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Constraint.hs @@ -243,6 +243,7 @@ viewConstrainedTypedValue mts (ConstrainedTypedValueView vty vval) = liftError ViewConstrainedShapeError (viewConstrainedShape mts ft vval) return (ConstrainedTypedValue ft shape) +-- See Note [JSON instance tweaks]. $(Aeson.TH.deriveJSON Aeson.defaultOptions { Aeson.constructorTagModifier = diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Cursor.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Cursor.hs index 1eed37632..b1f0e7c1b 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Cursor.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Cursor.hs @@ -129,4 +129,5 @@ viewCursor mts ft vcur = Nothing -> Left err Just v -> Right v +-- See Note [JSON instance tweaks]. $(Aeson.TH.deriveJSON Aeson.defaultOptions ''CursorView) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/FullType.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/FullType.hs index 0f9e0fb19..2f11ae457 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/FullType.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/FullType.hs @@ -241,6 +241,7 @@ viewPartTypeRepr mts = Just spt -> Right spt Nothing -> Left (BadAlias iden) +-- See Note [JSON instance tweaks]. $(Aeson.TH.deriveJSON Aeson.defaultOptions ''StructPackedReprView) $(Aeson.TH.deriveJSON Aeson.defaultOptions ''VarArgsReprView) $(Aeson.TH.deriveJSON Aeson.defaultOptions ''FloatInfoReprView) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs index 22b065eda..25c3a891d 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs @@ -283,6 +283,7 @@ viewUPostcond modCtx fs vup = cv <- liftError ViewClobberValueError (viewClobberValue mts gTy vcv) return (gSymb, SomeClobberValue cv) +-- See Note [JSON instance tweaks]. $(Aeson.TH.deriveJSON Aeson.defaultOptions { Aeson.fieldLabelModifier = drop (length ("vClobber" :: String)) } diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs index 4ee1b9963..5fbc49726 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs @@ -215,4 +215,5 @@ viewPreconds modCtx fs vpres = (viewUPostcond modCtx fsRep vpost) return (fSymb, post) +-- See Note [JSON instance tweaks]. $(Aeson.TH.deriveJSON Aeson.defaultOptions ''PrecondsView) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs index 1fdfc19f3..343ae7d51 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Shape.hs @@ -269,6 +269,7 @@ viewShape mts tag ft vshape = check cond err = when cond (Left err) getTag vtag = liftErr (tag ft vtag) +-- See Note [JSON instance tweaks]. $(deriveMutualJSON Aeson.defaultOptions { Aeson.constructorTagModifier = diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs index e632d51de..c4c671ce8 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs @@ -235,6 +235,7 @@ parseSpecs modCtx = specs <- viewSpecs modCtx fsRepr vspecs return (Map.insert funcSymb (SomeSpecs fsRepr specs) mp, missingFuns) +-- See Note [JSON instance tweaks]. $(Aeson.TH.deriveJSON Aeson.defaultOptions { Aeson.fieldLabelModifier = drop (length ("vSpec" :: String)) } diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs index e76776cd1..552b89233 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Util.hs @@ -57,6 +57,7 @@ newtype TypeName = TypeName { getTypeName :: Text } deriving (Eq, Ord, Show, Generic, Aeson.FromJSONKey, Aeson.ToJSONKey) +-- See Note [JSON instance tweaks]. $(Aeson.TH.deriveJSON Aeson.defaultOptions { Aeson.unwrapUnaryRecords = True } ''Alignment) From 1fc8be15b55aad0ba10b463d398258233cbdb5c3 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 10:43:44 -0400 Subject: [PATCH 16/40] uc-crux-llvm: Comment stating that commuteMaybe is sequenceA --- uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs index c4c671ce8..e40e8ccc5 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs @@ -190,7 +190,7 @@ viewSpec modCtx fsRep@(FS.FuncSigRepr _ args _) vspec = where mts = modCtx ^. moduleTypes - -- | Commute an applicative with Maybe + -- | Commute an applicative with Maybe. Equivalent to 'sequenceA'. commuteMaybe :: Applicative n => Maybe (n a) -> n (Maybe a) commuteMaybe (Just val) = Just <$> val commuteMaybe Nothing = pure Nothing From 653f7d5c908c7cd840db34c4de38029b0ba2762e Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 10:47:05 -0400 Subject: [PATCH 17/40] uc-crux-llvm: Clarify Spec.specPost --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs index 4e1f6791f..a3c86a5ff 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs @@ -87,8 +87,13 @@ data SpecSoundness data Spec m fs = forall va ret args. (fs ~ 'FS.FuncSig va ret args) => Spec - { specPre :: SpecPreconds m args + { -- | See 'UCCrux.LLVM.Specs.Apply.matchPreconds' for details of the + -- semantics. + specPre :: SpecPreconds m args , specPreSound :: SpecSoundness + -- | A 'Nothing' causes a minimal, unconstrained, fresh, symbolic return + -- value to be generated, see 'UCCrux.LLVM.Specs.Apply.applyPost' for + -- details. , specPost :: Maybe (Postcond m fs) , specPostSound :: SpecSoundness } @@ -120,6 +125,8 @@ minimalSpec (FS.FuncSigRepr _ args _) = Spec { specPre = SpecPreconds (emptyArgPreconds args) , specPreSound = Underapprox + -- This causes the fresh, unconstrained, symbolic return value to be + -- generated, see Spec.specPost , specPost = Nothing , specPostSound = Imprecise } From 1b7eaff61762e95dc9464f039b4d06f3d08980d9 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 10:47:37 -0400 Subject: [PATCH 18/40] uc-crux-llvm: Remove unused instances on SpecSoundness --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs index a3c86a5ff..30eea0619 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs @@ -78,7 +78,7 @@ data SpecSoundness | Underapprox -- | Neither over-approximate and under-approximate | Imprecise - deriving (Bounded, Enum, Eq, Ord, Show) + deriving (Eq, Ord, Show) -- | If the precondition ('specPre') holds, then the function will have the -- effects on program state specified in the postcondition ('specPost') See From 761b3bd8359781435ef39802ec176063cc421d68 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 10:56:26 -0400 Subject: [PATCH 19/40] uc-crux-llvm: Fix typos and clarify description of spec soundness --- uc-crux-llvm/doc/specs.md | 23 +++++++++++++--------- uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs | 9 +++++++-- 2 files changed, 21 insertions(+), 11 deletions(-) diff --git a/uc-crux-llvm/doc/specs.md b/uc-crux-llvm/doc/specs.md index e70bf128e..07325c7b6 100644 --- a/uc-crux-llvm/doc/specs.md +++ b/uc-crux-llvm/doc/specs.md @@ -90,16 +90,21 @@ indicate whether they over-approximate function behaviors, under-approximate them, both, or neither. There are four possible tags, the meaning of which depends on whether they are applied to preconditions or postconditions. -- `Overapprox`: For preconditions, means that the specified preconditions are - more restrictive than the actual implementation. For postconditions, it means - that the specified postcondition encapsulates all possible effects of the - implementation on the program state under the accompanying precondition. +- `Overapprox`: For preconditions, means that the specified preconditions are at + least as restrictive than the actual implementation. For postconditions, it + means that the specified postcondition encapsulates all possible effects of + the implementation on the program state under the accompanying precondition. - `Underapprox`: For preconditions, means that the specified preconditions are - less restrictive than the actual implementation. For postconditions, means - that the specified postcondition encapsulates some definitely possible effects - of the implementation on the program state under the accompanying precondition. -- Precise: Both over-approximate nor under-approximate. -- Imprecise: Neither over-approximate nor under-approximate. + at most as restrictive than the actual implementation. For postconditions, + means that the specified postcondition encapsulates some definitely possible + effects of the implementation on the program state under the accompanying + precondition. +- Precise: Both over-approximate and under-approximate, that is, a specification + that perfectly describes the possible behaviors of the specified procedure. +- Imprecise: Neither over-approximate nor under-approximate, that is, a + specification that bears none of the above relationships to the specified + procedure (but may still be useful in practice, e.g., if it's over- or + under-approximate for most---but not all---cases). These tags form a partial order with the following Hasse diagram: diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs index 30eea0619..ad53e6e1a 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs @@ -63,7 +63,9 @@ data SpecPreconds m (args :: Ctx (FullType m)) -- 'Overapprox' or 'Underapprox', and if you're willing to accept 'Imprecise', -- then you would be willing to accept any degree of precision as well. data SpecSoundness - = -- | Both over-approximate and under-approximate + = -- | Precise: Both over-approximate and under-approximate, that is, a + -- specification that perfectly describes the possible behaviors of the + -- specified procedure. Precise -- | For preconditions, means that the specified preconditions are more -- restrictive than the actual implementation. For postconditions, it means @@ -76,7 +78,10 @@ data SpecSoundness -- effects of the implementation on the program state under the accompanying -- precondition. | Underapprox - -- | Neither over-approximate and under-approximate + -- | Neither over-approximate nor under-approximate, that is, a specification + -- that bears none of the above relationships to the specified procedure (but + -- may still be useful in practice, e.g., if it's over- or under-approximate + -- for most---but not all---cases). | Imprecise deriving (Eq, Ord, Show) From 1f3c2ff499be8c85536dfdeafb4a74236465559a Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 11:04:10 -0400 Subject: [PATCH 20/40] uc-crux-llvm: Re-implement NonEmpty.singleton for GHC <9 compat --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs index ad53e6e1a..abc8c5148 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs @@ -138,4 +138,9 @@ minimalSpec (FS.FuncSigRepr _ args _) = -- | The minimal set of specs - just a single 'minimalSpec'. minimalSpecs :: FS.FuncSigRepr m fs -> Specs m fs -minimalSpecs = Specs . NE.singleton . minimalSpec +minimalSpecs = Specs . neSingleton . minimalSpec + where + -- | Added as NE.singleton in base-4.15/GHC 9. + neSingleton x = x NE.:| [] + + From 69baa3f1391a2383877c3c9f409225ef2831d492 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 12:04:38 -0400 Subject: [PATCH 21/40] uc-crux-llvm: Add more design/use-case docs for user-provided specs --- uc-crux-llvm/doc/specs.md | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/uc-crux-llvm/doc/specs.md b/uc-crux-llvm/doc/specs.md index 07325c7b6..597fec045 100644 --- a/uc-crux-llvm/doc/specs.md +++ b/uc-crux-llvm/doc/specs.md @@ -72,6 +72,26 @@ $ uc-crux-llvm --specs-path specs.json --entry-points main test.c [UC-Crux-LLVM] - g ``` +### Use Cases + +There are three main use cases in mind for this feature: + +- A user wants to analyze code with external library dependencies that can't be + linked into the LLVM bitcode due to build system difficulties or lack of + access to source code. The user can manually write specifications for a subset + of the external functions to get better analysis results (as in the above + example). +- UC-Crux maintainers wish to provide specifications of common library functions + (e.g., functions in `libc`) to improve analysis results on code using those + libraries. It's arguably easier to write these specs in the declarative format + (shown above as JSON) than as a Crucible override (Haskell function). + Perhaps users could one day select among over- or under-approximate overrides + (both provided by maintainers) for library functions depending on their goals. +- Some external, possibly partially automated process provides specifications as + part of a workflow with a system in which UC-Crux is just one component. + For example, some other source-level analysis or process might generate + potential specs and ask a human to choose among them. + ## Soundness of Specifications Specifications don't have to exactly describe the behavior of a function in @@ -130,3 +150,13 @@ over- or under-approximate specs. The JSON format for writing specifications is not yet stable. In the meantime, `src/UCCrux/LLVM/Spec` and `src/UCCrux/LLVM/Views/Spec` provide some indication of how it works. + +## Design + +There is a large space of possible specification formats, from simpler specs +that are able to adequately describe only a small subset of realistic functions, +to something with the same expressive power as writing a Crucible override in +Haskell. The hope is that the JSON format is somewhere in the middle: simple and +declarative enough to be easy to write and understand, while rich enough to +usefully specify reasonable C functions. The appropriate balance may become more +clear as the feature is developed further and more specs are written. From afc2ef3d9f35b8e42eb650f4b099c204d761c9cd Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 12:12:54 -0400 Subject: [PATCH 22/40] uc-crux-llvm: Add documentation to Main.Config.Type --- .../src/UCCrux/LLVM/Main/Config/Type.hs | 20 +++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs index 756a034ae..bb9c0adb1 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs @@ -6,6 +6,14 @@ License : BSD3 Maintainer : Langston Barrett Stability : provisional +The data types in this module are constructed from CLI/configuration files +passed to the UC-Crux-LLVM CLI. The idea is to "parse, not validate" from the +CLI options to these types. The documentation on these types refers to the +CLI/config options from which they are derived, see +"UCCrux.LLVM.Main.Config.FromEnv" (or run UC-Crux-LLVM with @--help@) for +descriptions of their intended effects, which are implemented in +"UCCrux.LLVM.Main". + The functions/types in this module aren't necessarily appropriate for using UC-Crux-LLVM as a library: 'TopLevelConfig' selects among a wide variety of functionality, a choice that is likely statically known for most library @@ -32,16 +40,24 @@ import UCCrux.LLVM.View.Specs (SpecsView) data AnalyzeConfig = AnalyzeConfig - { entryPoints :: NonEmpty FunctionName + { -- | @--entry-points@ + entryPoints :: NonEmpty FunctionName + -- | @--check-from@ , checkFrom :: [FunctionName] + -- | @--check-from-callers@ , checkFromCallers :: Bool + -- | @--specs-path@ , specs :: Map FunctionName SpecsView } deriving (Eq, Ord, Show) data RunConfig - = Explore ExConfig.ExploreConfig + = -- | @--explore@ + Explore ExConfig.ExploreConfig + -- | No corresponding CLI option, occurs when @--explore@ and + -- @--crash-equivalence@ are not used. | Analyze AnalyzeConfig + -- | @--crash-equivalence@ | CrashEquivalence EqConfig.EquivalenceConfig deriving (Eq, Ord, Show) From 512fbad4ef75ddd4de083b087c5949f7e6a77a53 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 13:11:47 -0400 Subject: [PATCH 23/40] uc-crux-llvm: Refactor configuration parsing --- .../src/UCCrux/LLVM/Main/Config/FromEnv.hs | 137 +++++++++--------- 1 file changed, 71 insertions(+), 66 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs index 4cfaefba4..279c0f4d7 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs @@ -92,30 +92,9 @@ processUCCruxLLVMOptions (initCOpts, initUCOpts) = do let appCtx = makeAppContext (verbosityFromInt (verbosity initUCOpts)) let doCrashOrder = crashOrder initUCOpts /= "" - - -- Figure out the entry points. If exploration mode is selected, the - -- specified entry points are irrelevant. If crash ordering is selected, - -- then entry points may or may not be specified. If neither is selected, - -- then entry points must be provided. - let makeEntries :: UCCruxLLVMOptions -> IO (Maybe (NonEmpty FunctionName)) - makeEntries uco - | doExplore uco = pure Nothing - | crashOrder uco /= "" = pure (nonEmpty (entryPoints uco)) - | otherwise = - Just <$> - maybe - (die - (unwords - [ "At least one entry point (--entry-points) is required", - "(or try --explore or --crash-order)" - ])) - pure - (nonEmpty (entryPoints uco)) - - entries <- makeEntries initUCOpts - when (doExplore initUCOpts && doCrashOrder) $ die "Can't specify both --explore and --crash-order" + (finalCOpts, finalLLOpts) <- processLLVMOptions ( initCOpts @@ -125,57 +104,83 @@ processUCCruxLLVMOptions (initCOpts, initUCOpts) = ucLLVMOptions initUCOpts ) - -- Parse JSON of user-provided function specs from file - let noSpecs :: Map FunctionName SpecsView - noSpecs = Map.empty - specs <- - if specsPath initUCOpts /= "" - then Aeson.eitherDecode <$> BS.readFile (specsPath initUCOpts) - else return (Right noSpecs) - specs' <- - case specs of - Left err -> die err - Right s -> return s + specs <- getSpecs -- can fail (exit) + entries <- makeEntries initUCOpts -- can fail (exit) let topConf = Config.TopLevelConfig { Config.ucLLVMOptions = finalLLOpts, - Config.runConfig = - case entries of - Just ents -> - Config.Analyze $ - Config.AnalyzeConfig - { Config.entryPoints = ents - , Config.checkFrom = checkFrom initUCOpts - , Config.checkFromCallers = checkFromCallers initUCOpts - , Config.specs = specs' - } - Nothing -> - if doExplore initUCOpts - then - Config.Explore - (ExConfig.ExploreConfig - { ExConfig.exploreAgain = reExplore initUCOpts, - ExConfig.exploreBudget = exploreBudget initUCOpts, - ExConfig.exploreTimeout = exploreTimeout initUCOpts, - ExConfig.exploreParallel = exploreParallel initUCOpts, - ExConfig.exploreSkipFunctions = skipFunctions initUCOpts, - ExConfig.exploreSpecs = specs' - }) - else - Config.CrashEquivalence - (EqConfig.EquivalenceConfig - { EqConfig.equivOrOrder = - if crashEquivalence initUCOpts - then EqConfig.Equivalence - else EqConfig.Order, - EqConfig.equivModule = crashOrder initUCOpts, - EqConfig.equivEntryPoints = entryPoints initUCOpts - }) + Config.runConfig = runConfig entries specs } - return (appCtx, finalCOpts, topConf) + where + -- Figure out the entry points. If exploration mode is selected, the + -- specified entry points are irrelevant. If crash ordering is selected, + -- then entry points may or may not be specified. If neither is selected, + -- then entry points must be provided. + makeEntries :: UCCruxLLVMOptions -> IO (Maybe (NonEmpty FunctionName)) + makeEntries uco + | doExplore uco = pure Nothing + | crashOrder uco /= "" = pure (nonEmpty (entryPoints uco)) + | otherwise = + Just <$> + maybe + (die + (unwords + [ "At least one entry point (--entry-points) is required", + "(or try --explore or --crash-order)" + ])) + pure + (nonEmpty (entryPoints uco)) + + -- Parse JSON of user-provided function specs from file + getSpecs = + do let noSpecs :: Map FunctionName SpecsView + noSpecs = Map.empty + specs <- + if specsPath initUCOpts /= "" + then Aeson.eitherDecode <$> BS.readFile (specsPath initUCOpts) + else return (Right noSpecs) + case specs of + Left err -> die err + Right s -> return s + + -- Create the top-level configuration data type + runConfig entries specs = + case entries of + Just ents -> + Config.Analyze $ + Config.AnalyzeConfig + { Config.entryPoints = ents + , Config.checkFrom = checkFrom initUCOpts + , Config.checkFromCallers = checkFromCallers initUCOpts + , Config.specs = specs + } + Nothing -> + if doExplore initUCOpts + then + Config.Explore + (ExConfig.ExploreConfig + { ExConfig.exploreAgain = reExplore initUCOpts, + ExConfig.exploreBudget = exploreBudget initUCOpts, + ExConfig.exploreTimeout = exploreTimeout initUCOpts, + ExConfig.exploreParallel = exploreParallel initUCOpts, + ExConfig.exploreSkipFunctions = skipFunctions initUCOpts, + ExConfig.exploreSpecs = specs + }) + else + Config.CrashEquivalence + (EqConfig.EquivalenceConfig + { EqConfig.equivOrOrder = + if crashEquivalence initUCOpts + then EqConfig.Equivalence + else EqConfig.Order, + EqConfig.equivModule = crashOrder initUCOpts, + EqConfig.equivEntryPoints = entryPoints initUCOpts + }) + + checkFromDoc :: Text checkFromDoc = "Check inferred contracts by symbolically executing from this function" From 843a7822b76d26260467e16bea989d21844a9dbf Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 13:23:54 -0400 Subject: [PATCH 24/40] uc-crux-llvm: Add more docs to matchPreconds --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index a93c55242..7362f9037 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -62,7 +62,15 @@ import UCCrux.LLVM.Specs.Type (Specs) import qualified UCCrux.LLVM.Specs.Type as Spec {- ORMOLU_ENABLE -} --- | Collapse all the preconditions of a 'Spec' to a single predicate +-- | Collapse all the preconditions of a 'Spec' to a single predicate. +-- +-- The predicate denotes whether or not the precondition holds in the given +-- state, where a state is the arguments, ('Ctx.Assignment' of +-- 'Crucible.RegEntry') plus the LLVM memory ('MemImpl'). +-- +-- Used in 'applySpecs' to construct the predicates determining which spec's +-- postcondition gets applied, i.e., the predicates governing a chain of +-- symbolic branches. matchPreconds :: IsSymInterface sym => HasLLVMAnn sym => @@ -70,9 +78,13 @@ matchPreconds :: (?memOpts :: MemOptions) => ModuleContext m arch -> sym -> + -- | LLVM memory MemImpl sym -> + -- | Types of function arguments Ctx.Assignment (FullTypeRepr m) argTypes -> + -- | Preconditions over arguments and memory Spec.SpecPreconds m argTypes -> + -- | Arguments to function Ctx.Assignment (Crucible.RegEntry sym) (MapToCrucibleType arch argTypes) -> IO (What4.Pred sym) matchPreconds modCtx sym mem argFTys preconds args = From a62a6276568e2f6686c3cb969601e624fb4f02a3 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 13:36:21 -0400 Subject: [PATCH 25/40] uc-crux-llvm: Heed warning on symbolicBranches --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 25 ++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index 7362f9037..ff6c6a08e 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE TypeOperators #-} {- Module : UCCrux.LLVM.Specs.Apply Description : Apply collections of specifications for LLVM functions @@ -40,6 +41,7 @@ import qualified What4.Interface as What4 -- crucible import qualified Lang.Crucible.Backend as Crucible import Lang.Crucible.Backend (IsSymInterface) +import qualified Lang.Crucible.Simulator.RegMap as Crucible import qualified Lang.Crucible.Simulator as Crucible -- crucible-llvm @@ -170,10 +172,17 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = specs' <- traverse (\s -> (s,) <$> liftIO (matchPre s)) (Spec.getSpecs specs) + let argsSize = Ctx.size args + cargsSize <- Crucible.regMapSize <$> Crucible.getOverrideArgs + -- Create one symbolic branch per Spec, conditioned on the preconditions let specBranches = [ ( precond - , applyPost bak modCtx tracker funcSymb fsRep mvar spec args + , -- Don't use args from outer scope directly (see warning on + -- 'Crucible.symbolicBranches'). + do args' <- Crucible.getOverrideArgs + let (_, Crucible.RegMap args'') = splitRegs cargsSize argsSize args' + applyPost bak modCtx tracker funcSymb fsRep mvar spec args'' , Nothing ) | (spec, precond) <- toList specs' @@ -183,7 +192,9 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = -- applies a minimal postcondition. let fallbackBranch = ( What4.truePred sym - , liftIO $ do + , -- NB: Can't use 'args' in this block, see warning on + -- 'Crucible.symbolicBranches'. + liftIO $ do -- TODO(lb): this behavior should depend on spec config, see TODO -- on 'Specs' Crucible.addFailedAssertion @@ -193,4 +204,12 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = ) let branches = specBranches ++ [fallbackBranch] - Crucible.symbolicBranches Crucible.emptyRegMap branches + Crucible.symbolicBranches (Crucible.RegMap args) branches + where + splitRegs :: + Ctx.Size ctx -> + Ctx.Size ctx' -> + Crucible.RegMap sym (ctx Ctx.<+> ctx') -> + (Crucible.RegMap sym ctx, Crucible.RegMap sym ctx') + splitRegs sz sz' (Crucible.RegMap m) = + (Crucible.RegMap (Ctx.take sz sz' m), Crucible.RegMap (Ctx.drop sz sz' m)) From 58a0462f36a65f81849cbbaed1a17501916aab96 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 13:54:27 -0400 Subject: [PATCH 26/40] uc-crux-llvm: Factor out and document symbolicBranches' --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 83 ++++++++++++++------- 1 file changed, 58 insertions(+), 25 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index ff6c6a08e..38485adac 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE TypeOperators #-} {- Module : UCCrux.LLVM.Specs.Apply Description : Apply collections of specifications for LLVM functions @@ -17,6 +16,7 @@ Should be easy enough given the information in 'CheckedConstraint'. {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeOperators #-} module UCCrux.LLVM.Specs.Apply ( applySpecs @@ -37,6 +37,7 @@ import qualified Data.Parameterized.Context as Ctx -- what4 import qualified What4.Interface as What4 +import qualified What4.ProgramLoc as What4 -- crucible import qualified Lang.Crucible.Backend as Crucible @@ -131,6 +132,49 @@ applyPost bak modCtx tracker funcSymb fsRep mvar spec args = Crucible.modifyGlobal mvar $ \mem -> liftIO (applyPostcond bak modCtx tracker funcSymb post retTy mem args) +-- | A variant of 'Crucible.symbolicBranches'. +-- +-- Useful when the branches use a 'Crucible.RegMap' of values of types @args@ +-- that are unrelated to the argument types of the override (@args'@). +-- +-- For convenience, passes the given 'Crucible.RegMap' of type @args@ directly +-- to the action taken in each branch, rather than requiring each branch to call +-- 'Crucible.getOverrideArgs' and @splitRegs@. +symbolicBranches' :: forall p sym ext rtp args args' res a. + IsSymInterface sym => + -- | Argument values for the branches + Crucible.RegMap sym args -> + -- | Branches to consider + [ ( What4.Pred sym + , Crucible.RegMap sym args -> Crucible.OverrideSim p sym ext rtp (args' Ctx.<+> args) res a + , Maybe What4.Position + ) + ] -> + Crucible.OverrideSim p sym ext rtp args' res a +symbolicBranches' args branches = + do let argsSize = Crucible.regMapSize args + args'Size <- Crucible.regMapSize <$> Crucible.getOverrideArgs + let branches' = + [ ( precond + , -- Don't use args from outer scope directly (see warning on + -- 'Crucible.symbolicBranches'). + do args'args <- Crucible.getOverrideArgs + let (_, safeArgs) = splitRegs args'Size argsSize args'args + action safeArgs + , pos + ) + | (precond, action, pos) <- branches + ] + Crucible.symbolicBranches args branches' + where + splitRegs :: + Ctx.Size ctx -> + Ctx.Size ctx' -> + Crucible.RegMap sym (ctx Ctx.<+> ctx') -> + (Crucible.RegMap sym ctx, Crucible.RegMap sym ctx') + splitRegs sz sz' (Crucible.RegMap m) = + (Crucible.RegMap (Ctx.take sz sz' m), Crucible.RegMap (Ctx.drop sz sz' m)) + -- | Apply a collection of specs (a 'Specs') to the current program state. -- -- Creates one symbolic branches per spec, as described on the Haddock for @@ -172,17 +216,13 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = specs' <- traverse (\s -> (s,) <$> liftIO (matchPre s)) (Spec.getSpecs specs) - let argsSize = Ctx.size args - cargsSize <- Crucible.regMapSize <$> Crucible.getOverrideArgs - -- Create one symbolic branch per Spec, conditioned on the preconditions let specBranches = [ ( precond - , -- Don't use args from outer scope directly (see warning on - -- 'Crucible.symbolicBranches'). - do args' <- Crucible.getOverrideArgs - let (_, Crucible.RegMap args'') = splitRegs cargsSize argsSize args' - applyPost bak modCtx tracker funcSymb fsRep mvar spec args'' + , -- Can't use 'args' in this block, see warning on + -- 'Crucible.symbolicBranches'. + \(Crucible.RegMap args') -> + applyPost bak modCtx tracker funcSymb fsRep mvar spec args' , Nothing ) | (spec, precond) <- toList specs' @@ -192,24 +232,17 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = -- applies a minimal postcondition. let fallbackBranch = ( What4.truePred sym - , -- NB: Can't use 'args' in this block, see warning on + , -- Can't use 'args' in this block, see warning on -- 'Crucible.symbolicBranches'. - liftIO $ do - -- TODO(lb): this behavior should depend on spec config, see TODO - -- on 'Specs' - Crucible.addFailedAssertion - bak - (Crucible.GenericSimError "No spec applied!") + \_args -> + liftIO $ do + -- TODO(lb): this behavior should depend on spec config, see TODO + -- on 'Specs' + Crucible.addFailedAssertion + bak + (Crucible.GenericSimError "No spec applied!") , Nothing ) let branches = specBranches ++ [fallbackBranch] - Crucible.symbolicBranches (Crucible.RegMap args) branches - where - splitRegs :: - Ctx.Size ctx -> - Ctx.Size ctx' -> - Crucible.RegMap sym (ctx Ctx.<+> ctx') -> - (Crucible.RegMap sym ctx, Crucible.RegMap sym ctx') - splitRegs sz sz' (Crucible.RegMap m) = - (Crucible.RegMap (Ctx.take sz sz' m), Crucible.RegMap (Ctx.drop sz sz' m)) + symbolicBranches' (Crucible.RegMap args) branches From 64966d7ae4e5c4b485610707ad1ea2c96759b1ad Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 13:57:40 -0400 Subject: [PATCH 27/40] uc-crux-llvm: Use overrideError in fallback branch of symbolicBranches --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index 38485adac..cc8e9973e 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -235,12 +235,9 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = , -- Can't use 'args' in this block, see warning on -- 'Crucible.symbolicBranches'. \_args -> - liftIO $ do - -- TODO(lb): this behavior should depend on spec config, see TODO - -- on 'Specs' - Crucible.addFailedAssertion - bak - (Crucible.GenericSimError "No spec applied!") + -- TODO(lb): this behavior should depend on spec config, see TODO + -- on 'Specs' + do Crucible.overrideError (Crucible.GenericSimError "No spec applied!") , Nothing ) From 5631ed06b3e44542f6c62c2d71c194179225bc81 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 14:32:09 -0400 Subject: [PATCH 28/40] uc-crux-llvm: Clarify the purpose of SimulatorHooks --- uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs | 4 ++-- uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs | 10 ++++++++-- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs index e1e02468f..dbce90bfc 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs @@ -101,6 +101,7 @@ bugfindingLoopWithCallbacks :: CruxOptions -> LLVMOptions -> Crucible.HandleAllocator -> + -- | Customizations to the symbolic execution process. See 'SimulatorHooks'. Sim.SimulatorCallbacks m arch argTypes (Sim.UCCruxSimulationResult m arch argTypes, r) -> IO (BugfindingResult m arch argTypes, Seq (Sim.UCCruxSimulationResult m arch argTypes, r)) bugfindingLoopWithCallbacks appCtx modCtx funCtx cfg cruxOpts llvmOpts halloc callbacks = @@ -224,8 +225,7 @@ bugfindingLoop appCtx modCtx funCtx cfg cruxOpts llvmOpts halloc specs = swap (cruxResult, ucCruxResult) = (ucCruxResult, cruxResult) post (result, results) = (result, fmap fst results) - -- Default (do-nothing) callbacks, except they register overrides for all - -- the provided function specs + -- Callbacks that register overrides for all the provided function specs. callbacks = Sim.addOverrides (map (uncurry mkSpecOverride) (Map.toList specs)) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs index 84221c22d..f7ebd19a8 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs @@ -159,7 +159,11 @@ data UCCruxSimulationResult m arch argTypes = UCCruxSimulationResult explanations :: [Located (Explanation m arch argTypes)] } --- | Based on 'Crux.SimulatorHooks' +-- | Like 'Crux.SimulatorHooks', these hooks provide the ability to customize +-- the symbolic execution process. In particular, they allow for registering +-- additional overrides via 'createOverrideHooks', and post-processing the +-- results of symbolic execution with access to the symbolic backend via +-- 'resultHook'. data SimulatorHooks sym bak m arch argTypes r = SimulatorHooks { createOverrideHooks :: [SymCreateOverrideFn m sym bak arch] @@ -175,7 +179,9 @@ data SimulatorHooks sym bak m arch argTypes r = } deriving Functor --- | Based on 'Crux.SimulatorCallbacks' +-- | Callbacks that customize the symbolic execution process. +-- +-- Compare to 'Crux.SimulatorCallbacks'. newtype SimulatorCallbacks m arch (argTypes :: Ctx (FullType m)) r = SimulatorCallbacks { getSimulatorCallbacks :: From 8561a53dce7045b6c75e7107366b01a7b9c9536d Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 19 Jul 2022 14:58:06 -0400 Subject: [PATCH 29/40] uc-crux-llvm: Add comment to SpecPreconds --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs index abc8c5148..59bade104 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs @@ -42,6 +42,9 @@ import UCCrux.LLVM.Precondition (emptyArgPreconds) import UCCrux.LLVM.Postcondition.Type (Postcond) -- | Preconditions required to hold for a 'Spec' to execute. +-- +-- Currently only holds preconditions on arguments, but should be extended with +-- preconditions on globals at some point. data SpecPreconds m (args :: Ctx (FullType m)) = SpecPreconds { -- | Preconditions on arguments to the specified function From 1344d391f7aa96bf169a9b0f86f43cc127f810c5 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Jul 2022 10:04:12 -0400 Subject: [PATCH 30/40] crucible: Add notdetBranches, clarify symbolicBranches docs --- .../Lang/Crucible/Simulator/OverrideSim.hs | 35 +++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs b/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs index cffa1b9c4..36ab819ff 100644 --- a/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs +++ b/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs @@ -37,6 +37,7 @@ module Lang.Crucible.Simulator.OverrideSim , overrideAbort , symbolicBranch , symbolicBranches + , notdetBranches , overrideReturn , overrideReturn' -- * Function calls @@ -86,6 +87,8 @@ import Data.List (foldl') import qualified Data.Parameterized.Context as Ctx import Data.Proxy import qualified Data.Text as T +import Data.Traversable (for) +import Numeric.Natural (Natural) import System.Exit import System.IO import System.IO.Error @@ -526,6 +529,9 @@ symbolicBranch p thn_args thn thn_pos els_args els els_pos = -- series of branches, one for each element of the list. The semantics of -- this construct is that the predicates are evaluated in order, until -- the first one that evaluates true; this branch will be the taken branch. +-- In other words, this operates like a chain of if-then-else statements; +-- later branches assume that earlier branches were not taken. +-- -- If no predicate is true, the construct will abort with a @VariantOptionsExhausted@ -- reason. If you wish to report an error condition instead, you should add a -- final default case with a true predicate that calls @overrideError@. @@ -555,6 +561,35 @@ symbolicBranches new_args xs0 = in overrideSymbolicBranch p all_args m' mpos old_args (go (i+1) xs) (Just (OtherPos msg)) go (0::Integer) xs0 +-- | Non-deterministically choose among several feasible branches. +-- +-- Unlike 'symbolicBranches', this function does not take only the first branch +-- with a predicate that evaluates to true; instead it takes /all/ branches with +-- predicates that evaluate to true. Each branch will not assume that other +-- branches weren't taken. +-- +-- Operationally, this works by by numbering all of the branches from 0 to n, +-- inventing a symbolic integer variable z, and adding z = i (where i ranges +-- from 0 to n) to the branch condition for each branch, and calling +-- 'symbolicBranches' on the result. Even though each branch given to +-- 'symbolicBranches' assumes earlier branches are not taken, each branch +-- condition has the form @(z = i) and p@, so the negation @~((z = i) and p)@ +-- is equivalent to @(z != i) or ~p@, so later branches don't assume the +-- negation of the branch condition of earlier branches (i.e., @~p@). +notdetBranches :: forall p sym ext rtp args new_args res a. + IsSymInterface sym => + RegMap sym new_args {- ^ argument values for the branches -} -> + [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a, Maybe Position)] + {- ^ Branches to consider -} -> + OverrideSim p sym ext rtp args res a +notdetBranches new_args xs0 = + do sym <- getSymInterface + z <- liftIO $ freshNat sym (safeSymbol "notdetBranchesZ") + xs <- for (zip [(0 :: Natural)..] xs0) $ \(i, (p, v, position)) -> + do p' <- liftIO $ andPred sym p =<< natEq sym z =<< natLit sym i + return (p', v, position) + symbolicBranches new_args xs + -------------------------------------------------------------------------------- -- FnBinding From 01901eaccd8bc71b9919c54801c2dc4984195eda Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Jul 2022 11:27:11 -0400 Subject: [PATCH 31/40] crucible-syntax: Add tests for nondetBranches These test the semantics of the nondetBranches construct. --- .../override-nondet-test-0.cbl | 8 +++ .../override-nondet-test-0.out.good | 4 ++ .../override-nondet-test-1.cbl | 8 +++ .../override-nondet-test-1.out.good | 4 ++ .../override-nondet-test-both.cbl | 11 +++ .../override-nondet-test-both.out.good | 72 +++++++++++++++++++ .../override-nondet-test-neither.cbl | 9 +++ .../override-nondet-test-neither.out.good | 20 ++++++ crucible-syntax/test/Overrides.hs | 27 ++++++- 9 files changed, 162 insertions(+), 1 deletion(-) create mode 100644 crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl create mode 100644 crucible-syntax/test-data/simulator-tests/override-nondet-test-0.out.good create mode 100644 crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl create mode 100644 crucible-syntax/test-data/simulator-tests/override-nondet-test-1.out.good create mode 100644 crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl create mode 100644 crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good create mode 100644 crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl create mode 100644 crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl b/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl new file mode 100644 index 000000000..5c65e5844 --- /dev/null +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl @@ -0,0 +1,8 @@ +(defun @main () Integer + (start start: + (let x (fresh Integer)) + (let y (fresh Integer)) + (let z (funcall @notdetBranchesTest 0 x y)) + (assert! (equal? z x) "should be true!") + (return z)) +) \ No newline at end of file diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.out.good b/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.out.good new file mode 100644 index 000000000..a0dc0d91d --- /dev/null +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.out.good @@ -0,0 +1,4 @@ +==== Begin Simulation ==== + +==== Finish Simulation ==== +==== No proof obligations ==== diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl b/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl new file mode 100644 index 000000000..021325ba7 --- /dev/null +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl @@ -0,0 +1,8 @@ +(defun @main () Integer + (start start: + (let x (fresh Integer)) + (let y (fresh Integer)) + (let z (funcall @notdetBranchesTest 1 x y)) + (assert! (equal? z y) "should be true!") + (return z)) +) \ No newline at end of file diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.out.good b/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.out.good new file mode 100644 index 000000000..a0dc0d91d --- /dev/null +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.out.good @@ -0,0 +1,4 @@ +==== Begin Simulation ==== + +==== Finish Simulation ==== +==== No proof obligations ==== diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl b/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl new file mode 100644 index 000000000..c3513931c --- /dev/null +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl @@ -0,0 +1,11 @@ +(defun @main () Integer + (start start: + (let w (fresh Integer)) + (let x (fresh Integer)) + (let y (fresh Integer)) + (assume! (or (equal? w 0) (equal? w 1)) "w is 0 or 1") + (let z (funcall @notdetBranchesTest w x y)) + (assert! (or (equal? z x) (equal? z y)) "should be true!") + (assert! (or (equal? x y) (not (and (equal? z x) (equal? z y)))) "should be true!") + (return z)) +) \ No newline at end of file diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good b/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good new file mode 100644 index 000000000..29c594039 --- /dev/null +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good @@ -0,0 +1,72 @@ +==== Begin Simulation ==== + +==== Finish Simulation ==== +==== Proof obligations ==== +Assuming: +* in main test-data/simulator-tests/override-nondet-test-both.cbl:6:5: w is 0 or 1 + not (and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i))) +* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to after branch 0 + not (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@11:i)) +* The branch in notdetBranchesTest from after branch 0 to after branch 1 + not (and (eq 1 cw@0:i) (eq 1 cnotdetBranchesZ@11:i)) +* The branch in notdetBranchesTest from after branch 1 to default branch + let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + v16 = eq 2 cnotdetBranchesZ@11:i + in and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) v16 +Prove: + default branch: error: in notdetBranchesTest + fall-through branch + false +PROVED +Assuming: +* in main test-data/simulator-tests/override-nondet-test-both.cbl:6:5: w is 0 or 1 + not (and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i))) +* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to after branch 0 + let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + v7 = eq 0 cw@0:i + -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + v12 = eq 0 cnotdetBranchesZ@11:i + in not (and v7 v12 (not (and v7 v12))) +* The branch in notdetBranchesTest from after branch 0 to second branch + let -- test-data/simulator-tests/override-nondet-test-both.cbl:10:5 + v43 = and (not (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnotdetBranchesZ@11:i))) + in not v43 +* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to first branch + let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + v7 = eq 0 cw@0:i + -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + v12 = eq 0 cnotdetBranchesZ@11:i + in not (and v7 v12 (not (and v7 v12))) +Prove: + test-data/simulator-tests/override-nondet-test-both.cbl:8:5: error: in main + should be true! + let -- after branch 2 + v28 = ite (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@11:i)) cx@1:i cy@2:i + in not (and (not (eq v28 cx@1:i)) (not (eq v28 cy@2:i))) +PROVED +Assuming: +* in main test-data/simulator-tests/override-nondet-test-both.cbl:6:5: w is 0 or 1 + not (and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i))) +* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to after branch 0 + let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + v7 = eq 0 cw@0:i + -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + v12 = eq 0 cnotdetBranchesZ@11:i + in not (and v7 v12 (not (and v7 v12))) +* The branch in notdetBranchesTest from after branch 0 to second branch + let -- test-data/simulator-tests/override-nondet-test-both.cbl:10:5 + v54 = and (not (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnotdetBranchesZ@11:i))) + in not v54 +* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to first branch + let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + v7 = eq 0 cw@0:i + -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + v12 = eq 0 cnotdetBranchesZ@11:i + in not (and v7 v12 (not (and v7 v12))) +Prove: + test-data/simulator-tests/override-nondet-test-both.cbl:9:5: error: in main + should be true! + let -- after branch 2 + v28 = ite (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@11:i)) cx@1:i cy@2:i + in not (and (eq v28 cx@1:i) (eq v28 cy@2:i) (not (eq cx@1:i cy@2:i))) +PROVED diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl b/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl new file mode 100644 index 000000000..0fa9b4bdc --- /dev/null +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl @@ -0,0 +1,9 @@ +(defun @main () Integer + (start start: + (let w (fresh Integer)) + (let x (fresh Integer)) + (let y (fresh Integer)) + (assume! (and (not (equal? w 0)) (not (equal? w 1))) "w is not 0 or 1") + (let z (funcall @notdetBranchesTest w x y)) + (return z)) +) \ No newline at end of file diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good b/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good new file mode 100644 index 000000000..127a70338 --- /dev/null +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good @@ -0,0 +1,20 @@ +==== Begin Simulation ==== + +==== Finish Simulation ==== +==== Proof obligations ==== +Assuming: +* in main test-data/simulator-tests/override-nondet-test-neither.cbl:6:5: w is not 0 or 1 + and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) +* The branch in main from test-data/simulator-tests/override-nondet-test-neither.cbl:7:12 to after branch 0 + not (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@12:i)) +* The branch in notdetBranchesTest from after branch 0 to after branch 1 + not (and (eq 1 cw@0:i) (eq 1 cnotdetBranchesZ@12:i)) +* The branch in notdetBranchesTest from after branch 1 to default branch + let -- test-data/simulator-tests/override-nondet-test-neither.cbl:7:12 + v17 = eq 2 cnotdetBranchesZ@12:i + in and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) v17 +Prove: + default branch: error: in notdetBranchesTest + fall-through branch + false +COUNTEREXAMPLE diff --git a/crucible-syntax/test/Overrides.hs b/crucible-syntax/test/Overrides.hs index 1a6d34e4d..fb6d1d1ab 100644 --- a/crucible-syntax/test/Overrides.hs +++ b/crucible-syntax/test/Overrides.hs @@ -39,7 +39,9 @@ setupOverrides _ ha = <*> pure (UseOverride (mkOverride "symbolicBranchTest" symbolicBranchTest)) f2 <- FnBinding <$> mkHandle ha "symbolicBranchesTest" <*> pure (UseOverride (mkOverride "symbolicBranchesTest" symbolicBranchesTest)) - return [(f1, InternalPos),(f2,InternalPos)] + f3 <- FnBinding <$> mkHandle ha "notdetBranchesTest" + <*> pure (UseOverride (mkOverride "notdetBranchesTest" notdetBranchesTest)) + return [(f1, InternalPos),(f2,InternalPos),(f3,InternalPos)] -- Test the @symbolicBranch@ override operation. @@ -91,3 +93,26 @@ symbolicBranchesTest = liftIO $ intAdd sym y x2 b4 = overrideError (GenericSimError "fall-through branch") + + +-- Test the @notdetBranches@ override operation. +-- +-- If the first argument is zero, returns the second argument. If it is one, +-- returns the third argument. If it could be either, returns both (i.e., +-- nondeterministic choice). If it couldn't be either, errors out. +notdetBranchesTest :: IsSymInterface sym => + OverrideSim p sym ext r + (EmptyCtx ::> IntegerType ::> IntegerType ::> IntegerType) IntegerType (RegValue sym IntegerType) +notdetBranchesTest = + do sym <- getSymInterface + args <- getOverrideArgs + cond <- reg @0 <$> getOverrideArgs + p1 <- liftIO $ intEq sym cond =<< intLit sym 0 + p2 <- liftIO $ intEq sym cond =<< intLit sym 1 + fallbackPred <- liftIO $ notPred sym =<< orPred sym p1 p2 + let fallback = overrideError (GenericSimError "fall-through branch") + notdetBranches args + [ (p1, reg @1 <$> getOverrideArgs, Just (OtherPos "first branch")) + , (p2, reg @2 <$> getOverrideArgs, Just (OtherPos "second branch")) + , (fallbackPred, fallback, Just (OtherPos "default branch")) + ] From 5787ea758e7d299c50941a12180c80c2236fef52 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Jul 2022 11:48:04 -0400 Subject: [PATCH 32/40] crucible, crucible-syntax: Fix typo (notdet -> nondet) --- .../override-nondet-test-0.cbl | 2 +- .../override-nondet-test-1.cbl | 2 +- .../override-nondet-test-both.cbl | 2 +- .../override-nondet-test-both.out.good | 32 +++++++++---------- .../override-nondet-test-neither.cbl | 2 +- .../override-nondet-test-neither.out.good | 12 +++---- crucible-syntax/test/Overrides.hs | 12 +++---- .../Lang/Crucible/Simulator/OverrideSim.hs | 8 ++--- 8 files changed, 36 insertions(+), 36 deletions(-) diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl b/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl index 5c65e5844..8fc883d57 100644 --- a/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl @@ -2,7 +2,7 @@ (start start: (let x (fresh Integer)) (let y (fresh Integer)) - (let z (funcall @notdetBranchesTest 0 x y)) + (let z (funcall @nondetBranchesTest 0 x y)) (assert! (equal? z x) "should be true!") (return z)) ) \ No newline at end of file diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl b/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl index 021325ba7..31b94026d 100644 --- a/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl @@ -2,7 +2,7 @@ (start start: (let x (fresh Integer)) (let y (fresh Integer)) - (let z (funcall @notdetBranchesTest 1 x y)) + (let z (funcall @nondetBranchesTest 1 x y)) (assert! (equal? z y) "should be true!") (return z)) ) \ No newline at end of file diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl b/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl index c3513931c..5603e097e 100644 --- a/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl @@ -4,7 +4,7 @@ (let x (fresh Integer)) (let y (fresh Integer)) (assume! (or (equal? w 0) (equal? w 1)) "w is 0 or 1") - (let z (funcall @notdetBranchesTest w x y)) + (let z (funcall @nondetBranchesTest w x y)) (assert! (or (equal? z x) (equal? z y)) "should be true!") (assert! (or (equal? x y) (not (and (equal? z x) (equal? z y)))) "should be true!") (return z)) diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good b/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good index 29c594039..8154b4293 100644 --- a/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good @@ -6,15 +6,15 @@ Assuming: * in main test-data/simulator-tests/override-nondet-test-both.cbl:6:5: w is 0 or 1 not (and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i))) * The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to after branch 0 - not (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@11:i)) -* The branch in notdetBranchesTest from after branch 0 to after branch 1 - not (and (eq 1 cw@0:i) (eq 1 cnotdetBranchesZ@11:i)) -* The branch in notdetBranchesTest from after branch 1 to default branch + not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i)) +* The branch in nondetBranchesTest from after branch 0 to after branch 1 + not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i)) +* The branch in nondetBranchesTest from after branch 1 to default branch let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 - v16 = eq 2 cnotdetBranchesZ@11:i + v16 = eq 2 cnondetBranchesZ@11:i in and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) v16 Prove: - default branch: error: in notdetBranchesTest + default branch: error: in nondetBranchesTest fall-through branch false PROVED @@ -25,23 +25,23 @@ Assuming: let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 v7 = eq 0 cw@0:i -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 - v12 = eq 0 cnotdetBranchesZ@11:i + v12 = eq 0 cnondetBranchesZ@11:i in not (and v7 v12 (not (and v7 v12))) -* The branch in notdetBranchesTest from after branch 0 to second branch +* The branch in nondetBranchesTest from after branch 0 to second branch let -- test-data/simulator-tests/override-nondet-test-both.cbl:10:5 - v43 = and (not (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnotdetBranchesZ@11:i))) + v43 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i))) in not v43 * The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to first branch let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 v7 = eq 0 cw@0:i -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 - v12 = eq 0 cnotdetBranchesZ@11:i + v12 = eq 0 cnondetBranchesZ@11:i in not (and v7 v12 (not (and v7 v12))) Prove: test-data/simulator-tests/override-nondet-test-both.cbl:8:5: error: in main should be true! let -- after branch 2 - v28 = ite (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@11:i)) cx@1:i cy@2:i + v28 = ite (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i)) cx@1:i cy@2:i in not (and (not (eq v28 cx@1:i)) (not (eq v28 cy@2:i))) PROVED Assuming: @@ -51,22 +51,22 @@ Assuming: let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 v7 = eq 0 cw@0:i -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 - v12 = eq 0 cnotdetBranchesZ@11:i + v12 = eq 0 cnondetBranchesZ@11:i in not (and v7 v12 (not (and v7 v12))) -* The branch in notdetBranchesTest from after branch 0 to second branch +* The branch in nondetBranchesTest from after branch 0 to second branch let -- test-data/simulator-tests/override-nondet-test-both.cbl:10:5 - v54 = and (not (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnotdetBranchesZ@11:i))) + v54 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i))) in not v54 * The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to first branch let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 v7 = eq 0 cw@0:i -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 - v12 = eq 0 cnotdetBranchesZ@11:i + v12 = eq 0 cnondetBranchesZ@11:i in not (and v7 v12 (not (and v7 v12))) Prove: test-data/simulator-tests/override-nondet-test-both.cbl:9:5: error: in main should be true! let -- after branch 2 - v28 = ite (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@11:i)) cx@1:i cy@2:i + v28 = ite (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i)) cx@1:i cy@2:i in not (and (eq v28 cx@1:i) (eq v28 cy@2:i) (not (eq cx@1:i cy@2:i))) PROVED diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl b/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl index 0fa9b4bdc..f80141765 100644 --- a/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl @@ -4,6 +4,6 @@ (let x (fresh Integer)) (let y (fresh Integer)) (assume! (and (not (equal? w 0)) (not (equal? w 1))) "w is not 0 or 1") - (let z (funcall @notdetBranchesTest w x y)) + (let z (funcall @nondetBranchesTest w x y)) (return z)) ) \ No newline at end of file diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good b/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good index 127a70338..0fc875c03 100644 --- a/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good +++ b/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good @@ -6,15 +6,15 @@ Assuming: * in main test-data/simulator-tests/override-nondet-test-neither.cbl:6:5: w is not 0 or 1 and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) * The branch in main from test-data/simulator-tests/override-nondet-test-neither.cbl:7:12 to after branch 0 - not (and (eq 0 cw@0:i) (eq 0 cnotdetBranchesZ@12:i)) -* The branch in notdetBranchesTest from after branch 0 to after branch 1 - not (and (eq 1 cw@0:i) (eq 1 cnotdetBranchesZ@12:i)) -* The branch in notdetBranchesTest from after branch 1 to default branch + not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@12:i)) +* The branch in nondetBranchesTest from after branch 0 to after branch 1 + not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@12:i)) +* The branch in nondetBranchesTest from after branch 1 to default branch let -- test-data/simulator-tests/override-nondet-test-neither.cbl:7:12 - v17 = eq 2 cnotdetBranchesZ@12:i + v17 = eq 2 cnondetBranchesZ@12:i in and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) v17 Prove: - default branch: error: in notdetBranchesTest + default branch: error: in nondetBranchesTest fall-through branch false COUNTEREXAMPLE diff --git a/crucible-syntax/test/Overrides.hs b/crucible-syntax/test/Overrides.hs index fb6d1d1ab..41e3d1cb0 100644 --- a/crucible-syntax/test/Overrides.hs +++ b/crucible-syntax/test/Overrides.hs @@ -39,8 +39,8 @@ setupOverrides _ ha = <*> pure (UseOverride (mkOverride "symbolicBranchTest" symbolicBranchTest)) f2 <- FnBinding <$> mkHandle ha "symbolicBranchesTest" <*> pure (UseOverride (mkOverride "symbolicBranchesTest" symbolicBranchesTest)) - f3 <- FnBinding <$> mkHandle ha "notdetBranchesTest" - <*> pure (UseOverride (mkOverride "notdetBranchesTest" notdetBranchesTest)) + f3 <- FnBinding <$> mkHandle ha "nondetBranchesTest" + <*> pure (UseOverride (mkOverride "nondetBranchesTest" nondetBranchesTest)) return [(f1, InternalPos),(f2,InternalPos),(f3,InternalPos)] @@ -95,15 +95,15 @@ symbolicBranchesTest = b4 = overrideError (GenericSimError "fall-through branch") --- Test the @notdetBranches@ override operation. +-- Test the @nondetBranches@ override operation. -- -- If the first argument is zero, returns the second argument. If it is one, -- returns the third argument. If it could be either, returns both (i.e., -- nondeterministic choice). If it couldn't be either, errors out. -notdetBranchesTest :: IsSymInterface sym => +nondetBranchesTest :: IsSymInterface sym => OverrideSim p sym ext r (EmptyCtx ::> IntegerType ::> IntegerType ::> IntegerType) IntegerType (RegValue sym IntegerType) -notdetBranchesTest = +nondetBranchesTest = do sym <- getSymInterface args <- getOverrideArgs cond <- reg @0 <$> getOverrideArgs @@ -111,7 +111,7 @@ notdetBranchesTest = p2 <- liftIO $ intEq sym cond =<< intLit sym 1 fallbackPred <- liftIO $ notPred sym =<< orPred sym p1 p2 let fallback = overrideError (GenericSimError "fall-through branch") - notdetBranches args + nondetBranches args [ (p1, reg @1 <$> getOverrideArgs, Just (OtherPos "first branch")) , (p2, reg @2 <$> getOverrideArgs, Just (OtherPos "second branch")) , (fallbackPred, fallback, Just (OtherPos "default branch")) diff --git a/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs b/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs index 36ab819ff..e586ac6fe 100644 --- a/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs +++ b/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs @@ -37,7 +37,7 @@ module Lang.Crucible.Simulator.OverrideSim , overrideAbort , symbolicBranch , symbolicBranches - , notdetBranches + , nondetBranches , overrideReturn , overrideReturn' -- * Function calls @@ -576,15 +576,15 @@ symbolicBranches new_args xs0 = -- condition has the form @(z = i) and p@, so the negation @~((z = i) and p)@ -- is equivalent to @(z != i) or ~p@, so later branches don't assume the -- negation of the branch condition of earlier branches (i.e., @~p@). -notdetBranches :: forall p sym ext rtp args new_args res a. +nondetBranches :: forall p sym ext rtp args new_args res a. IsSymInterface sym => RegMap sym new_args {- ^ argument values for the branches -} -> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a, Maybe Position)] {- ^ Branches to consider -} -> OverrideSim p sym ext rtp args res a -notdetBranches new_args xs0 = +nondetBranches new_args xs0 = do sym <- getSymInterface - z <- liftIO $ freshNat sym (safeSymbol "notdetBranchesZ") + z <- liftIO $ freshNat sym (safeSymbol "nondetBranchesZ") xs <- for (zip [(0 :: Natural)..] xs0) $ \(i, (p, v, position)) -> do p' <- liftIO $ andPred sym p =<< natEq sym z =<< natLit sym i return (p', v, position) From 5150b997a8b26bb08ec3a5629a6538cf6de48883 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Jul 2022 12:54:13 -0400 Subject: [PATCH 33/40] crucible: Expand Haddock on nondetBranches --- crucible/src/Lang/Crucible/Simulator/OverrideSim.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs b/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs index e586ac6fe..13a9dff89 100644 --- a/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs +++ b/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs @@ -568,6 +568,10 @@ symbolicBranches new_args xs0 = -- predicates that evaluate to true. Each branch will not assume that other -- branches weren't taken. -- +-- As with 'symbolicBranch', any symbolic values needed by the branches should be +-- placed into the @RegMap@ argument and retrieved when needed. See the comment +-- on 'symbolicBranch'. +-- -- Operationally, this works by by numbering all of the branches from 0 to n, -- inventing a symbolic integer variable z, and adding z = i (where i ranges -- from 0 to n) to the branch condition for each branch, and calling From 157e1040085b6cfa99c93f90d0dd9eb50c253a57 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Jul 2022 13:18:36 -0400 Subject: [PATCH 34/40] uc-crux-llvm: Use nondetBranches instead of symbolicBranches --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 84 +++++++++++++-------- uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs | 11 +-- 2 files changed, 56 insertions(+), 39 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index cc8e9973e..9f756901f 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -13,6 +13,7 @@ Should be easy enough given the information in 'CheckedConstraint'. {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} @@ -132,26 +133,55 @@ applyPost bak modCtx tracker funcSymb fsRep mvar spec args = Crucible.modifyGlobal mvar $ \mem -> liftIO (applyPostcond bak modCtx tracker funcSymb post retTy mem args) --- | A variant of 'Crucible.symbolicBranches'. +-- | Like 'nondetBranches', but with a fallback case. -- --- Useful when the branches use a 'Crucible.RegMap' of values of types @args@ --- that are unrelated to the argument types of the override (@args'@). +-- The fallback case has a branch condition equivalent to the negation of the +-- disjunction of the branch conditions of all the supplied branches; i.e., it +-- is taken just when none of the other branches are. +nondetBranchesWithFallback :: forall p sym ext rtp args new_args res a. + IsSymInterface sym => + -- | Argument values for the branches + Crucible.RegMap sym new_args -> + -- | Branches to consider + [ ( What4.Pred sym + , Crucible.OverrideSim p sym ext rtp (args Ctx.<+> new_args) res a + , Maybe What4.Position + ) + ] -> + -- | Fallback branch + Crucible.OverrideSim p sym ext rtp (args Ctx.<+> new_args) res a -> + Crucible.OverrideSim p sym ext rtp args res a +nondetBranchesWithFallback newArgs branches fallbackBranch = + do sym <- Crucible.getSymInterface + orPred <- liftIO $ What4.orOneOf sym Lens.folded [p | (p, _, _) <- branches] + fallbackPred <- liftIO $ What4.notPred sym orPred + let p = (Just (What4.OtherPos "fallback branch")) + Crucible.nondetBranches newArgs ((fallbackPred, fallbackBranch, p):branches) + +-- | A variant of 'nondetBranchesWithFallback'. +-- +-- Does a few things convenient for use in 'applySpecs': -- --- For convenience, passes the given 'Crucible.RegMap' of type @args@ directly --- to the action taken in each branch, rather than requiring each branch to call --- 'Crucible.getOverrideArgs' and @splitRegs@. -symbolicBranches' :: forall p sym ext rtp args args' res a. +-- * Passes in the 'Crucible.RegMap' of values of types @args@ as a function +-- argument to the branches so they don't have to call +-- 'Crucible.getOverrideArgs' and split the arguments. +-- * Enforces that each branch doesn't care about the override argument +-- types (e.g. is polymorphic in @args''@). This isn't functionally necessary, +-- but is perhaps more clear by virtue of being more polymorphic. +nondetBranches' :: forall p sym ext rtp args new_args res a. IsSymInterface sym => -- | Argument values for the branches - Crucible.RegMap sym args -> + Crucible.RegMap sym new_args -> -- | Branches to consider [ ( What4.Pred sym - , Crucible.RegMap sym args -> Crucible.OverrideSim p sym ext rtp (args' Ctx.<+> args) res a + , Crucible.RegMap sym new_args -> Crucible.OverrideSim p sym ext rtp (args Ctx.<+> new_args) res a , Maybe What4.Position ) ] -> - Crucible.OverrideSim p sym ext rtp args' res a -symbolicBranches' args branches = + -- | Fallback branch + Crucible.OverrideSim p sym ext rtp (args Ctx.<+> new_args) res a -> + Crucible.OverrideSim p sym ext rtp args res a +nondetBranches' args branches fallback = do let argsSize = Crucible.regMapSize args args'Size <- Crucible.regMapSize <$> Crucible.getOverrideArgs let branches' = @@ -165,7 +195,7 @@ symbolicBranches' args branches = ) | (precond, action, pos) <- branches ] - Crucible.symbolicBranches args branches' + nondetBranchesWithFallback args branches' fallback where splitRegs :: Ctx.Size ctx -> @@ -177,9 +207,9 @@ symbolicBranches' args branches = -- | Apply a collection of specs (a 'Specs') to the current program state. -- --- Creates one symbolic branches per spec, as described on the Haddock for --- 'Specs' the semantics is that the first spec with a matching precondition has --- its postcondition applied to mutate memory and supply a return value. +-- Creates one symbolic branches per spec; as described on the Haddock for +-- 'Specs' the semantics is that every spec with a true precondition has its +-- postcondition applied to mutate memory and supply a return value. applySpecs :: forall m arch sym bak fs va mft args argTypes p ext r cargs ret. ArchOk arch => @@ -217,7 +247,7 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = traverse (\s -> (s,) <$> liftIO (matchPre s)) (Spec.getSpecs specs) -- Create one symbolic branch per Spec, conditioned on the preconditions - let specBranches = + let branches = [ ( precond , -- Can't use 'args' in this block, see warning on -- 'Crucible.symbolicBranches'. @@ -228,18 +258,10 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = | (spec, precond) <- toList specs' ] - -- Add a fallback branch that (depending on the Spec) either fails or - -- applies a minimal postcondition. - let fallbackBranch = - ( What4.truePred sym - , -- Can't use 'args' in this block, see warning on - -- 'Crucible.symbolicBranches'. - \_args -> - -- TODO(lb): this behavior should depend on spec config, see TODO - -- on 'Specs' - do Crucible.overrideError (Crucible.GenericSimError "No spec applied!") - , Nothing - ) - - let branches = specBranches ++ [fallbackBranch] - symbolicBranches' (Crucible.RegMap args) branches + -- TODO(lb): this behavior should depend on spec config, see TODO + -- on 'Specs' + let err = Crucible.GenericSimError "No spec applied!" + nondetBranches' + (Crucible.RegMap args) + branches + (Crucible.overrideError err) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs index 59bade104..e63791114 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs @@ -108,14 +108,11 @@ data Spec m fs -- | A collection of specifications for a function. -- --- The semantics are that the specs are tried in order. The first one that has a --- matching precondition results in its postcondition being applied, just as in --- 'Lang.Crucible.Simulator.OverrideSim.symbolicBranches'. +-- The semantics are that the specs are tried in order. All specs with true +-- preconditions have their postcondition applied; they are used as branches in +-- 'Lang.Crucible.Simulator.OverrideSim.nondetBranches'. -- -- TODO(lb): Configure whether matching is an error. --- --- TODO(lb): A semantics of non-deterministic choice rather than first-wins --- would probably be superior. newtype Specs m fs = Specs { getSpecs :: NonEmpty (Spec m fs) } @@ -145,5 +142,3 @@ minimalSpecs = Specs . neSingleton . minimalSpec where -- | Added as NE.singleton in base-4.15/GHC 9. neSingleton x = x NE.:| [] - - From d1048817487bd14c32badd41dfff2047f51219e1 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Jul 2022 13:23:18 -0400 Subject: [PATCH 35/40] uc-crux-llvm: Inline extraneous/confusing helper function --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 66 +++++---------------- 1 file changed, 16 insertions(+), 50 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index 9f756901f..1807ebcd5 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -158,53 +158,6 @@ nondetBranchesWithFallback newArgs branches fallbackBranch = let p = (Just (What4.OtherPos "fallback branch")) Crucible.nondetBranches newArgs ((fallbackPred, fallbackBranch, p):branches) --- | A variant of 'nondetBranchesWithFallback'. --- --- Does a few things convenient for use in 'applySpecs': --- --- * Passes in the 'Crucible.RegMap' of values of types @args@ as a function --- argument to the branches so they don't have to call --- 'Crucible.getOverrideArgs' and split the arguments. --- * Enforces that each branch doesn't care about the override argument --- types (e.g. is polymorphic in @args''@). This isn't functionally necessary, --- but is perhaps more clear by virtue of being more polymorphic. -nondetBranches' :: forall p sym ext rtp args new_args res a. - IsSymInterface sym => - -- | Argument values for the branches - Crucible.RegMap sym new_args -> - -- | Branches to consider - [ ( What4.Pred sym - , Crucible.RegMap sym new_args -> Crucible.OverrideSim p sym ext rtp (args Ctx.<+> new_args) res a - , Maybe What4.Position - ) - ] -> - -- | Fallback branch - Crucible.OverrideSim p sym ext rtp (args Ctx.<+> new_args) res a -> - Crucible.OverrideSim p sym ext rtp args res a -nondetBranches' args branches fallback = - do let argsSize = Crucible.regMapSize args - args'Size <- Crucible.regMapSize <$> Crucible.getOverrideArgs - let branches' = - [ ( precond - , -- Don't use args from outer scope directly (see warning on - -- 'Crucible.symbolicBranches'). - do args'args <- Crucible.getOverrideArgs - let (_, safeArgs) = splitRegs args'Size argsSize args'args - action safeArgs - , pos - ) - | (precond, action, pos) <- branches - ] - nondetBranchesWithFallback args branches' fallback - where - splitRegs :: - Ctx.Size ctx -> - Ctx.Size ctx' -> - Crucible.RegMap sym (ctx Ctx.<+> ctx') -> - (Crucible.RegMap sym ctx, Crucible.RegMap sym ctx') - splitRegs sz sz' (Crucible.RegMap m) = - (Crucible.RegMap (Ctx.take sz sz' m), Crucible.RegMap (Ctx.drop sz sz' m)) - -- | Apply a collection of specs (a 'Specs') to the current program state. -- -- Creates one symbolic branches per spec; as described on the Haddock for @@ -246,13 +199,17 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = specs' <- traverse (\s -> (s,) <$> liftIO (matchPre s)) (Spec.getSpecs specs) + let argsSize = Ctx.size args + cargsSize <- Crucible.regMapSize <$> Crucible.getOverrideArgs -- Create one symbolic branch per Spec, conditioned on the preconditions let branches = [ ( precond , -- Can't use 'args' in this block, see warning on -- 'Crucible.symbolicBranches'. - \(Crucible.RegMap args') -> - applyPost bak modCtx tracker funcSymb fsRep mvar spec args' + do ovArgs <- Crucible.getOverrideArgs + let (_, Crucible.RegMap safeArgs) = + splitRegs cargsSize argsSize ovArgs + applyPost bak modCtx tracker funcSymb fsRep mvar spec safeArgs , Nothing ) | (spec, precond) <- toList specs' @@ -261,7 +218,16 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = -- TODO(lb): this behavior should depend on spec config, see TODO -- on 'Specs' let err = Crucible.GenericSimError "No spec applied!" - nondetBranches' + nondetBranchesWithFallback (Crucible.RegMap args) branches (Crucible.overrideError err) + + where + splitRegs :: + Ctx.Size ctx -> + Ctx.Size ctx' -> + Crucible.RegMap sym (ctx Ctx.<+> ctx') -> + (Crucible.RegMap sym ctx, Crucible.RegMap sym ctx') + splitRegs sz sz' (Crucible.RegMap m) = + (Crucible.RegMap (Ctx.take sz sz' m), Crucible.RegMap (Ctx.drop sz sz' m)) From e0412a212005c4a4a5850e9da12f14f3c3929c77 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Jul 2022 13:31:08 -0400 Subject: [PATCH 36/40] uc-crux-llvm: Refactor applySpecs --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 59 ++++++++++----------- 1 file changed, 28 insertions(+), 31 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index 1807ebcd5..adf0abe39 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -189,39 +189,20 @@ applySpecs :: Crucible.OverrideSim p sym ext r cargs ret (Crucible.RegValue sym (FS.ReturnTypeToCrucibleType arch mft)) applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = - do FS.FuncSigRepr _ argTys _ <- return fsRep + do -- Create one symbolic branch per Spec, conditioned on the preconditions + FS.FuncSigRepr _ argTys _ <- return fsRep let sym = Crucible.backendGetSym bak - - -- Collapse preconditions into predicates mem <- Crucible.readGlobal mvar - let matchPre (Spec.Spec specPre _ _ _) = - matchPreconds modCtx sym mem argTys specPre args - specs' <- - traverse (\s -> (s,) <$> liftIO (matchPre s)) (Spec.getSpecs specs) - - let argsSize = Ctx.size args - cargsSize <- Crucible.regMapSize <$> Crucible.getOverrideArgs - -- Create one symbolic branch per Spec, conditioned on the preconditions - let branches = - [ ( precond - , -- Can't use 'args' in this block, see warning on - -- 'Crucible.symbolicBranches'. - do ovArgs <- Crucible.getOverrideArgs - let (_, Crucible.RegMap safeArgs) = - splitRegs cargsSize argsSize ovArgs - applyPost bak modCtx tracker funcSymb fsRep mvar spec safeArgs - , Nothing - ) - | (spec, precond) <- toList specs' - ] - - -- TODO(lb): this behavior should depend on spec config, see TODO - -- on 'Specs' - let err = Crucible.GenericSimError "No spec applied!" - nondetBranchesWithFallback - (Crucible.RegMap args) - branches - (Crucible.overrideError err) + branches <- + mapM (specToBranch sym mem argTys) (toList (Spec.getSpecs specs)) + + let reason = Crucible.GenericSimError "No spec applied!" + let err = Crucible.overrideError reason + -- TODO(lb): Whether or not to error in the fallback case should depend on + -- spec config, see TODO on 'Specs' + let fallback = err + + nondetBranchesWithFallback (Crucible.RegMap args) branches fallback where splitRegs :: @@ -231,3 +212,19 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = (Crucible.RegMap sym ctx, Crucible.RegMap sym ctx') splitRegs sz sz' (Crucible.RegMap m) = (Crucible.RegMap (Ctx.take sz sz' m), Crucible.RegMap (Ctx.drop sz sz' m)) + + -- Convert a Spec into a branch for 'nondetBranches' + specToBranch sym mem argTys spec@(Spec.Spec specPre _ _ _) = + do precond <- liftIO (matchPreconds modCtx sym mem argTys specPre args) + let argsSize = Ctx.size args + cargsSize <- Crucible.regMapSize <$> Crucible.getOverrideArgs + return $ + ( precond + , -- Can't use 'args' in this block, see warning on + -- 'Crucible.nondetBranches'. + do ovArgs <- Crucible.getOverrideArgs + let (_, Crucible.RegMap safeArgs) = + splitRegs cargsSize argsSize ovArgs + applyPost bak modCtx tracker funcSymb fsRep mvar spec safeArgs + , Nothing -- position + ) From 3a9e07e7539e5bcc6b6c1f3dc74f4b09071008f4 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Jul 2022 13:35:02 -0400 Subject: [PATCH 37/40] uc-crux-llvm: Fix typo --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index adf0abe39..cbfbe696a 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -160,7 +160,7 @@ nondetBranchesWithFallback newArgs branches fallbackBranch = -- | Apply a collection of specs (a 'Specs') to the current program state. -- --- Creates one symbolic branches per spec; as described on the Haddock for +-- Creates one symbolic branch per spec; as described on the Haddock for -- 'Specs' the semantics is that every spec with a true precondition has its -- postcondition applied to mutate memory and supply a return value. applySpecs :: From 65e8016c4039eb5668f4c57d258612249c0ed867 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Jul 2022 13:37:20 -0400 Subject: [PATCH 38/40] uc-crux-llvm: Fix hlint errors (redundant brackets, etc.) --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index cbfbe696a..64e83976c 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -16,7 +16,6 @@ Should be easy enough given the information in 'CheckedConstraint'. {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeOperators #-} module UCCrux.LLVM.Specs.Apply @@ -155,7 +154,7 @@ nondetBranchesWithFallback newArgs branches fallbackBranch = do sym <- Crucible.getSymInterface orPred <- liftIO $ What4.orOneOf sym Lens.folded [p | (p, _, _) <- branches] fallbackPred <- liftIO $ What4.notPred sym orPred - let p = (Just (What4.OtherPos "fallback branch")) + let p = Just (What4.OtherPos "fallback branch") Crucible.nondetBranches newArgs ((fallbackPred, fallbackBranch, p):branches) -- | Apply a collection of specs (a 'Specs') to the current program state. @@ -218,7 +217,7 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = do precond <- liftIO (matchPreconds modCtx sym mem argTys specPre args) let argsSize = Ctx.size args cargsSize <- Crucible.regMapSize <$> Crucible.getOverrideArgs - return $ + return ( precond , -- Can't use 'args' in this block, see warning on -- 'Crucible.nondetBranches'. From dfec9e8e6050ae511c818a3016ce16f6a24ef0ae Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Jul 2022 14:25:17 -0400 Subject: [PATCH 39/40] uc-crux-llvm: More refactoring in applySpec --- uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs index 64e83976c..fd1cc9897 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Specs/Apply.hs @@ -212,6 +212,18 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = splitRegs sz sz' (Crucible.RegMap m) = (Crucible.RegMap (Ctx.take sz sz' m), Crucible.RegMap (Ctx.drop sz sz' m)) + withSplitOverrideArgs :: + Ctx.Size old_args -> + Ctx.Size new_args -> + (forall args'. + Crucible.RegMap sym old_args -> + Crucible.RegMap sym new_args -> + Crucible.OverrideSim p sym ext rtp args' res a) -> + Crucible.OverrideSim p sym ext rtp (old_args Ctx.<+> new_args) res a + withSplitOverrideArgs oldSz newSz k = + do (args_, new_args) <- splitRegs oldSz newSz <$> Crucible.getOverrideArgs + k args_ new_args + -- Convert a Spec into a branch for 'nondetBranches' specToBranch sym mem argTys spec@(Spec.Spec specPre _ _ _) = do precond <- liftIO (matchPreconds modCtx sym mem argTys specPre args) @@ -221,9 +233,8 @@ applySpecs bak modCtx tracker funcSymb specs fsRep mvar args = ( precond , -- Can't use 'args' in this block, see warning on -- 'Crucible.nondetBranches'. - do ovArgs <- Crucible.getOverrideArgs - let (_, Crucible.RegMap safeArgs) = - splitRegs cargsSize argsSize ovArgs - applyPost bak modCtx tracker funcSymb fsRep mvar spec safeArgs + withSplitOverrideArgs cargsSize argsSize $ + \_ (Crucible.RegMap safeArgs) -> + applyPost bak modCtx tracker funcSymb fsRep mvar spec safeArgs , Nothing -- position ) From 979ddfb2b2f10ef310afe8d5f41af6e66044f494 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 26 Jul 2022 10:21:00 -0400 Subject: [PATCH 40/40] crucible: Clarify comment on nondetBranches --- crucible/src/Lang/Crucible/Simulator/OverrideSim.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs b/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs index 13a9dff89..7cbe9597d 100644 --- a/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs +++ b/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs @@ -565,8 +565,9 @@ symbolicBranches new_args xs0 = -- -- Unlike 'symbolicBranches', this function does not take only the first branch -- with a predicate that evaluates to true; instead it takes /all/ branches with --- predicates that evaluate to true. Each branch will not assume that other --- branches weren't taken. +-- predicates that are not syntactically false (or cannot be proved unreachable +-- with path satisfiability checking, if enabled). Each branch will /not/ assume +-- that other branches weren't taken. -- -- As with 'symbolicBranch', any symbolic values needed by the branches should be -- placed into the @RegMap@ argument and retrieved when needed. See the comment