mirror of
https://github.com/GaloisInc/what4.git
synced 2024-11-29 13:55:51 +03:00
what4-transition-system: v0.0.2.0
This commit updates to the changes in language-sally 0.2.1.0. In particular, queries now receive a state they can use. This commit also updates the test suite (which is not actually testing anything but running the translation on examples), to account for all recent changes. This commit also removes some code that has made obsolete by the same recent changes: we no longer need to generate accessors as we receive a What4.SymStruct that we can reach into using What4.structField.
This commit is contained in:
Valentin Robert
parent
9ad0fc47b8
commit
a4c51d7062
@ -10,7 +10,7 @@ dependencies:
|
||||
- containers ^>= 0.6
|
||||
- io-streams
|
||||
- lens
|
||||
- language-sally ^>= 0.2
|
||||
- language-sally ^>= 0.2.1.0
|
||||
- mtl
|
||||
- parameterized-utils ^>= 2.0
|
||||
- text
|
||||
@ -42,4 +42,4 @@ tests:
|
||||
main: TransitionSystemTest.hs
|
||||
source-dirs: test
|
||||
|
||||
version: 0.0.1.0
|
||||
version: 0.0.2.0
|
||||
|
||||
@ -18,7 +18,6 @@ module What4.TransitionSystem
|
||||
( CtxState,
|
||||
TransitionSystem (..),
|
||||
createStateStruct,
|
||||
mkAccessors,
|
||||
mySallyNames,
|
||||
-- stateField,
|
||||
transitionSystemToSally,
|
||||
@ -28,9 +27,8 @@ where
|
||||
|
||||
import qualified Control.Lens as L
|
||||
import Control.Monad.Identity
|
||||
import Data.Functor.Const
|
||||
import Data.Functor.Const (Const (..))
|
||||
import qualified Data.Parameterized.Context as Ctx
|
||||
import Data.Parameterized.TraversableFC
|
||||
import qualified Language.Sally as S
|
||||
import What4.BaseTypes
|
||||
import What4.Expr
|
||||
@ -65,7 +63,20 @@ data TransitionSystem sym state = TransitionSystem
|
||||
What4.SymStruct sym state ->
|
||||
What4.SymStruct sym state ->
|
||||
IO [(S.Name, What4.Pred sym)],
|
||||
queries :: IO [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.
|
||||
queries ::
|
||||
What4.SymStruct sym state ->
|
||||
IO [What4.Pred sym]
|
||||
}
|
||||
|
||||
data SallyNames = SallyNames
|
||||
@ -124,36 +135,20 @@ sideConditions ::
|
||||
IO (S.SallyPred t)
|
||||
sideConditions sym stateReprs state =
|
||||
do
|
||||
preds <- concat <$> toListFC getConst <$> Ctx.traverseWithIndex createSideCondition stateReprs
|
||||
preds <- Ctx.traverseAndCollect sideConditionsForIndex stateReprs
|
||||
What4.andAllOf sym L.folded preds
|
||||
where
|
||||
createSideCondition :: Ctx.Index state bt -> BaseTypeRepr bt -> IO (Const [S.SallyPred t] bt)
|
||||
createSideCondition _index _tp = pure (Const []) -- FIXME
|
||||
-- do
|
||||
-- let zipped = Ctx.zipWith Pair stateReprs accessors
|
||||
-- natConditions <- foldrMFC' addSideCondition [] zipped
|
||||
-- What4.andAllOf sym L.folded natConditions
|
||||
-- where
|
||||
-- addSideCondition ::
|
||||
-- Product BaseTypeRepr (ExprSymFn t (CtxState state)) tp ->
|
||||
-- [S.SallyPred t] ->
|
||||
-- IO [S.SallyPred t]
|
||||
-- addSideCondition p acc = do
|
||||
-- c <- sideCondition p
|
||||
-- return $ c ++ acc
|
||||
-- sideCondition ::
|
||||
-- Product BaseTypeRepr (ExprSymFn t (CtxState state)) tp ->
|
||||
-- IO [S.SallyPred t]
|
||||
-- sideCondition (Pair BaseBoolRepr _) = return []
|
||||
-- sideCondition (Pair BaseNatRepr e) =
|
||||
-- do
|
||||
-- nZ <- What4.natLit sym 0
|
||||
-- natFieldValue <- What4.applySymFn sym e (Ctx.Empty Ctx.:> state)
|
||||
-- (: []) <$> What4.natLe sym nZ natFieldValue
|
||||
-- sideCondition (Pair BaseIntegerRepr _) = return []
|
||||
-- sideCondition (Pair BaseRealRepr _) = return []
|
||||
-- sideCondition (Pair (BaseBVRepr _) _) = return []
|
||||
-- sideCondition (Pair _ _) = error "Not implemented"
|
||||
sideConditionsForIndex :: Ctx.Index state tp -> BaseTypeRepr tp -> IO [S.SallyPred t]
|
||||
sideConditionsForIndex _ BaseBoolRepr = return []
|
||||
sideConditionsForIndex i BaseNatRepr =
|
||||
do
|
||||
nZ <- What4.natLit sym 0
|
||||
natFieldValue <- What4.structField sym state i
|
||||
(: []) <$> What4.natLe sym nZ natFieldValue
|
||||
sideConditionsForIndex _ BaseIntegerRepr = return []
|
||||
sideConditionsForIndex _ BaseRealRepr = return []
|
||||
sideConditionsForIndex _ (BaseBVRepr _) = return []
|
||||
sideConditionsForIndex _ bt = error $ "sideConditions: Not implemented for base type " ++ show bt ++ ". Please report."
|
||||
|
||||
createStateStruct ::
|
||||
What4.IsSymExprBuilder sym =>
|
||||
@ -233,10 +228,17 @@ makeSallyTransitions
|
||||
return (allTransitions ++ [mainTransition])
|
||||
|
||||
makeSallyQueries ::
|
||||
S.Name ->
|
||||
[What4.Pred (ExprBuilder t st fs)] ->
|
||||
[S.SallyQuery t]
|
||||
makeSallyQueries systemName = map (sallyQuery systemName)
|
||||
sym ~ ExprBuilder t st fs =>
|
||||
sym ->
|
||||
SallyNames ->
|
||||
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 =
|
||||
@ -260,13 +262,11 @@ transitionSystemToSally
|
||||
stateName,
|
||||
systemName
|
||||
}
|
||||
ts@TransitionSystem
|
||||
{ queries
|
||||
} =
|
||||
ts =
|
||||
do
|
||||
sallyStateFormulaPredicate <- sallyInitialState sym ts
|
||||
sallyTransitions <- makeSallyTransitions sym sn ts
|
||||
sallyQueries <- makeSallyQueries systemName <$> queries
|
||||
sallyQueries <- makeSallyQueries sym sn ts
|
||||
let sallyInitialFormula =
|
||||
S.SallyStateFormula
|
||||
{ S.sallyStateFormulaName = initialName,
|
||||
@ -291,49 +291,5 @@ transitionSystemToSally
|
||||
S.sallyQueries
|
||||
}
|
||||
|
||||
-- | @mkAccessors@ creates an assignment of function symbols to each state field. The
|
||||
-- name is given by the @Const String@ assignment, the input type is the whole
|
||||
-- state type, and the return type is the type of the given field.
|
||||
mkAccessors ::
|
||||
What4.IsSymExprBuilder sym =>
|
||||
sym ->
|
||||
Ctx.Assignment BaseTypeRepr state ->
|
||||
Ctx.Assignment (Const What4.SolverSymbol) state ->
|
||||
IO (Ctx.Assignment (What4.SymFn sym (CtxState state)) state)
|
||||
mkAccessors sym stateType =
|
||||
Ctx.traverseWithIndex
|
||||
( \index (Const symbol) ->
|
||||
What4.freshTotalUninterpFn
|
||||
sym
|
||||
symbol
|
||||
(Ctx.Empty Ctx.:> BaseStructRepr stateType)
|
||||
(stateType Ctx.! index)
|
||||
)
|
||||
|
||||
-- | @freshStateVars@ instantiates a state type with fresh variables, and
|
||||
-- returns the assignment of fields to variables. This can be used any time a
|
||||
-- new state is needed.
|
||||
-- freshStateVars ::
|
||||
-- What4.IsSymExprBuilder sym =>
|
||||
-- sym ->
|
||||
-- String ->
|
||||
-- -- | state type
|
||||
-- Ctx.Assignment BaseTypeRepr state ->
|
||||
-- IO (Ctx.Assignment (SymExpr sym) state)
|
||||
-- freshStateVars sym name ctx =
|
||||
-- Ctx.traverseWithIndex (\ ndx -> What4.freshConstant sym (userSymbol' (name ++ "_" ++ show (Ctx.indexVal ndx)))) ctx
|
||||
|
||||
-- | A context with just one field, a struct type for the state
|
||||
type CtxState state = Ctx.EmptyCtx Ctx.::> BaseStructType state
|
||||
|
||||
-- stateField ::
|
||||
-- What4.IsSymExprBuilder sym =>
|
||||
-- sym ->
|
||||
-- -- Ctx.Assignment (What4.SymFn sym (CtxState state)) state ->
|
||||
-- -- L.Lens' (Ctx.Assignment (What4.SymFn sym (CtxState state)) state) (What4.SymFn sym (CtxState state) ret) ->
|
||||
-- Ctx.Index state ret ->
|
||||
-- What4.SymStruct sym state ->
|
||||
-- IO (SymExpr sym ret)
|
||||
-- stateField sym state index =
|
||||
-- What4.structField sym state index
|
||||
-- -- What4.applySymFn sym (L.view field fields) (Ctx.Empty Ctx.:> state)
|
||||
|
||||
@ -21,25 +21,11 @@ import qualified Control.Lens as L
|
||||
import Control.Monad (join)
|
||||
import qualified Data.Parameterized.Context as Ctx
|
||||
import Data.Parameterized.Nonce
|
||||
-- import Data.Parameterized.Some
|
||||
-- import Data.Parameterized.TraversableFC
|
||||
-- import qualified Data.Set as Set
|
||||
-- import Data.Text (Text)
|
||||
-- import qualified Data.Text.Lazy as Lazy
|
||||
-- import qualified Data.Text.Lazy.Builder as Builder
|
||||
import Language.Sally
|
||||
import Language.Sally.Writer
|
||||
import qualified System.IO.Streams as Streams
|
||||
-- import qualified Text.PrettyPrint.ANSI.Leijen as PP
|
||||
import What4.BaseTypes
|
||||
import What4.Expr
|
||||
import What4.Expr.Builder
|
||||
import qualified What4.Interface as What4
|
||||
-- import What4.ProblemFeatures
|
||||
-- import What4.Protocol.SMTLib2 hiding (newWriter)
|
||||
-- import What4.Protocol.SMTLib2.Syntax as SMT2
|
||||
import What4.Protocol.SMTWriter as SMTWriter
|
||||
import What4.Solver.Adapter
|
||||
import What4.TransitionSystem
|
||||
import Prelude hiding (init)
|
||||
|
||||
@ -55,8 +41,8 @@ displayTransitionSystem ::
|
||||
displayTransitionSystem sym transitionSystem =
|
||||
do
|
||||
sts <- transitionSystemToSally sym mySallyNames transitionSystem
|
||||
sexp <- sexpOfTrResult sym sts
|
||||
print . sxPretty $ sexp
|
||||
sexp <- sexpOfSally sym sts
|
||||
print . sexpToCompactDoc $ sexp
|
||||
|
||||
main :: IO ()
|
||||
main =
|
||||
@ -128,7 +114,7 @@ counterTransitions ::
|
||||
What4.SymStruct sym CounterStateType ->
|
||||
-- | next state
|
||||
What4.SymStruct sym CounterStateType ->
|
||||
IO [(String, What4.Pred sym)]
|
||||
IO [(Name, What4.Pred sym)]
|
||||
counterTransitions sym state next =
|
||||
do
|
||||
stateCounterIsEven <- What4.structField sym state counterIsEven
|
||||
@ -143,7 +129,7 @@ counterTransitions sym state next =
|
||||
bStateNeg <- What4.notPred sym stateCounterIsEven
|
||||
boolCond <- What4.eqPred sym nextCounterIsEven bStateNeg
|
||||
andCond <- What4.andPred sym boolCond natCond
|
||||
return [("CounterTransition", andCond)]
|
||||
return [(userSymbol' "CounterTransition", andCond)]
|
||||
|
||||
-- | TODO
|
||||
counterTransitionSystem ::
|
||||
@ -153,11 +139,11 @@ counterTransitionSystem sym =
|
||||
do
|
||||
return $
|
||||
TransitionSystem
|
||||
{ stateFieldsRepr = knownRepr,
|
||||
stateFieldsNames = counterFieldNames,
|
||||
initialStatePred = counterInitial sym,
|
||||
{ stateReprs = knownRepr,
|
||||
stateNames = counterFieldNames,
|
||||
initialStatePredicate = counterInitial sym,
|
||||
stateTransitions = counterTransitions sym,
|
||||
queries = pure []
|
||||
queries = const (pure [])
|
||||
}
|
||||
|
||||
--
|
||||
@ -211,7 +197,7 @@ realsTransitions ::
|
||||
What4.SymStruct sym RealsStateType ->
|
||||
-- | next state
|
||||
What4.SymStruct sym RealsStateType ->
|
||||
IO [(String, What4.Pred sym)]
|
||||
IO [(Name, What4.Pred sym)]
|
||||
realsTransitions sym state next =
|
||||
do
|
||||
pState <- What4.structField sym state pReals
|
||||
@ -227,7 +213,7 @@ realsTransitions sym state next =
|
||||
-- (= next.x state.x)
|
||||
c3 <- What4.realEq sym xNext xState
|
||||
t <- What4.andPred sym c1 =<< What4.andPred sym c2 c3
|
||||
return [("RealsTransition", t)]
|
||||
return [(userSymbol' "RealsTransition", t)]
|
||||
|
||||
-- | TODO
|
||||
realsTransitionSystem ::
|
||||
@ -237,9 +223,9 @@ realsTransitionSystem sym =
|
||||
do
|
||||
return $
|
||||
TransitionSystem
|
||||
{ stateFieldsRepr = knownRepr,
|
||||
stateFieldsNames = realsFieldNames,
|
||||
initialStatePred = realsInitial sym,
|
||||
{ stateReprs = knownRepr,
|
||||
stateNames = realsFieldNames,
|
||||
initialStatePredicate = realsInitial sym,
|
||||
stateTransitions = realsTransitions sym,
|
||||
queries = pure []
|
||||
queries = const (pure [])
|
||||
}
|
||||
|
||||
@ -1,19 +1,20 @@
|
||||
cabal-version: 1.12
|
||||
|
||||
-- This file has been generated from package.yaml by hpack version 0.33.0.
|
||||
-- This file has been generated from package.yaml by hpack version 0.34.2.
|
||||
--
|
||||
-- see: https://github.com/sol/hpack
|
||||
--
|
||||
-- hash: d51f186fc63bb5e8b1476af71e4f661d2ca4f5df1f64d4686a18e2ad6351f6c4
|
||||
-- hash: 962c45929ee60827138ddd7bb54e11f0c7c760ffb0661c504cfce5253c8ce4d6
|
||||
|
||||
name: what4-transition-system
|
||||
version: 0.0.1.0
|
||||
version: 0.0.2.0
|
||||
synopsis: Generates transition systems from What4 descriptions
|
||||
description: Generates transition systems from What4 descriptions
|
||||
author: Valentin Robert <valentin.robert.42@gmail.com>
|
||||
maintainer: Valentin Robert <valentin.robert.42@gmail.com>
|
||||
copyright: Galois, Inc. 2020
|
||||
license: ISC
|
||||
license: BSD3
|
||||
license-file: LICENSE
|
||||
build-type: Simple
|
||||
|
||||
library
|
||||
@ -30,7 +31,7 @@ library
|
||||
, bytestring
|
||||
, containers >=0.6 && <0.7
|
||||
, io-streams
|
||||
, language-sally >=0.2 && <0.3
|
||||
, language-sally >=0.2.1.0 && <0.3
|
||||
, lens
|
||||
, mtl
|
||||
, parameterized-utils >=2.0 && <2.1
|
||||
@ -52,7 +53,7 @@ test-suite transition-system-tests
|
||||
, bytestring
|
||||
, containers >=0.6 && <0.7
|
||||
, io-streams
|
||||
, language-sally >=0.2 && <0.3
|
||||
, language-sally >=0.2.1.0 && <0.3
|
||||
, lens
|
||||
, mtl
|
||||
, parameterized-utils >=2.0 && <2.1
|
||||
|
||||
Loading…
Reference in New Issue
Block a user