diff --git a/.gitmodules b/.gitmodules index 9ec4b341..30b639c2 100644 --- a/.gitmodules +++ b/.gitmodules @@ -7,3 +7,7 @@ [submodule "dependencies/blt"] path = dependencies/blt url = https://github.com/GaloisInc/blt +[submodule "dependencies/language-sally"] + path = dependencies/language-sally + url = https://github.com/GaloisInc/language-sally.git + diff --git a/cabal.project b/cabal.project index 066c504b..b6cf07d8 100644 --- a/cabal.project +++ b/cabal.project @@ -8,8 +8,10 @@ packages: what4/ what4-abc/ what4-blt/ + what4-transition-system/ optional-packages: dependencies/abcBridge/ dependencies/aig/ dependencies/blt/ + dependencies/language-sally/ diff --git a/dependencies/language-sally b/dependencies/language-sally new file mode 160000 index 00000000..2ed17f2e --- /dev/null +++ b/dependencies/language-sally @@ -0,0 +1 @@ +Subproject commit 2ed17f2e5522bf3b2abcca79ce00b6e4567a681d diff --git a/what4-transition-system/LICENSE b/what4-transition-system/LICENSE new file mode 100644 index 00000000..613daeef --- /dev/null +++ b/what4-transition-system/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2020 Galois Inc. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in + the documentation and/or other materials provided with the + distribution. + + * Neither the name of Galois, Inc. nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/what4-transition-system/src/What4/TransitionSystem.hs b/what4-transition-system/src/What4/TransitionSystem.hs new file mode 100644 index 00000000..11d2ce21 --- /dev/null +++ b/what4-transition-system/src/What4/TransitionSystem.hs @@ -0,0 +1,174 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +-- | +-- Module : What4.TransitionSystem +-- Description : Definition of a transition system made of What4 expressions +-- Copyright : (c) Galois Inc, 2020-2021 +-- License : BSD3 +-- Maintainer : val@galois.com +-- | +module What4.TransitionSystem + ( CtxState, + TransitionSystem (..), + createStateStruct, + makeInitialState, + makeQueries, + makeTransitions, + userSymbol', + ) +where + +import qualified Control.Lens as L +import Control.Monad.Identity (forM) +import Data.Functor.Const (Const (..)) +import qualified Data.Parameterized.Context as Ctx +import qualified What4.BaseTypes as BaseTypes +import What4.Expr (ExprBuilder) +import qualified What4.Interface as What4 +import Prelude hiding (init) + +-- | Convenient wrapper around @What4.userSymbol@ for when we're willing to fail +-- on error. +userSymbol' :: String -> What4.SolverSymbol +userSymbol' s = case What4.userSymbol s of + Left e -> error $ show e + Right symbol -> symbol + +-- | @TransitionSystem@ can be used to describe a transition system, which can +-- then be elaborated into a set of SMT formulas. +data TransitionSystem sym state = TransitionSystem + { -- | Representations for the fields of the state type, can be computed + -- automatically using @knownRepr@ for a concrete type parameter @state@. + stateReprs :: Ctx.Assignment BaseTypes.BaseTypeRepr state, + -- | Names of the field accessor for each state field. + stateNames :: Ctx.Assignment (Const What4.SolverSymbol) state, + -- | Initial state predicate. + initialStatePredicate :: + What4.SymStruct sym state -> + IO (What4.Pred sym), + -- | Binary relations over states for the transition, parameterized by the + -- current state and the next state. Should return a name for each + -- transition, and their boolean formula. + stateTransitions :: + What4.SymStruct sym state -> + What4.SymStruct sym state -> + IO [(What4.SolverSymbol, What4.Pred sym)], + -- | Queries that must hold at all states. + queries :: + What4.SymStruct sym state -> + IO [What4.Pred sym] + } + +createStateStruct :: + What4.IsSymExprBuilder sym => + sym -> + -- | Namespace of the state structure. + String -> + Ctx.Assignment BaseTypes.BaseTypeRepr state -> + IO (What4.SymStruct sym state) +createStateStruct sym namespace stateType = + What4.freshConstant sym (userSymbol' namespace) (What4.BaseStructRepr stateType) + +-- Actually I think it'll be better to have a fresh struct rather than having fields +-- What4.mkStruct sym =<< freshStateVars sym namespace stateType + +-- | A context with just one field, a struct type for the state. +type CtxState state = Ctx.EmptyCtx Ctx.::> BaseTypes.BaseStructType state + +-- | Computes a set of side conditions we must add to state formulas to account +-- for the mismatch between What4 types and sally types. For instance, a What4 +-- @Nat@ must be translated as a Sally @Int@ (since Sally does not have natural +-- numbers), with a side condition of positivity. +sideConditions :: + forall sym t st fs state. + sym ~ ExprBuilder t st fs => + sym -> + -- | state type + Ctx.Assignment BaseTypes.BaseTypeRepr state -> + -- | state on which to operate + What4.SymStruct sym state -> + IO (What4.Pred sym) +sideConditions sym stateReprs _state = + do + preds <- Ctx.traverseAndCollect sideConditionsForIndex stateReprs + What4.andAllOf sym L.folded preds + where + sideConditionsForIndex :: + Ctx.Index state tp -> + BaseTypes.BaseTypeRepr tp -> + IO [What4.Pred sym] + sideConditionsForIndex _ BaseTypes.BaseBoolRepr = return [] + sideConditionsForIndex _ BaseTypes.BaseIntegerRepr = return [] + sideConditionsForIndex _ BaseTypes.BaseRealRepr = return [] + sideConditionsForIndex _ (BaseTypes.BaseBVRepr _) = return [] + sideConditionsForIndex _ bt = + error $ "sideConditions: Not implemented for base type " ++ show bt ++ ". Please report." + +makeInitialState :: + sym ~ ExprBuilder t st fs => + sym -> + TransitionSystem sym state -> + IO (What4.Pred sym) +makeInitialState sym (TransitionSystem {initialStatePredicate, stateReprs}) = + do + init <- createStateStruct sym "init" stateReprs + initP <- initialStatePredicate init + sideP <- sideConditions sym stateReprs init + What4.andPred sym initP sideP + +makeTransitions :: + sym ~ ExprBuilder t st fs => + sym -> + -- | Name to use for the "main" transition. + What4.SolverSymbol -> + -- | Exporter-specific transition builder of transition, receiving as input + -- the name of that transition and the transition predicate. + (What4.SolverSymbol -> What4.Pred sym -> transition) -> + TransitionSystem sym state -> + IO [transition] +makeTransitions + sym + mainTransitionName + makeTransition + (TransitionSystem {stateReprs, stateTransitions}) = + do + state <- createStateStruct sym "state" stateReprs + next <- createStateStruct sym "next" stateReprs + transitions <- stateTransitions state next + allTransitions <- forM transitions $ \(name, transitionP) -> + do + stateSideP <- sideConditions sym stateReprs state + nextSideP <- sideConditions sym stateReprs next + transitionRelation <- What4.andAllOf sym L.folded [transitionP, stateSideP, nextSideP] + return $ makeTransition name transitionRelation + -- the main transition is the conjunction of all transitions + -- FIXME: turn the name of the transition into an expression + transitionsPreds <- forM (fst <$> transitions) $ \transitionName -> + What4.freshConstant sym transitionName BaseTypes.BaseBoolRepr + transitionRelation <- What4.orOneOf sym L.folded transitionsPreds + let mainTransition = makeTransition mainTransitionName transitionRelation + -- A transition may only refer to previously-defined transitions, so + -- @mainTransition@ must be last. + return (allTransitions ++ [mainTransition]) + +makeQueries :: + sym ~ ExprBuilder t st fs => + sym -> + (What4.Pred sym -> query) -> + TransitionSystem sym state -> + IO [query] +makeQueries + sym + makeQuery + (TransitionSystem {queries, stateReprs}) = + do + -- NOTE: Event though some backend queries do not use a namespace, we need + -- to use a "query" namespace here, as it forces the What4 backend to + -- treat those fields as different from the "state"/"next" ones. + queryState <- createStateStruct sym "query" stateReprs + (makeQuery <$>) <$> queries queryState diff --git a/what4-transition-system/src/What4/TransitionSystem/Exporter/Sally.hs b/what4-transition-system/src/What4/TransitionSystem/Exporter/Sally.hs new file mode 100644 index 00000000..be36a683 --- /dev/null +++ b/what4-transition-system/src/What4/TransitionSystem/Exporter/Sally.hs @@ -0,0 +1,112 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} + +-- | +-- Module : What4.TransitionSystem.Exporter.Sally +-- Description : Export What4 transition system to the Sally format +-- Copyright : (c) Galois Inc, 2020-2021 +-- License : BSD3 +-- Maintainer : val@galois.com +module What4.TransitionSystem.Exporter.Sally + ( exportTransitionSystem, + mySallyNames, + ) +where + +import qualified Data.Parameterized.Context as Ctx +import qualified Language.Sally as S +import What4.Expr (ExprBuilder) +import qualified What4.Interface as What4 +import qualified What4.TransitionSystem as TS +import Prelude hiding (init) + +data SallyNames = SallyNames + { -- | Name of the initial state predicate + initialName :: S.Name, + -- | Name of the main transition + mainTransitionName :: S.Name, + -- | Name of the state type + stateName :: S.Name, + -- | Name of the transition system + systemName :: S.Name + } + +-- | @mySallyNames@ has some default names since we currently don't care too +-- much about changing them +mySallyNames :: SallyNames +mySallyNames = + SallyNames + { initialName = TS.userSymbol' "InitialState", + mainTransitionName = TS.userSymbol' "MainTransition", + stateName = TS.userSymbol' "State", + systemName = TS.userSymbol' "System" + } + +sallyState :: + SallyNames -> + TS.TransitionSystem sym stateType -> + S.SallyState stateType Ctx.EmptyCtx +sallyState + (SallyNames {stateName}) + (TS.TransitionSystem {TS.stateNames, TS.stateReprs}) = + S.SallyState + { S.sallyStateName = stateName, + S.sallyStateVars = stateReprs, + S.sallyStateVarsNames = stateNames, + S.sallyStateInputs = Ctx.Empty, + S.sallyStateInputsNames = Ctx.Empty + } + +sallyQuery :: S.Name -> What4.Pred (ExprBuilder t st fs) -> S.SallyQuery t +sallyQuery systemName sallyQueryPredicate = + S.SallyQuery + { S.sallyQuerySystemName = systemName, + -- sqLet = [], + S.sallyQueryPredicate, + S.sallyQueryComment = "" + } + +exportTransitionSystem :: + ExprBuilder t st fs -> + SallyNames -> + TS.TransitionSystem (ExprBuilder t st fs) stateType -> + IO (S.Sally t stateType Ctx.EmptyCtx Ctx.EmptyCtx) +exportTransitionSystem + sym + (sn@SallyNames {initialName, mainTransitionName, stateName, systemName}) + ts = + do + sallyStateFormulaPredicate <- TS.makeInitialState sym ts + sallyTransitions <- + TS.makeTransitions + sym + mainTransitionName + (S.SallyTransition stateName) + ts + sallyQueries <- TS.makeQueries sym (sallyQuery systemName) ts + let sallyInitialFormula = + S.SallyStateFormula + { S.sallyStateFormulaName = initialName, + S.sallyStateFormulaDomain = stateName, + S.sallyStateFormulaPredicate + } + let sallySystem = + S.SallySystem + { S.sallySystemName = systemName, + S.sallySystemStateName = stateName, + S.sallySystemInitialStateName = initialName, + S.sallySystemTransitionName = mainTransitionName + } + return $ + S.Sally + { S.sallyState = sallyState sn ts, + S.sallyFormulas = [], + S.sallyConstants = Ctx.Empty, + S.sallyInitialFormula, + S.sallyTransitions, + S.sallySystem, + S.sallyQueries + } diff --git a/what4-transition-system/test/Main.hs b/what4-transition-system/test/Main.hs new file mode 100644 index 00000000..ec084787 --- /dev/null +++ b/what4-transition-system/test/Main.hs @@ -0,0 +1,237 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | +-- Module : Main +-- Copyright : (c) Galois Inc, 2020-2021 +-- License : BSD3 +-- Maintainer : val@galois.com +-- | +module Main where + +import qualified Control.Lens as L +import Control.Monad (join) +import Data.Parameterized (knownRepr) +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Nonce (withIONonceGenerator) +import Language.Sally (Name, sexpOfSally, sexpToCompactDoc) +import qualified What4.BaseTypes as BaseTypes +import What4.Expr + ( ExprBuilder, + FloatModeRepr (FloatIEEERepr), + newExprBuilder, + ) +import What4.Expr.Builder (SymbolBinding (..)) +import qualified What4.Interface as What4 +import What4.TransitionSystem (TransitionSystem (..), userSymbol') +import qualified What4.TransitionSystem.Exporter.Sally as Sally +import Prelude hiding (init) + +showBinding :: SymbolBinding t -> String +showBinding (VarSymbolBinding x) = show x +showBinding (FnSymbolBinding x) = show x + +displayTransitionSystem :: + sym ~ ExprBuilder t st fs => + sym -> + TransitionSystem sym stateFields -> + IO () +displayTransitionSystem sym transitionSystem = + do + sts <- Sally.exportTransitionSystem sym Sally.mySallyNames transitionSystem + sexp <- sexpOfSally sym sts + print . sexpToCompactDoc $ sexp + +main :: IO () +main = + do + withIONonceGenerator $ \nonceGen -> do + sym <- newExprBuilder FloatIEEERepr State nonceGen + ts <- counterTransitionSystem sym + displayTransitionSystem sym ts + withIONonceGenerator $ \nonceGen -> do + sym <- newExprBuilder FloatIEEERepr State nonceGen + ts <- realsTransitionSystem sym + displayTransitionSystem sym ts + +-- We don't need any information in the state +data State t = State + +makeFieldNames :: + forall stateType. + [What4.SolverSymbol] -> + Ctx.Assignment BaseTypes.BaseTypeRepr stateType -> + Ctx.Assignment (L.Const What4.SolverSymbol) stateType +makeFieldNames fields rep = Ctx.generate (Ctx.size rep) generator + where + generator :: Ctx.Index stateType tp -> L.Const What4.SolverSymbol tp + generator index = L.Const (fields !! (Ctx.indexVal index)) + +-- +-- Example 1: a simple counter +-- +type CounterStateType = Ctx.EmptyCtx Ctx.::> BaseTypes.BaseBoolType Ctx.::> BaseTypes.BaseIntegerType + +counterStateFields :: [What4.SolverSymbol] +counterStateFields = userSymbol' <$> ["counterIsEven", "counter"] + +counterFieldNames :: Ctx.Assignment (L.Const What4.SolverSymbol) CounterStateType +counterFieldNames = makeFieldNames counterStateFields knownRepr + +counterIsEven :: Ctx.Index CounterStateType BaseTypes.BaseBoolType +counterIsEven = Ctx.natIndex @0 + +counter :: Ctx.Index CounterStateType BaseTypes.BaseIntegerType +counter = Ctx.natIndex @1 + +-- | Example initial state predicate, this one constrains the `bool` field to be +-- true, and the `nat` field to be equal to zero +counterInitial :: + What4.IsSymExprBuilder sym => + sym -> + -- | mapping to a variable for each state field + What4.SymStruct sym CounterStateType -> + IO (What4.Pred sym) +counterInitial sym init = + do + initCounterIsEven <- What4.structField sym init counterIsEven + initCounter <- What4.structField sym init counter + nZero <- What4.intLit sym 0 + natCond <- What4.intEq sym initCounter nZero + andCond <- What4.andPred sym initCounterIsEven natCond + return andCond + +-- | Example state transition, here, during a transition, the boolean gets +-- negated, and the natural number gets incremented. One property of such a +-- system would be that when the boolean is false, the number is even (assuming +-- a false and zero initial state). +counterTransitions :: + What4.IsSymExprBuilder sym => + sym -> + -- | current state + What4.SymStruct sym CounterStateType -> + -- | next state + What4.SymStruct sym CounterStateType -> + IO [(Name, What4.Pred sym)] +counterTransitions sym state next = + do + stateCounterIsEven <- What4.structField sym state counterIsEven + stateCounter <- What4.structField sym state counter + nextCounterIsEven <- What4.structField sym next counterIsEven + nextCounter <- What4.structField sym next counter + -- (= next.counter (+ 1 state.counter)) + nOne <- What4.intLit sym 1 + nStatePlusOne <- What4.intAdd sym nOne stateCounter + natCond <- What4.intEq sym nextCounter nStatePlusOne + -- (= next.counterIsEven (not state.counterIsEven)) + bStateNeg <- What4.notPred sym stateCounterIsEven + boolCond <- What4.eqPred sym nextCounterIsEven bStateNeg + andCond <- What4.andPred sym boolCond natCond + return [(userSymbol' "CounterTransition", andCond)] + +-- | TODO +counterTransitionSystem :: + ExprBuilder t st fs -> + IO (TransitionSystem (ExprBuilder t st fs) CounterStateType) +counterTransitionSystem sym = + do + return $ + TransitionSystem + { stateReprs = knownRepr, + stateNames = counterFieldNames, + initialStatePredicate = counterInitial sym, + stateTransitions = counterTransitions sym, + queries = const (pure []) + } + +-- +-- Example 2: using real numbers +-- + +-- based on sally/test/regress/bmc/nra/algebraic.mcmt + +type RealsStateType = + Ctx.EmptyCtx + Ctx.::> BaseTypes.BaseRealType + Ctx.::> BaseTypes.BaseRealType + Ctx.::> BaseTypes.BaseRealType + +realsStateFields :: [What4.SolverSymbol] +realsStateFields = userSymbol' <$> ["P", "x", "n"] + +realsFieldNames :: Ctx.Assignment (L.Const What4.SolverSymbol) RealsStateType +realsFieldNames = makeFieldNames realsStateFields knownRepr + +pReals :: Ctx.Index RealsStateType BaseTypes.BaseRealType +pReals = Ctx.natIndex @0 + +xReals :: Ctx.Index RealsStateType BaseTypes.BaseRealType +xReals = Ctx.natIndex @1 + +nReals :: Ctx.Index RealsStateType BaseTypes.BaseRealType +nReals = Ctx.natIndex @2 + +realsInitial :: + What4.IsSymExprBuilder sym => + sym -> + -- | mapping to a variable for each state field + What4.SymStruct sym RealsStateType -> + IO (What4.Pred sym) +realsInitial sym init = + do + pInit <- What4.structField sym init pReals + nInit <- What4.structField sym init nReals + -- (and (= P 1) (= n 0)) + join + ( What4.andPred sym + <$> (What4.realEq sym pInit =<< What4.realLit sym 1) + <*> (What4.realEq sym nInit =<< What4.realLit sym 0) + ) + +realsTransitions :: + What4.IsSymExprBuilder sym => + sym -> + -- | current state + What4.SymStruct sym RealsStateType -> + -- | next state + What4.SymStruct sym RealsStateType -> + IO [(Name, What4.Pred sym)] +realsTransitions sym state next = + do + pState <- What4.structField sym state pReals + xState <- What4.structField sym state xReals + nState <- What4.structField sym state nReals + pNext <- What4.structField sym next pReals + xNext <- What4.structField sym next xReals + nNext <- What4.structField sym next nReals + -- (= next.P (* state.P state.x) + c1 <- join $ What4.realEq sym pNext <$> What4.realMul sym pState xState + -- (= next.n (+ state.n 1)) + c2 <- join $ What4.realEq sym nNext <$> (What4.realAdd sym nState =<< What4.realLit sym 1) + -- (= next.x state.x) + c3 <- What4.realEq sym xNext xState + t <- What4.andPred sym c1 =<< What4.andPred sym c2 c3 + return [(userSymbol' "RealsTransition", t)] + +-- | TODO +realsTransitionSystem :: + ExprBuilder t st fs -> + IO (TransitionSystem (ExprBuilder t st fs) RealsStateType) +realsTransitionSystem sym = + do + return $ + TransitionSystem + { stateReprs = knownRepr, + stateNames = realsFieldNames, + initialStatePredicate = realsInitial sym, + stateTransitions = realsTransitions sym, + queries = const (pure []) + } diff --git a/what4-transition-system/what4-transition-system.cabal b/what4-transition-system/what4-transition-system.cabal new file mode 100644 index 00000000..29bb1847 --- /dev/null +++ b/what4-transition-system/what4-transition-system.cabal @@ -0,0 +1,52 @@ +cabal-version: 3.0 +name: what4-transition-system +version: 0.0.3.0 +synopsis: Generates transition systems from What4 descriptions +description: Generates transition systems from What4 descriptions +author: Valentin Robert +maintainer: Valentin Robert +copyright: Galois, Inc. 2020-2021 +license: BSD-3-Clause +license-file: LICENSE +build-type: Simple + +common dependencies + build-depends: + , ansi-wl-pprint ^>=0.6 + , base >=4.12 && <4.15 + , bytestring + , containers ^>=0.6 + , io-streams + , language-sally ^>=0.3 + , lens + , mtl + , parameterized-utils >=2.0 && <2.2 + , text + , what4 ^>=1.1 + +library + import: dependencies + exposed-modules: + What4.TransitionSystem + What4.TransitionSystem.Exporter.Sally + + other-modules: Paths_what4_transition_system + hs-source-dirs: src + ghc-options: + -Wall -Werror=incomplete-patterns -Werror=missing-methods + -Werror=overlapping-patterns + + default-language: Haskell2010 + +test-suite what4-transition-system-tests + import: dependencies + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: Paths_what4_transition_system + hs-source-dirs: test + ghc-options: + -Wall -Werror=incomplete-patterns -Werror=missing-methods + -Werror=overlapping-patterns + + build-depends: what4-transition-system + default-language: Haskell2010