copilot-theorem 3.20 → 4.0
raw patch · 4 files changed
+199/−10 lines, 4 filesdep ~copilot-coredep ~copilot-prettyprinterPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: copilot-core, copilot-prettyprinter
API changes (from Hackage documentation)
Files
- CHANGELOG +5/−0
- copilot-theorem.cabal +3/−3
- src/Copilot/Theorem/What4/Translate.hs +132/−3
- tests/Test/Copilot/Theorem/What4.hs +59/−4
CHANGELOG view
@@ -1,3 +1,8 @@+2024-09-07+ * Version bump (4.0). (#532)+ * Add support for struct updates in Copilot.Theorem.What4. (#524)+ * Add support for array updates in Copilot.Theorem.What4. (#36)+ 2024-07-07 * Version bump (3.20). (#522) * What4 upper-bound dependency version bump. (#514)
copilot-theorem.cabal view
@@ -14,7 +14,7 @@ <https://copilot-language.github.io>. -version : 3.20+version : 4.0 license : BSD3 license-file : LICENSE maintainer : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -63,8 +63,8 @@ , xml >= 1.3 && < 1.4 , what4 >= 1.3 && < 1.7 - , copilot-core >= 3.20 && < 3.21- , copilot-prettyprinter >= 3.20 && < 3.21+ , copilot-core >= 4.0 && < 4.1+ , copilot-prettyprinter >= 4.0 && < 4.1 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove
src/Copilot/Theorem/What4/Translate.hs view
@@ -52,16 +52,18 @@ import Data.Parameterized.Classes (KnownRepr (..)) import Data.Parameterized.Context (EmptyCtx, type (::>)) import Data.Parameterized.NatRepr (LeqProof (..), NatCases (..),- NatRepr, decNat, isZeroOrGT1,+ NatRepr, decNat, incNat,+ intValue, isZeroOrGT1, knownNat, minusPlusCancel,- mkNatRepr, testNatCases)+ mkNatRepr, testNatCases,+ testStrictLeq) import Data.Parameterized.Some (Some (..)) import Data.Parameterized.SymbolRepr (SymbolRepr, knownSymbol) import qualified Data.Parameterized.Vector as V import Data.Type.Equality (TestEquality (..), (:~:) (..)) import Data.Word (Word32) import GHC.TypeLits (KnownSymbol)-import GHC.TypeNats (KnownNat, type (<=))+import GHC.TypeNats (KnownNat, type (<=), type (+)) import qualified Panic as Panic import qualified What4.BaseTypes as WT@@ -799,6 +801,8 @@ (CE.BwShiftL _ _, xe1, xe2) -> translateBwShiftL xe1 xe2 (CE.BwShiftR _ _, xe1, xe2) -> translateBwShiftR xe1 xe2 (CE.Index _, xe1, xe2) -> translateIndex xe1 xe2+ (CE.UpdateField atp _ftp extractor, structXe, fieldXe) ->+ translateUpdateField atp extractor structXe fieldXe where -- Translate an 'CE.Add' operation and its arguments into a what4 -- representation of the appropriate type.@@ -964,6 +968,55 @@ liftIO $ buildIndexExpr sym ix xes _ -> unexpectedValues "index operation" + -- Translate an 'CE.UpdateField' operation and its arguments into a what4+ -- representation. This function will panic if one of the following does not+ -- hold:+ --+ -- - The argument is not a struct.+ --+ -- - The struct's field cannot be found.+ translateUpdateField :: forall struct s.+ KnownSymbol s+ => CT.Type struct+ -- ^ The type of the struct argument+ -> (struct -> CT.Field s b)+ -- ^ Extract a struct field+ -> XExpr sym+ -- ^ The first argument value (should be a struct)+ -> XExpr sym+ -- ^ The second argument value (should be the same type+ -- as the struct field)+ -> TransM sym (XExpr sym)+ -- ^ The first argument value, but with an updated+ -- value for the supplied field.+ translateUpdateField structTp extractor structXe newFieldXe =+ case (structTp, structXe) of+ (CT.Struct s, XStruct structFieldXes) ->+ case mIx s of+ Just ix -> return $ XStruct $ updateAt ix newFieldXe structFieldXes+ Nothing ->+ panic [ "Could not find field " ++ show fieldNameRepr+ , show s+ ]+ _ -> unexpectedValues "update-field operation"+ where+ -- Update an element of a list at a particular index. This assumes the+ -- preconditions that the index is a non-negative number that is less+ -- than the length of the list.+ updateAt :: forall a. Int -> a -> [a] -> [a]+ updateAt _ _ [] = []+ updateAt 0 new (_:xs) = new : xs+ updateAt n new (x:xs) = x : updateAt (n-1) new xs++ fieldNameRepr :: SymbolRepr s+ fieldNameRepr = fieldName (extractor undefined)++ structFieldNameReprs :: CT.Struct struct => struct -> [Some SymbolRepr]+ structFieldNameReprs s = valueName <$> CT.toValues s++ mIx :: CT.Struct struct => struct -> Maybe Int+ mIx s = elemIndex (Some fieldNameRepr) (structFieldNameReprs s)+ -- Check the types of the arguments. If the arguments are bitvector values, -- apply the 'BVOp2'. If the arguments are floating-point values, apply the -- 'FPOp2'. Otherwise, 'panic'.@@ -1090,7 +1143,37 @@ translateOp3 sym origExpr op xe1 xe2 xe3 = case (op, xe1, xe2, xe3) of (CE.Mux _, XBool te, xe1, xe2) -> liftIO $ mkIte sym te xe1 xe2 (CE.Mux _, _, _, _) -> unexpectedValues "mux operation"+ (CE.UpdateArray _, xe1, xe2, xe3) -> translateUpdateArray xe1 xe2 xe3 where+ -- Translate an 'CE.UpdateArray' operation and its arguments into a what4+ -- representation. This checks that the first argument is an 'XArray' and+ -- the second argument is an 'XWord32', invoking 'panic' is this invariant+ -- is not upheld.+ --+ -- Note: Currently, copilot only checks if array indices are out of bounds+ -- as a side condition. The method of translation we are using simply+ -- creates a nest of if-then-else expression to check the index expression+ -- against all possible indices. If the index expression is known by the+ -- solver to be out of bounds (for instance, if it is a constant 5 for an+ -- array of 5 elements), then the if-then-else will trivially resolve to+ -- true.+ translateUpdateArray :: XExpr sym+ -> XExpr sym+ -> XExpr sym+ -> TransM sym (XExpr sym)+ translateUpdateArray xe1 xe2 newXe = case (xe1, xe2) of+ (XArray xes, XWord32 ix) -> do+ -- The second argument should not be out of bounds (i.e., greater than+ -- or equal to the length of the array)+ xesLenBV <- liftIO $ WI.bvLit sym knownNat $ BV.mkBV knownNat+ $ toInteger $ V.lengthInt xes+ inRange <- liftIO $ WI.bvUlt sym ix xesLenBV+ addSidePred inRange++ xes' <- liftIO $ buildUpdateArrayExpr sym xes ix newXe+ pure $ XArray xes'+ _ -> unexpectedValues "update array operation"+ unexpectedValues :: forall m x . (Panic.HasCallStack, MonadIO m) => String -> m x unexpectedValues op =@@ -1128,6 +1211,52 @@ curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx) ixEq <- WI.bvEq sym curIxExpr ix mkIte sym ixEq xe rstExpr++-- | Construct an expression that updates an array element at a particular index+-- by building a chain of @if@ expressions, where each expression checks if the+-- current index is equal to a given index in the array. If the indices are+-- equal, return the array with the element at that index updated. Otherwise,+-- proceed to the next @if@ expression, which checks the next index in the+-- array.+buildUpdateArrayExpr :: forall sym n.+ (1 <= n, WFP.IsInterpretedFloatExprBuilder sym)+ => sym+ -> V.Vector n (XExpr sym)+ -- ^ Elements+ -> WI.SymBV sym 32+ -- ^ Index+ -> XExpr sym+ -- ^ New element+ -> IO (V.Vector n (XExpr sym))+buildUpdateArrayExpr sym xelts ix newXe = loop (knownNat @0)+ where+ n :: NatRepr n+ n = V.length xelts++ n32 :: NatRepr 32+ n32 = knownNat @32++ loop :: forall i.+ ((i + 1) <= n)+ => NatRepr i+ -> IO (V.Vector n (XExpr sym))+ loop curIx =+ case testStrictLeq nextIx n of+ -- Recursive case+ Left LeqProof -> do+ rstExpr <- loop nextIx+ curIxExpr <- WI.bvLit sym n32 $ BV.mkBV n32 $ intValue curIx+ ixEq <- WI.bvEq sym curIxExpr ix+ V.zipWithM (mkIte sym ixEq) newXelts rstExpr+ -- Base case, we are at the last possible index (n - 1)+ Right Refl ->+ pure newXelts+ where+ nextIx :: NatRepr (i + 1)+ nextIx = incNat curIx++ newXelts :: V.Vector n (XExpr sym)+ newXelts = V.insertAt curIx newXe xelts -- | Construct an @if@ expression of the appropriate type. mkIte :: WFP.IsInterpretedFloatExprBuilder sym
tests/Test/Copilot/Theorem/What4.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE DataKinds #-} -- The following warning is disabled due to a necessary instance of SatResult -- defined in this module. {-# OPTIONS_GHC -fno-warn-orphans #-}@@ -6,17 +7,22 @@ -- External imports import Data.Int (Int8)+import Data.Word (Word32) import Test.Framework (Test, testGroup) import Test.Framework.Providers.QuickCheck2 (testProperty)-import Test.QuickCheck (Property, arbitrary, forAll)+import Test.QuickCheck (Arbitrary (arbitrary), Property,+ arbitrary, forAll) import Test.QuickCheck.Monadic (monadicIO, run) -- External imports: Copilot-import Copilot.Core.Expr (Expr (Const, Op2))-import Copilot.Core.Operators (Op2 (..))+import Copilot.Core.Expr (Expr (Const, Op1, Op2))+import Copilot.Core.Operators (Op1 (..), Op2 (..)) import Copilot.Core.Spec (Spec (..)) import qualified Copilot.Core.Spec as Copilot-import Copilot.Core.Type (Typed (typeOf))+import Copilot.Core.Type (Field (..),+ Struct (toValues, typeName),+ Type (Struct), Typed (typeOf),+ Value (..)) -- Internal imports: Modules being tested import Copilot.Theorem.What4 (SatResult (..), Solver (..), prove)@@ -30,6 +36,7 @@ [ testProperty "Prove via Z3 that true is valid" testProveZ3True , testProperty "Prove via Z3 that false is invalid" testProveZ3False , testProperty "Prove via Z3 that x == x is valid" testProveZ3EqConst+ , testProperty "Prove via Z3 that a struct update is valid" testProveZ3StructUpdate ] -- * Individual tests@@ -76,6 +83,54 @@ spec :: Int8 -> Spec spec x = propSpec propName $ Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)++-- | Test that Z3 is able to prove the following expresion valid:+-- @+-- for all (s :: MyStruct),+-- ((s ## testField =$ (+1)) # testField) == ((s # testField) + 1)+-- @+testProveZ3StructUpdate :: Property+testProveZ3StructUpdate = forAll arbitrary $ \x ->+ monadicIO $ run $ checkResult Z3 propName (spec x) Valid+ where+ propName :: String+ propName = "prop"++ spec :: TestStruct -> Spec+ spec s = propSpec propName $+ Op2+ (Eq typeOf)+ (getField+ (Op2+ (UpdateField typeOf typeOf testField)+ sExpr+ (add1 (getField sExpr))))+ (add1 (getField sExpr))+ where+ sExpr :: Expr TestStruct+ sExpr = Const typeOf s++ getField :: Expr TestStruct -> Expr Word32+ getField = Op1 (GetField typeOf typeOf testField)++ add1 :: Expr Word32 -> Expr Word32+ add1 x = Op2 (Add typeOf) x (Const typeOf 1)++-- | A simple data type with a 'Struct' instance and a 'Field'. This is only+-- used as part of 'testProveZ3StructUpdate'.+newtype TestStruct = TestStruct { testField :: Field "testField" Word32 }++instance Arbitrary TestStruct where+ arbitrary = do+ w32 <- arbitrary+ return (TestStruct (Field w32))++instance Struct TestStruct where+ typeName _ = "testStruct"+ toValues s = [Value typeOf (testField s)]++instance Typed TestStruct where+ typeOf = Struct (TestStruct (Field 0)) -- | Check that the solver's satisfiability result for the given property in -- the given spec matches the expectation.