mirror of
https://github.com/GaloisInc/what4.git
synced 2024-09-11 04:05:38 +03:00
Update to changes in language-sally.
This commit is contained in:
parent
95a514fba2
commit
f74d8eaa4e
3
.gitmodules
vendored
3
.gitmodules
vendored
@ -7,9 +7,6 @@
|
||||
[submodule "dependencies/blt"]
|
||||
path = dependencies/blt
|
||||
url = https://github.com/GaloisInc/blt
|
||||
[submodule "dependencies/parameterized-utils"]
|
||||
path = dependencies/parameterized-utils
|
||||
url = https://github.com/GaloisInc/parameterized-utils
|
||||
[submodule "dependencies/language-sally"]
|
||||
path = dependencies/language-sally
|
||||
url = https://github.com/GaloisInc/language-sally.git
|
||||
|
2
dependencies/language-sally
vendored
2
dependencies/language-sally
vendored
@ -1 +1 @@
|
||||
Subproject commit a52404a9d3f2ff88809f0ad2832ffa518b7ac89b
|
||||
Subproject commit 2ed17f2e5522bf3b2abcca79ce00b6e4567a681d
|
@ -1,195 +1,141 @@
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE NamedFieldPuns #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
|
||||
-- | TODO
|
||||
-- |
|
||||
-- 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,
|
||||
mySallyNames,
|
||||
-- stateField,
|
||||
transitionSystemToSally,
|
||||
makeInitialState,
|
||||
makeQueries,
|
||||
makeTransitions,
|
||||
userSymbol',
|
||||
)
|
||||
where
|
||||
|
||||
import qualified Control.Lens as L
|
||||
import Control.Monad.Identity
|
||||
import Control.Monad.Identity (forM)
|
||||
import Data.Functor.Const (Const (..))
|
||||
import qualified Data.Parameterized.Context as Ctx
|
||||
import qualified Language.Sally as S
|
||||
import What4.BaseTypes
|
||||
import What4.Expr
|
||||
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. We try to have this type
|
||||
-- **not** depend on Sally.
|
||||
-- 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 value of @state@
|
||||
stateReprs :: Ctx.Assignment BaseTypeRepr state,
|
||||
-- | names of the field accessor for each state field
|
||||
{ -- | 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
|
||||
-- | 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. Returns a name for each
|
||||
-- | 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.
|
||||
-- NOTE: it is now important that each transition receives its own,
|
||||
-- fresh copy of the state structs, so that What4 knows not to try and
|
||||
-- share them, and to declare them in each Sally transition.
|
||||
stateTransitions ::
|
||||
What4.SymStruct sym state ->
|
||||
What4.SymStruct sym state ->
|
||||
IO [(S.Name, What4.Pred sym)],
|
||||
-- | Sally queries that must hold at all states
|
||||
--
|
||||
-- It may seem surprising that it receives a state, since Sally queries are
|
||||
-- not namespaced. The issue is, if we don't namespace the fields
|
||||
-- corresponding to the arguments of the block that the query refers to,
|
||||
-- they will be anonymized by the SMTWriter.
|
||||
--
|
||||
-- By creating the "query" state struct, the fields will be namespaced as
|
||||
-- "query.field". We can detect those fields in the writer (just as we do
|
||||
-- for the "init" namespace, that must exist for What4 but must be erased
|
||||
-- for Sally), and remove the field access as we print.
|
||||
IO [(What4.SolverSymbol, What4.Pred sym)],
|
||||
-- | Queries that must hold at all states.
|
||||
queries ::
|
||||
What4.SymStruct sym state ->
|
||||
IO [What4.Pred sym]
|
||||
}
|
||||
|
||||
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
|
||||
}
|
||||
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)
|
||||
|
||||
-- | @mySallyNames@ has some default names since we currently don't care too
|
||||
-- much about changing them
|
||||
mySallyNames :: SallyNames
|
||||
mySallyNames =
|
||||
SallyNames
|
||||
{ initialName = userSymbol' "InitialState",
|
||||
mainTransitionName = userSymbol' "MainTransition",
|
||||
stateName = userSymbol' "State",
|
||||
systemName = userSymbol' "System"
|
||||
}
|
||||
-- Actually I think it'll be better to have a fresh struct rather than having fields
|
||||
-- What4.mkStruct sym =<< freshStateVars sym namespace stateType
|
||||
|
||||
sallyState ::
|
||||
SallyNames ->
|
||||
TransitionSystem sym stateType ->
|
||||
S.SallyState stateType Ctx.EmptyCtx
|
||||
sallyState
|
||||
SallyNames
|
||||
{ stateName
|
||||
}
|
||||
TransitionSystem
|
||||
{ stateNames,
|
||||
stateReprs
|
||||
} =
|
||||
S.SallyState
|
||||
{ S.sallyStateName = stateName,
|
||||
S.sallyStateVars = stateReprs,
|
||||
S.sallyStateVarsNames = stateNames,
|
||||
S.sallyStateInputs = Ctx.Empty,
|
||||
S.sallyStateInputsNames = Ctx.Empty
|
||||
}
|
||||
-- | 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 t st fs state.
|
||||
ExprBuilder t st fs ->
|
||||
forall sym t st fs state.
|
||||
sym ~ ExprBuilder t st fs =>
|
||||
sym ->
|
||||
-- | state type
|
||||
Ctx.Assignment BaseTypeRepr state ->
|
||||
Ctx.Assignment BaseTypes.BaseTypeRepr state ->
|
||||
-- | state on which to operate
|
||||
What4.SymStruct (ExprBuilder t st fs) state ->
|
||||
IO (S.SallyPred t)
|
||||
sideConditions sym stateReprs state =
|
||||
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 -> BaseTypeRepr tp -> IO [S.SallyPred t]
|
||||
sideConditionsForIndex _ BaseBoolRepr = return []
|
||||
sideConditionsForIndex _ BaseIntegerRepr = return []
|
||||
sideConditionsForIndex _ BaseRealRepr = return []
|
||||
sideConditionsForIndex _ (BaseBVRepr _) = return []
|
||||
sideConditionsForIndex _ bt = error $ "sideConditions: Not implemented for base type " ++ show bt ++ ". Please report."
|
||||
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."
|
||||
|
||||
createStateStruct ::
|
||||
What4.IsSymExprBuilder sym =>
|
||||
makeInitialState ::
|
||||
sym ~ ExprBuilder t st fs =>
|
||||
sym ->
|
||||
String ->
|
||||
Ctx.Assignment BaseTypeRepr state ->
|
||||
IO (What4.SymStruct sym state)
|
||||
createStateStruct sym namespace stateType =
|
||||
What4.freshConstant sym (userSymbol' namespace) (What4.BaseStructRepr stateType)
|
||||
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
|
||||
|
||||
-- actually I think it'll be better to have a fresh struct rather than having fields
|
||||
-- What4.mkStruct sym =<< freshStateVars sym namespace stateType
|
||||
|
||||
sallyInitialState ::
|
||||
ExprBuilder t st fs ->
|
||||
TransitionSystem (ExprBuilder t st fs) state ->
|
||||
IO (S.SallyPred t)
|
||||
sallyInitialState
|
||||
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
|
||||
TransitionSystem
|
||||
{ initialStatePredicate,
|
||||
stateReprs
|
||||
} =
|
||||
do
|
||||
init <- createStateStruct sym "init" stateReprs
|
||||
initP <- initialStatePredicate init
|
||||
sideP <- sideConditions sym stateReprs init
|
||||
What4.andPred sym initP sideP
|
||||
|
||||
makeSallyTransitions ::
|
||||
ExprBuilder t st fs ->
|
||||
SallyNames ->
|
||||
TransitionSystem (ExprBuilder t st fs) state ->
|
||||
IO [S.SallyTransition t]
|
||||
makeSallyTransitions
|
||||
sym
|
||||
( SallyNames
|
||||
{ mainTransitionName,
|
||||
stateName
|
||||
}
|
||||
)
|
||||
( TransitionSystem
|
||||
{ stateReprs,
|
||||
stateTransitions
|
||||
}
|
||||
) =
|
||||
mainTransitionName
|
||||
makeTransition
|
||||
(TransitionSystem {stateReprs, stateTransitions}) =
|
||||
do
|
||||
state <- createStateStruct sym "state" stateReprs
|
||||
next <- createStateStruct sym "next" stateReprs
|
||||
@ -199,92 +145,30 @@ makeSallyTransitions
|
||||
stateSideP <- sideConditions sym stateReprs state
|
||||
nextSideP <- sideConditions sym stateReprs next
|
||||
transitionRelation <- What4.andAllOf sym L.folded [transitionP, stateSideP, nextSideP]
|
||||
return $
|
||||
S.SallyTransition
|
||||
{ S.transitionName = name,
|
||||
S.transitionDomain = stateName,
|
||||
-- traLet = [],
|
||||
S.transitionRelation
|
||||
}
|
||||
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 (S.transitionName <$> allTransitions) $ \transitionName ->
|
||||
What4.freshConstant sym transitionName BaseBoolRepr
|
||||
transitionsPreds <- forM (fst <$> transitions) $ \transitionName ->
|
||||
What4.freshConstant sym transitionName BaseTypes.BaseBoolRepr
|
||||
transitionRelation <- What4.orOneOf sym L.folded transitionsPreds
|
||||
let mainTransition =
|
||||
S.SallyTransition
|
||||
{ S.transitionName = mainTransitionName,
|
||||
S.transitionDomain = stateName,
|
||||
-- traLet = [],
|
||||
S.transitionRelation
|
||||
}
|
||||
-- a transition may only refer to previously-defined transitions, so
|
||||
-- @mainTransition@ must be last
|
||||
let mainTransition = makeTransition mainTransitionName transitionRelation
|
||||
-- A transition may only refer to previously-defined transitions, so
|
||||
-- @mainTransition@ must be last.
|
||||
return (allTransitions ++ [mainTransition])
|
||||
|
||||
makeSallyQueries ::
|
||||
makeQueries ::
|
||||
sym ~ ExprBuilder t st fs =>
|
||||
sym ->
|
||||
SallyNames ->
|
||||
(What4.Pred sym -> query) ->
|
||||
TransitionSystem sym state ->
|
||||
IO [S.SallyQuery t]
|
||||
makeSallyQueries sym
|
||||
SallyNames {systemName }
|
||||
TransitionSystem { queries, stateReprs }
|
||||
= do
|
||||
queryState <- createStateStruct sym "query" stateReprs
|
||||
map (sallyQuery systemName) <$> queries queryState
|
||||
|
||||
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 = ""
|
||||
}
|
||||
|
||||
transitionSystemToSally ::
|
||||
ExprBuilder t st fs ->
|
||||
SallyNames ->
|
||||
TransitionSystem (ExprBuilder t st fs) stateType ->
|
||||
IO (S.Sally t stateType Ctx.EmptyCtx Ctx.EmptyCtx)
|
||||
transitionSystemToSally
|
||||
IO [query]
|
||||
makeQueries
|
||||
sym
|
||||
sn@SallyNames
|
||||
{ initialName,
|
||||
mainTransitionName,
|
||||
stateName,
|
||||
systemName
|
||||
}
|
||||
ts =
|
||||
makeQuery
|
||||
(TransitionSystem {queries, stateReprs}) =
|
||||
do
|
||||
sallyStateFormulaPredicate <- sallyInitialState sym ts
|
||||
sallyTransitions <- makeSallyTransitions sym sn ts
|
||||
sallyQueries <- makeSallyQueries sym sn 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
|
||||
}
|
||||
|
||||
-- | A context with just one field, a struct type for the state
|
||||
type CtxState state = Ctx.EmptyCtx Ctx.::> BaseStructType state
|
||||
-- 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
|
||||
|
@ -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
|
||||
}
|
@ -10,23 +10,29 @@
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
-- |
|
||||
-- Module : TransitionSystemTest
|
||||
-- Copyright : (c) Galois Inc, 2020
|
||||
-- Module : Main
|
||||
-- Copyright : (c) Galois Inc, 2020-2021
|
||||
-- License : BSD3
|
||||
-- Maintainer : valentin.robert.42@gmail.com
|
||||
-- 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
|
||||
import Language.Sally
|
||||
import What4.BaseTypes
|
||||
import Data.Parameterized.Nonce (withIONonceGenerator)
|
||||
import Language.Sally (Name, sexpOfSally, sexpToCompactDoc)
|
||||
import qualified What4.BaseTypes as BaseTypes
|
||||
import What4.Expr
|
||||
import What4.Expr.Builder
|
||||
( ExprBuilder,
|
||||
FloatModeRepr (FloatIEEERepr),
|
||||
newExprBuilder,
|
||||
)
|
||||
import What4.Expr.Builder (SymbolBinding (..))
|
||||
import qualified What4.Interface as What4
|
||||
import What4.TransitionSystem
|
||||
import What4.TransitionSystem (TransitionSystem (..), userSymbol')
|
||||
import qualified What4.TransitionSystem.Exporter.Sally as Sally
|
||||
import Prelude hiding (init)
|
||||
|
||||
showBinding :: SymbolBinding t -> String
|
||||
@ -40,7 +46,7 @@ displayTransitionSystem ::
|
||||
IO ()
|
||||
displayTransitionSystem sym transitionSystem =
|
||||
do
|
||||
sts <- transitionSystemToSally sym mySallyNames transitionSystem
|
||||
sts <- Sally.exportTransitionSystem sym Sally.mySallyNames transitionSystem
|
||||
sexp <- sexpOfSally sym sts
|
||||
print . sexpToCompactDoc $ sexp
|
||||
|
||||
@ -62,7 +68,7 @@ data State t = State
|
||||
makeFieldNames ::
|
||||
forall stateType.
|
||||
[What4.SolverSymbol] ->
|
||||
Ctx.Assignment BaseTypeRepr stateType ->
|
||||
Ctx.Assignment BaseTypes.BaseTypeRepr stateType ->
|
||||
Ctx.Assignment (L.Const What4.SolverSymbol) stateType
|
||||
makeFieldNames fields rep = Ctx.generate (Ctx.size rep) generator
|
||||
where
|
||||
@ -72,7 +78,7 @@ makeFieldNames fields rep = Ctx.generate (Ctx.size rep) generator
|
||||
--
|
||||
-- Example 1: a simple counter
|
||||
--
|
||||
type CounterStateType = Ctx.EmptyCtx Ctx.::> BaseBoolType Ctx.::> BaseNatType
|
||||
type CounterStateType = Ctx.EmptyCtx Ctx.::> BaseTypes.BaseBoolType Ctx.::> BaseTypes.BaseIntegerType
|
||||
|
||||
counterStateFields :: [What4.SolverSymbol]
|
||||
counterStateFields = userSymbol' <$> ["counterIsEven", "counter"]
|
||||
@ -80,10 +86,10 @@ counterStateFields = userSymbol' <$> ["counterIsEven", "counter"]
|
||||
counterFieldNames :: Ctx.Assignment (L.Const What4.SolverSymbol) CounterStateType
|
||||
counterFieldNames = makeFieldNames counterStateFields knownRepr
|
||||
|
||||
counterIsEven :: Ctx.Index CounterStateType BaseBoolType
|
||||
counterIsEven :: Ctx.Index CounterStateType BaseTypes.BaseBoolType
|
||||
counterIsEven = Ctx.natIndex @0
|
||||
|
||||
counter :: Ctx.Index CounterStateType BaseNatType
|
||||
counter :: Ctx.Index CounterStateType BaseTypes.BaseIntegerType
|
||||
counter = Ctx.natIndex @1
|
||||
|
||||
-- | Example initial state predicate, this one constrains the `bool` field to be
|
||||
@ -98,8 +104,8 @@ counterInitial sym init =
|
||||
do
|
||||
initCounterIsEven <- What4.structField sym init counterIsEven
|
||||
initCounter <- What4.structField sym init counter
|
||||
nZero <- What4.natLit sym 0
|
||||
natCond <- What4.natEq sym initCounter nZero
|
||||
nZero <- What4.intLit sym 0
|
||||
natCond <- What4.intEq sym initCounter nZero
|
||||
andCond <- What4.andPred sym initCounterIsEven natCond
|
||||
return andCond
|
||||
|
||||
@ -122,9 +128,9 @@ counterTransitions sym state next =
|
||||
nextCounterIsEven <- What4.structField sym next counterIsEven
|
||||
nextCounter <- What4.structField sym next counter
|
||||
-- (= next.counter (+ 1 state.counter))
|
||||
nOne <- What4.natLit sym 1
|
||||
nStatePlusOne <- What4.natAdd sym nOne stateCounter
|
||||
natCond <- What4.natEq sym nextCounter nStatePlusOne
|
||||
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
|
||||
@ -154,9 +160,9 @@ counterTransitionSystem sym =
|
||||
|
||||
type RealsStateType =
|
||||
Ctx.EmptyCtx
|
||||
Ctx.::> BaseRealType
|
||||
Ctx.::> BaseRealType
|
||||
Ctx.::> BaseRealType
|
||||
Ctx.::> BaseTypes.BaseRealType
|
||||
Ctx.::> BaseTypes.BaseRealType
|
||||
Ctx.::> BaseTypes.BaseRealType
|
||||
|
||||
realsStateFields :: [What4.SolverSymbol]
|
||||
realsStateFields = userSymbol' <$> ["P", "x", "n"]
|
||||
@ -164,13 +170,13 @@ realsStateFields = userSymbol' <$> ["P", "x", "n"]
|
||||
realsFieldNames :: Ctx.Assignment (L.Const What4.SolverSymbol) RealsStateType
|
||||
realsFieldNames = makeFieldNames realsStateFields knownRepr
|
||||
|
||||
pReals :: Ctx.Index RealsStateType BaseRealType
|
||||
pReals :: Ctx.Index RealsStateType BaseTypes.BaseRealType
|
||||
pReals = Ctx.natIndex @0
|
||||
|
||||
xReals :: Ctx.Index RealsStateType BaseRealType
|
||||
xReals :: Ctx.Index RealsStateType BaseTypes.BaseRealType
|
||||
xReals = Ctx.natIndex @1
|
||||
|
||||
nReals :: Ctx.Index RealsStateType BaseRealType
|
||||
nReals :: Ctx.Index RealsStateType BaseTypes.BaseRealType
|
||||
nReals = Ctx.natIndex @2
|
||||
|
||||
realsInitial ::
|
@ -5,7 +5,7 @@ synopsis: Generates transition systems from What4 descriptions
|
||||
description: Generates transition systems from What4 descriptions
|
||||
author: Valentin Robert <val@galois.com>
|
||||
maintainer: Valentin Robert <val@galois.com>
|
||||
copyright: Galois, Inc. 2020
|
||||
copyright: Galois, Inc. 2020-2021
|
||||
license: BSD-3-Clause
|
||||
license-file: LICENSE
|
||||
build-type: Simple
|
||||
@ -13,7 +13,7 @@ build-type: Simple
|
||||
common dependencies
|
||||
build-depends:
|
||||
, ansi-wl-pprint ^>=0.6
|
||||
, base >=4.13 && <4.15
|
||||
, base >=4.12 && <4.15
|
||||
, bytestring
|
||||
, containers ^>=0.6
|
||||
, io-streams
|
||||
@ -22,11 +22,14 @@ common dependencies
|
||||
, mtl
|
||||
, parameterized-utils >=2.0 && <2.2
|
||||
, text
|
||||
, what4
|
||||
, what4 ^>=1.1
|
||||
|
||||
library
|
||||
import: dependencies
|
||||
exposed-modules: What4.TransitionSystem
|
||||
exposed-modules:
|
||||
What4.TransitionSystem
|
||||
What4.TransitionSystem.Exporter.Sally
|
||||
|
||||
other-modules: Paths_what4_transition_system
|
||||
hs-source-dirs: src
|
||||
ghc-options:
|
||||
@ -35,14 +38,15 @@ library
|
||||
|
||||
default-language: Haskell2010
|
||||
|
||||
test-suite transition-system-tests
|
||||
test-suite what4-transition-system-tests
|
||||
import: dependencies
|
||||
type: exitcode-stdio-1.0
|
||||
main-is: TransitionSystemTest.hs
|
||||
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
|
||||
|
Loading…
Reference in New Issue
Block a user