From 9ad0fc47b801b096a5af5bf7310fc080af8a3754 Mon Sep 17 00:00:00 2001 From: Valentin Robert Date: Thu, 11 Jun 2020 10:06:45 +0200 Subject: [PATCH 1/4] what4-transition-system: v0.0.1.0 --- .gitmodules | 7 + dependencies/language-sally | 1 + what4-transition-system/LICENSE | 30 ++ what4-transition-system/package.yaml | 45 +++ .../src/What4/TransitionSystem.hs | 339 ++++++++++++++++++ .../test/TransitionSystemTest.hs | 245 +++++++++++++ .../what4-transition-system.cabal | 62 ++++ 7 files changed, 729 insertions(+) create mode 160000 dependencies/language-sally create mode 100644 what4-transition-system/LICENSE create mode 100644 what4-transition-system/package.yaml create mode 100644 what4-transition-system/src/What4/TransitionSystem.hs create mode 100644 what4-transition-system/test/TransitionSystemTest.hs create mode 100644 what4-transition-system/what4-transition-system.cabal diff --git a/.gitmodules b/.gitmodules index 9ec4b341..31f3286a 100644 --- a/.gitmodules +++ b/.gitmodules @@ -7,3 +7,10 @@ [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 + diff --git a/dependencies/language-sally b/dependencies/language-sally new file mode 160000 index 00000000..a52404a9 --- /dev/null +++ b/dependencies/language-sally @@ -0,0 +1 @@ +Subproject commit a52404a9d3f2ff88809f0ad2832ffa518b7ac89b 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/package.yaml b/what4-transition-system/package.yaml new file mode 100644 index 00000000..1c22cfb1 --- /dev/null +++ b/what4-transition-system/package.yaml @@ -0,0 +1,45 @@ +author: + - Valentin Robert + +copyright: Galois, Inc. 2020 + +dependencies: + - ansi-wl-pprint ^>= 0.6 + - base ^>= 4.13 + - bytestring + - containers ^>= 0.6 + - io-streams + - lens + - language-sally ^>= 0.2 + - mtl + - parameterized-utils ^>= 2.0 + - text + - what4 + +description: Generates transition systems from What4 descriptions + +ghc-options: + - -Wall + - -Werror=incomplete-patterns + - -Werror=missing-methods + - -Werror=overlapping-patterns + +library: + exposed-modules: + - What4.TransitionSystem + source-dirs: src + +license: BSD3 + +name: what4-transition-system + +synopsis: Generates transition systems from What4 descriptions + +tests: + transition-system-tests: + dependencies: + - what4-transition-system + main: TransitionSystemTest.hs + source-dirs: test + +version: 0.0.1.0 diff --git a/what4-transition-system/src/What4/TransitionSystem.hs b/what4-transition-system/src/What4/TransitionSystem.hs new file mode 100644 index 00000000..0fcae8f5 --- /dev/null +++ b/what4-transition-system/src/What4/TransitionSystem.hs @@ -0,0 +1,339 @@ +{-# 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 + ( CtxState, + TransitionSystem (..), + createStateStruct, + mkAccessors, + mySallyNames, + -- stateField, + transitionSystemToSally, + userSymbol', + ) +where + +import qualified Control.Lens as L +import Control.Monad.Identity +import Data.Functor.Const +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.TraversableFC +import qualified Language.Sally as S +import What4.BaseTypes +import What4.Expr +import qualified What4.Interface as What4 +import Prelude hiding (init) + +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. +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 + 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. Returns 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)], + queries :: 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 + } + +-- | @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" + } + +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 + } + +-- | 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 -> + -- | state type + Ctx.Assignment BaseTypeRepr state -> + -- | state on which to operate + What4.SymStruct (ExprBuilder t st fs) state -> + IO (S.SallyPred t) +sideConditions sym stateReprs state = + do + preds <- concat <$> toListFC getConst <$> Ctx.traverseWithIndex createSideCondition 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" + +createStateStruct :: + What4.IsSymExprBuilder sym => + sym -> + String -> + Ctx.Assignment 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 + +sallyInitialState :: + ExprBuilder t st fs -> + TransitionSystem (ExprBuilder t st fs) state -> + IO (S.SallyPred t) +sallyInitialState + 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 + } + ) = + 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 $ + S.SallyTransition + { S.transitionName = name, + S.transitionDomain = stateName, + -- traLet = [], + S.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 + 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 + return (allTransitions ++ [mainTransition]) + +makeSallyQueries :: + S.Name -> + [What4.Pred (ExprBuilder t st fs)] -> + [S.SallyQuery t] +makeSallyQueries systemName = map (sallyQuery systemName) + +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 + sym + sn@SallyNames + { initialName, + mainTransitionName, + stateName, + systemName + } + ts@TransitionSystem + { queries + } = + do + sallyStateFormulaPredicate <- sallyInitialState sym ts + sallyTransitions <- makeSallyTransitions sym sn ts + sallyQueries <- makeSallyQueries systemName <$> queries + 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 + } + +-- | @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) diff --git a/what4-transition-system/test/TransitionSystemTest.hs b/what4-transition-system/test/TransitionSystemTest.hs new file mode 100644 index 00000000..9fc4a5fc --- /dev/null +++ b/what4-transition-system/test/TransitionSystemTest.hs @@ -0,0 +1,245 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | +-- Module : TransitionSystemTest +-- Copyright : (c) Galois Inc, 2020 +-- License : BSD3 +-- Maintainer : valentin.robert.42@gmail.com +-- | +module Main where + +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) + +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 <- transitionSystemToSally sym mySallyNames transitionSystem + sexp <- sexpOfTrResult sym sts + print . sxPretty $ 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 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.::> BaseBoolType Ctx.::> BaseNatType + +counterStateFields :: [What4.SolverSymbol] +counterStateFields = userSymbol' <$> ["counterIsEven", "counter"] + +counterFieldNames :: Ctx.Assignment (L.Const What4.SolverSymbol) CounterStateType +counterFieldNames = makeFieldNames counterStateFields knownRepr + +counterIsEven :: Ctx.Index CounterStateType BaseBoolType +counterIsEven = Ctx.natIndex @0 + +counter :: Ctx.Index CounterStateType BaseNatType +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.natLit sym 0 + natCond <- What4.natEq 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 [(String, 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.natLit sym 1 + nStatePlusOne <- What4.natAdd sym nOne stateCounter + natCond <- What4.natEq 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 [("CounterTransition", andCond)] + +-- | TODO +counterTransitionSystem :: + ExprBuilder t st fs -> + IO (TransitionSystem (ExprBuilder t st fs) CounterStateType) +counterTransitionSystem sym = + do + return $ + TransitionSystem + { stateFieldsRepr = knownRepr, + stateFieldsNames = counterFieldNames, + initialStatePred = counterInitial sym, + stateTransitions = counterTransitions sym, + queries = pure [] + } + +-- +-- Example 2: using real numbers +-- + +-- based on sally/test/regress/bmc/nra/algebraic.mcmt + +type RealsStateType = + Ctx.EmptyCtx + Ctx.::> BaseRealType + Ctx.::> BaseRealType + Ctx.::> 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 BaseRealType +pReals = Ctx.natIndex @0 + +xReals :: Ctx.Index RealsStateType BaseRealType +xReals = Ctx.natIndex @1 + +nReals :: Ctx.Index RealsStateType 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 [(String, 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 [("RealsTransition", t)] + +-- | TODO +realsTransitionSystem :: + ExprBuilder t st fs -> + IO (TransitionSystem (ExprBuilder t st fs) RealsStateType) +realsTransitionSystem sym = + do + return $ + TransitionSystem + { stateFieldsRepr = knownRepr, + stateFieldsNames = realsFieldNames, + initialStatePred = realsInitial sym, + stateTransitions = realsTransitions sym, + queries = 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..dcf47f62 --- /dev/null +++ b/what4-transition-system/what4-transition-system.cabal @@ -0,0 +1,62 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.33.0. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: d51f186fc63bb5e8b1476af71e4f661d2ca4f5df1f64d4686a18e2ad6351f6c4 + +name: what4-transition-system +version: 0.0.1.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 +license: ISC +build-type: Simple + +library + exposed-modules: + What4.TransitionSystem + other-modules: + Paths_what4_transition_system + hs-source-dirs: + src + ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns + build-depends: + ansi-wl-pprint >=0.6 && <0.7 + , base >=4.13 && <4.14 + , bytestring + , containers >=0.6 && <0.7 + , io-streams + , language-sally >=0.2 && <0.3 + , lens + , mtl + , parameterized-utils >=2.0 && <2.1 + , text + , what4 + default-language: Haskell2010 + +test-suite transition-system-tests + type: exitcode-stdio-1.0 + main-is: TransitionSystemTest.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: + ansi-wl-pprint >=0.6 && <0.7 + , base >=4.13 && <4.14 + , bytestring + , containers >=0.6 && <0.7 + , io-streams + , language-sally >=0.2 && <0.3 + , lens + , mtl + , parameterized-utils >=2.0 && <2.1 + , text + , what4 + , what4-transition-system + default-language: Haskell2010 From a4c51d7062d815743a318dd6030907181bbea396 Mon Sep 17 00:00:00 2001 From: Valentin Robert Date: Wed, 24 Jun 2020 14:30:28 +0200 Subject: [PATCH 2/4] 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. --- what4-transition-system/package.yaml | 4 +- .../src/What4/TransitionSystem.hs | 124 ++++++------------ .../test/TransitionSystemTest.hs | 42 ++---- .../what4-transition-system.cabal | 13 +- 4 files changed, 63 insertions(+), 120 deletions(-) diff --git a/what4-transition-system/package.yaml b/what4-transition-system/package.yaml index 1c22cfb1..4f30380a 100644 --- a/what4-transition-system/package.yaml +++ b/what4-transition-system/package.yaml @@ -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 diff --git a/what4-transition-system/src/What4/TransitionSystem.hs b/what4-transition-system/src/What4/TransitionSystem.hs index 0fcae8f5..36b3d419 100644 --- a/what4-transition-system/src/What4/TransitionSystem.hs +++ b/what4-transition-system/src/What4/TransitionSystem.hs @@ -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) diff --git a/what4-transition-system/test/TransitionSystemTest.hs b/what4-transition-system/test/TransitionSystemTest.hs index 9fc4a5fc..f68ac9f9 100644 --- a/what4-transition-system/test/TransitionSystemTest.hs +++ b/what4-transition-system/test/TransitionSystemTest.hs @@ -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 []) } diff --git a/what4-transition-system/what4-transition-system.cabal b/what4-transition-system/what4-transition-system.cabal index dcf47f62..d4399610 100644 --- a/what4-transition-system/what4-transition-system.cabal +++ b/what4-transition-system/what4-transition-system.cabal @@ -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 maintainer: Valentin Robert 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 From 95a514fba2aff514d4fb2d54e1d3b4e52fd79669 Mon Sep 17 00:00:00 2001 From: Valentin Robert Date: Mon, 22 Mar 2021 18:09:06 -0700 Subject: [PATCH 3/4] what4-transition-system: v0.0.3.0 Update to changes in language-sally. --- cabal.project | 2 + what4-transition-system/package.yaml | 45 ---------- .../src/What4/TransitionSystem.hs | 5 -- .../what4-transition-system.cabal | 87 ++++++++----------- 4 files changed, 38 insertions(+), 101 deletions(-) delete mode 100644 what4-transition-system/package.yaml 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/what4-transition-system/package.yaml b/what4-transition-system/package.yaml deleted file mode 100644 index 4f30380a..00000000 --- a/what4-transition-system/package.yaml +++ /dev/null @@ -1,45 +0,0 @@ -author: - - Valentin Robert - -copyright: Galois, Inc. 2020 - -dependencies: - - ansi-wl-pprint ^>= 0.6 - - base ^>= 4.13 - - bytestring - - containers ^>= 0.6 - - io-streams - - lens - - language-sally ^>= 0.2.1.0 - - mtl - - parameterized-utils ^>= 2.0 - - text - - what4 - -description: Generates transition systems from What4 descriptions - -ghc-options: - - -Wall - - -Werror=incomplete-patterns - - -Werror=missing-methods - - -Werror=overlapping-patterns - -library: - exposed-modules: - - What4.TransitionSystem - source-dirs: src - -license: BSD3 - -name: what4-transition-system - -synopsis: Generates transition systems from What4 descriptions - -tests: - transition-system-tests: - dependencies: - - what4-transition-system - main: TransitionSystemTest.hs - source-dirs: test - -version: 0.0.2.0 diff --git a/what4-transition-system/src/What4/TransitionSystem.hs b/what4-transition-system/src/What4/TransitionSystem.hs index 36b3d419..bd83f840 100644 --- a/what4-transition-system/src/What4/TransitionSystem.hs +++ b/what4-transition-system/src/What4/TransitionSystem.hs @@ -140,11 +140,6 @@ sideConditions sym stateReprs state = where 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 [] diff --git a/what4-transition-system/what4-transition-system.cabal b/what4-transition-system/what4-transition-system.cabal index d4399610..489286c8 100644 --- a/what4-transition-system/what4-transition-system.cabal +++ b/what4-transition-system/what4-transition-system.cabal @@ -1,63 +1,48 @@ -cabal-version: 1.12 +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 +license: BSD-3-Clause +license-file: LICENSE +build-type: Simple --- This file has been generated from package.yaml by hpack version 0.34.2. --- --- see: https://github.com/sol/hpack --- --- hash: 962c45929ee60827138ddd7bb54e11f0c7c760ffb0661c504cfce5253c8ce4d6 - -name: what4-transition-system -version: 0.0.2.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 -license: BSD3 -license-file: LICENSE -build-type: Simple - -library - exposed-modules: - What4.TransitionSystem - other-modules: - Paths_what4_transition_system - hs-source-dirs: - src - ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns +common dependencies build-depends: - ansi-wl-pprint >=0.6 && <0.7 - , base >=4.13 && <4.14 + , ansi-wl-pprint ^>=0.6 + , base >=4.13 && <4.15 , bytestring - , containers >=0.6 && <0.7 + , containers ^>=0.6 , io-streams - , language-sally >=0.2.1.0 && <0.3 + , language-sally ^>=0.3 , lens , mtl - , parameterized-utils >=2.0 && <2.1 + , parameterized-utils >=2.0 && <2.2 , text , what4 + +library + import: dependencies + exposed-modules: What4.TransitionSystem + 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 transition-system-tests - type: exitcode-stdio-1.0 - main-is: TransitionSystemTest.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: - ansi-wl-pprint >=0.6 && <0.7 - , base >=4.13 && <4.14 - , bytestring - , containers >=0.6 && <0.7 - , io-streams - , language-sally >=0.2.1.0 && <0.3 - , lens - , mtl - , parameterized-utils >=2.0 && <2.1 - , text - , what4 - , what4-transition-system + import: dependencies + type: exitcode-stdio-1.0 + main-is: TransitionSystemTest.hs + other-modules: Paths_what4_transition_system + hs-source-dirs: test + ghc-options: + -Wall -Werror=incomplete-patterns -Werror=missing-methods + -Werror=overlapping-patterns + default-language: Haskell2010 From f74d8eaa4eb71592409983e2e1ddaadf029ccd7f Mon Sep 17 00:00:00 2001 From: Valentin Robert Date: Mon, 22 Mar 2021 18:09:06 -0700 Subject: [PATCH 4/4] Update to changes in language-sally. --- .gitmodules | 3 - dependencies/language-sally | 2 +- .../src/What4/TransitionSystem.hs | 308 ++++++------------ .../What4/TransitionSystem/Exporter/Sally.hs | 112 +++++++ .../test/{TransitionSystemTest.hs => Main.hs} | 54 +-- .../what4-transition-system.cabal | 16 +- 6 files changed, 249 insertions(+), 246 deletions(-) create mode 100644 what4-transition-system/src/What4/TransitionSystem/Exporter/Sally.hs rename what4-transition-system/test/{TransitionSystemTest.hs => Main.hs} (81%) diff --git a/.gitmodules b/.gitmodules index 31f3286a..30b639c2 100644 --- a/.gitmodules +++ b/.gitmodules @@ -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 diff --git a/dependencies/language-sally b/dependencies/language-sally index a52404a9..2ed17f2e 160000 --- a/dependencies/language-sally +++ b/dependencies/language-sally @@ -1 +1 @@ -Subproject commit a52404a9d3f2ff88809f0ad2832ffa518b7ac89b +Subproject commit 2ed17f2e5522bf3b2abcca79ce00b6e4567a681d diff --git a/what4-transition-system/src/What4/TransitionSystem.hs b/what4-transition-system/src/What4/TransitionSystem.hs index bd83f840..11d2ce21 100644 --- a/what4-transition-system/src/What4/TransitionSystem.hs +++ b/what4-transition-system/src/What4/TransitionSystem.hs @@ -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 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/TransitionSystemTest.hs b/what4-transition-system/test/Main.hs similarity index 81% rename from what4-transition-system/test/TransitionSystemTest.hs rename to what4-transition-system/test/Main.hs index f68ac9f9..ec084787 100644 --- a/what4-transition-system/test/TransitionSystemTest.hs +++ b/what4-transition-system/test/Main.hs @@ -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 :: diff --git a/what4-transition-system/what4-transition-system.cabal b/what4-transition-system/what4-transition-system.cabal index 489286c8..29bb1847 100644 --- a/what4-transition-system/what4-transition-system.cabal +++ b/what4-transition-system/what4-transition-system.cabal @@ -5,7 +5,7 @@ synopsis: Generates transition systems from What4 descriptions description: Generates transition systems from What4 descriptions author: Valentin Robert maintainer: Valentin Robert -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