mirror of
https://github.com/digital-asset/daml.git
synced 2024-09-20 01:07:18 +03:00
WIP: Draft version constraint generation (#5472)
First version of static verification tool. The current state of the tool: - Reads DAR files. - Partially evaluates the code. - Generates constraints for the field and choice to be verified. - Passes the constraints to an SMT solver. - Some basic tests.
This commit is contained in:
Gert-Jan Bottu
GitHub
parent
d7cc5e07c3
commit
2af134ca69
@ -896,6 +896,15 @@ nixpkgs_package(
|
||||
repositories = dev_env_nix_repos,
|
||||
)
|
||||
|
||||
nixpkgs_package(
|
||||
name = "z3_nix",
|
||||
attribute_path = "z3",
|
||||
fail_not_supported = False,
|
||||
nix_file = "//nix:bazel.nix",
|
||||
nix_file_deps = common_nix_file_deps,
|
||||
repositories = dev_env_nix_repos,
|
||||
) if not is_windows else None
|
||||
|
||||
dev_env_tool(
|
||||
name = "postgresql_dev_env",
|
||||
nix_include = [
|
||||
|
||||
@ -640,6 +640,7 @@ exports_files(["stack.exe"], visibility = ["//visibility:public"])
|
||||
"semigroups",
|
||||
"semver",
|
||||
"silently",
|
||||
"simple-smt",
|
||||
"sorted-list",
|
||||
"split",
|
||||
"stache",
|
||||
|
||||
@ -3,7 +3,7 @@
|
||||
|
||||
-- | DAML-LF Numeric literals, with scale attached.
|
||||
module DA.Daml.LF.Ast.Numeric
|
||||
( Numeric
|
||||
( Numeric (..)
|
||||
, NumericError (..)
|
||||
, E10
|
||||
, numeric
|
||||
|
||||
131
compiler/daml-lf-verify/BUILD.bazel
Normal file
131
compiler/daml-lf-verify/BUILD.bazel
Normal file
@ -0,0 +1,131 @@
|
||||
# Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
# SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
load("//rules_daml:daml.bzl", "daml_compile")
|
||||
load("//bazel_tools:haskell.bzl", "da_haskell_binary", "da_haskell_library", "da_haskell_test")
|
||||
load("@os_info//:os_info.bzl", "is_windows")
|
||||
|
||||
da_haskell_binary(
|
||||
name = "daml-lf-verify",
|
||||
srcs = glob(["src/**/*.hs"]),
|
||||
data = [
|
||||
"@z3_nix//:bin/z3",
|
||||
] if not is_windows else [],
|
||||
hackage_deps = [
|
||||
"aeson",
|
||||
"base",
|
||||
"bytestring",
|
||||
"containers",
|
||||
"deepseq",
|
||||
"Decimal",
|
||||
"extra",
|
||||
"filepath",
|
||||
"ghc-lib-parser",
|
||||
"hashable",
|
||||
"lens",
|
||||
"mtl",
|
||||
"optparse-applicative",
|
||||
"prettyprinter",
|
||||
"recursion-schemes",
|
||||
"safe",
|
||||
"scientific",
|
||||
"simple-smt",
|
||||
"template-haskell",
|
||||
"text",
|
||||
"time",
|
||||
"unordered-containers",
|
||||
"zip-archive",
|
||||
],
|
||||
main_function = "DA.Daml.LF.Verify.main",
|
||||
src_strip_prefix = "src",
|
||||
visibility = ["//visibility:public"],
|
||||
deps = [
|
||||
"//compiler/daml-lf-ast",
|
||||
"//compiler/daml-lf-proto",
|
||||
"//compiler/daml-lf-reader",
|
||||
"//compiler/daml-lf-tools",
|
||||
"//libs-haskell/bazel-runfiles",
|
||||
"//libs-haskell/da-hs-base",
|
||||
],
|
||||
)
|
||||
|
||||
da_haskell_library(
|
||||
name = "daml-lf-verify-lib",
|
||||
srcs = glob(["src/**/*.hs"]),
|
||||
data = [
|
||||
"@z3_nix//:bin/z3",
|
||||
] if not is_windows else [],
|
||||
hackage_deps = [
|
||||
"aeson",
|
||||
"base",
|
||||
"bytestring",
|
||||
"containers",
|
||||
"deepseq",
|
||||
"Decimal",
|
||||
"extra",
|
||||
"filepath",
|
||||
"ghc-lib-parser",
|
||||
"hashable",
|
||||
"lens",
|
||||
"mtl",
|
||||
"optparse-applicative",
|
||||
"prettyprinter",
|
||||
"recursion-schemes",
|
||||
"safe",
|
||||
"scientific",
|
||||
"simple-smt",
|
||||
"template-haskell",
|
||||
"text",
|
||||
"time",
|
||||
"unordered-containers",
|
||||
"zip-archive",
|
||||
],
|
||||
src_strip_prefix = "src",
|
||||
visibility = ["//visibility:public"],
|
||||
deps = [
|
||||
"//compiler/daml-lf-ast",
|
||||
"//compiler/daml-lf-proto",
|
||||
"//compiler/daml-lf-reader",
|
||||
"//compiler/daml-lf-tools",
|
||||
"//libs-haskell/bazel-runfiles",
|
||||
"//libs-haskell/da-hs-base",
|
||||
],
|
||||
)
|
||||
|
||||
daml_compile(
|
||||
name = "quickstart",
|
||||
srcs = glob(["daml/quickstart/**/*.daml"]),
|
||||
version = "1.0.0",
|
||||
)
|
||||
|
||||
daml_compile(
|
||||
name = "conditionals",
|
||||
srcs = glob(["daml/conditionals/**/*.daml"]),
|
||||
version = "1.0.0",
|
||||
)
|
||||
|
||||
da_haskell_test(
|
||||
name = "verify-tests",
|
||||
srcs = glob(["tests/**/*.hs"]),
|
||||
data = [
|
||||
":conditionals.dar",
|
||||
":quickstart.dar",
|
||||
] if not is_windows else [],
|
||||
hackage_deps = [
|
||||
"base",
|
||||
"containers",
|
||||
"filepath",
|
||||
"tasty",
|
||||
"tasty-hunit",
|
||||
],
|
||||
main_function = "DA.Daml.LF.Verify.Tests.mainTest",
|
||||
src_strip_prefix = "tests",
|
||||
visibility = ["//visibility:public"],
|
||||
deps = [
|
||||
":daml-lf-verify-lib",
|
||||
"//compiler/daml-lf-ast",
|
||||
"//libs-haskell/bazel-runfiles",
|
||||
"//libs-haskell/da-hs-base",
|
||||
"//libs-haskell/test-utils",
|
||||
],
|
||||
) if not is_windows else None
|
||||
61
compiler/daml-lf-verify/daml/conditionals/daml/Iou.daml
Normal file
61
compiler/daml-lf-verify/daml/conditionals/daml/Iou.daml
Normal file
@ -0,0 +1,61 @@
|
||||
-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
|
||||
module Iou where
|
||||
|
||||
template Iou with
|
||||
owner: Party
|
||||
content: Int
|
||||
where
|
||||
signatory owner
|
||||
|
||||
choice SuccA: ContractId Iou
|
||||
controller owner
|
||||
do
|
||||
if False
|
||||
then create Iou with owner; content = content
|
||||
else create Iou with owner; content = content
|
||||
|
||||
choice SuccB: ContractId Iou
|
||||
controller owner
|
||||
do
|
||||
if 1 == 1
|
||||
then create Iou with owner; content = content
|
||||
else create Iou with owner; content = 0
|
||||
|
||||
choice SuccC: ContractId Iou
|
||||
controller owner
|
||||
do
|
||||
if True
|
||||
then do
|
||||
_ <- create Iou with owner; content = content
|
||||
create Iou with owner; content = 0
|
||||
else create Iou with owner; content = content
|
||||
|
||||
choice SuccD: ContractId Iou
|
||||
controller owner
|
||||
do
|
||||
if True
|
||||
then do
|
||||
cid1 <- create Iou with owner; content = content
|
||||
archive cid1
|
||||
create Iou with owner; content = content
|
||||
else create Iou with owner; content = content
|
||||
|
||||
choice FailA: ContractId Iou
|
||||
controller owner
|
||||
do
|
||||
if 1 == 1
|
||||
then create Iou with owner; content = 0
|
||||
else create Iou with owner; content = content
|
||||
|
||||
choice FailB: ContractId Iou
|
||||
controller owner
|
||||
do
|
||||
if False
|
||||
then create Iou with owner; content = content
|
||||
else do
|
||||
_ <- create Iou with owner; content = content
|
||||
create Iou with owner; content = content
|
||||
|
||||
86
compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml
Normal file
86
compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml
Normal file
@ -0,0 +1,86 @@
|
||||
-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
|
||||
module Iou where
|
||||
|
||||
type IouCid = ContractId Iou
|
||||
|
||||
template Iou
|
||||
with
|
||||
issuer : Party
|
||||
owner : Party
|
||||
currency : Text
|
||||
amount : Decimal
|
||||
observers : [Party]
|
||||
where
|
||||
ensure amount > 0.0
|
||||
|
||||
signatory issuer, owner
|
||||
|
||||
observer observers
|
||||
|
||||
controller owner can
|
||||
|
||||
-- Split the IOU by dividing the amount.
|
||||
Iou_Split : (IouCid, IouCid)
|
||||
with
|
||||
splitAmount: Decimal
|
||||
do
|
||||
let restAmount = amount - splitAmount
|
||||
splitCid <- create this with amount = splitAmount
|
||||
restCid <- create this with amount = restAmount
|
||||
return (splitCid, restCid)
|
||||
|
||||
-- Merge two IOUs by aggregating their amounts.
|
||||
Iou_Merge : IouCid
|
||||
with
|
||||
otherCid: IouCid
|
||||
do
|
||||
otherIou <- fetch otherCid
|
||||
-- Check the two IOU's are compatible
|
||||
assert (
|
||||
currency == otherIou.currency &&
|
||||
owner == otherIou.owner &&
|
||||
issuer == otherIou.issuer
|
||||
)
|
||||
-- Retire the old Iou
|
||||
archive otherCid
|
||||
-- Return the merged Iou
|
||||
create this with amount = amount + otherIou.amount
|
||||
|
||||
Iou_Transfer : ContractId IouTransfer
|
||||
with
|
||||
newOwner : Party
|
||||
do create IouTransfer with iou = this; newOwner
|
||||
|
||||
Iou_AddObserver : IouCid
|
||||
with
|
||||
newObserver : Party
|
||||
do create this with observers = newObserver :: observers
|
||||
|
||||
Iou_RemoveObserver : IouCid
|
||||
with
|
||||
oldObserver : Party
|
||||
do create this with observers = filter (/= oldObserver) observers
|
||||
|
||||
template IouTransfer
|
||||
with
|
||||
iou : Iou
|
||||
newOwner : Party
|
||||
where
|
||||
signatory iou.issuer, iou.owner
|
||||
|
||||
controller iou.owner can
|
||||
IouTransfer_Cancel : IouCid
|
||||
do create iou
|
||||
|
||||
controller newOwner can
|
||||
IouTransfer_Reject : IouCid
|
||||
do create iou
|
||||
|
||||
IouTransfer_Accept : IouCid
|
||||
do
|
||||
create iou with
|
||||
owner = newOwner
|
||||
observers = []
|
||||
49
compiler/daml-lf-verify/daml/quickstart/daml/IouTrade.daml
Normal file
49
compiler/daml-lf-verify/daml/quickstart/daml/IouTrade.daml
Normal file
@ -0,0 +1,49 @@
|
||||
-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
|
||||
module IouTrade where
|
||||
|
||||
import DA.Assert
|
||||
|
||||
import Iou
|
||||
|
||||
template IouTrade
|
||||
with
|
||||
buyer : Party
|
||||
seller : Party
|
||||
baseIouCid : IouCid
|
||||
baseIssuer : Party
|
||||
baseCurrency : Text
|
||||
baseAmount : Decimal
|
||||
quoteIssuer : Party
|
||||
quoteCurrency : Text
|
||||
quoteAmount : Decimal
|
||||
where
|
||||
signatory buyer
|
||||
|
||||
controller seller can
|
||||
IouTrade_Accept : (IouCid, IouCid)
|
||||
with
|
||||
quoteIouCid : IouCid
|
||||
do
|
||||
baseIou <- fetch baseIouCid
|
||||
baseIssuer === baseIou.issuer
|
||||
baseCurrency === baseIou.currency
|
||||
baseAmount === baseIou.amount
|
||||
buyer === baseIou.owner
|
||||
quoteIou <- fetch quoteIouCid
|
||||
quoteIssuer === quoteIou.issuer
|
||||
quoteCurrency === quoteIou.currency
|
||||
quoteAmount === quoteIou.amount
|
||||
seller === quoteIou.owner
|
||||
quoteIouTransferCid <- exercise quoteIouCid Iou_Transfer with
|
||||
newOwner = buyer
|
||||
transferredQuoteIouCid <- exercise quoteIouTransferCid IouTransfer_Accept
|
||||
baseIouTransferCid <- exercise baseIouCid Iou_Transfer with
|
||||
newOwner = seller
|
||||
transferredBaseIouCid <- exercise baseIouTransferCid IouTransfer_Accept
|
||||
return (transferredQuoteIouCid, transferredBaseIouCid)
|
||||
|
||||
TradeProposal_Reject : ()
|
||||
do return ()
|
||||
140
compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs
Normal file
140
compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs
Normal file
@ -0,0 +1,140 @@
|
||||
-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
|
||||
-- | Static verification of DAML packages.
|
||||
module DA.Daml.LF.Verify
|
||||
( main
|
||||
, verify
|
||||
) where
|
||||
|
||||
import Data.Maybe
|
||||
import qualified Data.NameMap as NM
|
||||
import qualified Data.Text as T
|
||||
import Data.Text.Prettyprint.Doc
|
||||
import Data.Text.Prettyprint.Doc.Render.String
|
||||
import Options.Applicative
|
||||
import System.Exit
|
||||
import System.IO
|
||||
|
||||
import DA.Daml.LF.Ast.Base
|
||||
import DA.Daml.LF.Verify.Generate
|
||||
import DA.Daml.LF.Verify.Solve
|
||||
import DA.Daml.LF.Verify.Read
|
||||
import DA.Daml.LF.Verify.Context
|
||||
import DA.Bazel.Runfiles
|
||||
|
||||
getSolver :: IO FilePath
|
||||
getSolver = locateRunfiles "z3_nix/bin/z3"
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
Options{..} <- execParser optionsParserInfo
|
||||
let choiceTmpl = TypeConName [T.pack optChoiceTmpl]
|
||||
choiceName = ChoiceName (T.pack optChoiceName)
|
||||
fieldTmpl = TypeConName [T.pack optFieldTmpl]
|
||||
fieldName = FieldName (T.pack optFieldName)
|
||||
result <- verify optInputDar putStrLn choiceTmpl choiceName fieldTmpl fieldName
|
||||
print result
|
||||
|
||||
outputError :: Error
|
||||
-- ^ The error message.
|
||||
-> String
|
||||
-- ^ An additional message providing context.
|
||||
-> IO a
|
||||
outputError err msg = do
|
||||
hPutStrLn stderr msg
|
||||
hPrint stderr err
|
||||
exitFailure
|
||||
|
||||
-- | Execute the full verification pipeline.
|
||||
verify :: FilePath
|
||||
-- ^ The DAR file to load.
|
||||
-> (String -> IO ())
|
||||
-- ^ Function for debugging printouts.
|
||||
-> TypeConName
|
||||
-- ^ The template in which the given choice is defined.
|
||||
-> ChoiceName
|
||||
-- ^ The choice to be verified.
|
||||
-> TypeConName
|
||||
-- ^ The template in which the given field is defined.
|
||||
-> FieldName
|
||||
-- ^ The field to be verified.
|
||||
-> IO Result
|
||||
verify dar debug choiceTmplName choiceName fieldTmplName fieldName = do
|
||||
-- Read the packages to analyse, and initialise the provided solver.
|
||||
pkgs <- readPackages [dar]
|
||||
solver <- getSolver
|
||||
-- Find the given template names in the packages.
|
||||
choiceTmpl <- findTemplate pkgs choiceTmplName
|
||||
fieldTmpl <- findTemplate pkgs fieldTmplName
|
||||
-- Start reading data type and value definitions. References to other
|
||||
-- values are just stored as references at this point.
|
||||
debug "Start value gathering"
|
||||
case runEnv (genPackages pkgs) (emptyEnv :: Env 'ValueGathering) of
|
||||
Left err-> outputError err "Value phase finished with error: "
|
||||
Right env1 -> do
|
||||
-- All value definitions have been handled. Start computing closures of
|
||||
-- the stored value references. After this phase, all value references
|
||||
-- should be inlined.
|
||||
debug "Start value solving"
|
||||
let env2 = solveValueReferences env1
|
||||
-- Start reading template definitions. References to choices are just
|
||||
-- stored as references at this point.
|
||||
debug "Start choice gathering"
|
||||
case runEnv (genPackages pkgs) env2 of
|
||||
Left err -> outputError err "Choice phase finished with error: "
|
||||
Right env3 -> do
|
||||
-- All choice definitions have been handled. Start computing closures
|
||||
-- of the stored choice references. After this phase, all choice
|
||||
-- references should be inlined.
|
||||
debug "Start choice solving"
|
||||
let env4 = solveChoiceReferences env3
|
||||
-- Construct the actual constraints to be solved by the SMT solver.
|
||||
debug "Start constraint solving phase"
|
||||
let cset = constructConstr env4 choiceTmpl choiceName fieldTmpl fieldName
|
||||
debug $ renderString $ layoutCompact ("Create: " <+> pretty (_cCres cset))
|
||||
debug $ renderString $ layoutCompact ("Archive: " <+> pretty (_cArcs cset))
|
||||
-- Pass the constraints to the SMT solver.
|
||||
solveConstr solver debug cset
|
||||
where
|
||||
-- | Lookup the first package that defines the given template. This avoids
|
||||
-- having to pass in the package reference manually when using the tool.
|
||||
findTemplate :: [(PackageId, (Package, Maybe PackageName))]
|
||||
-- ^ The package from the DAR file.
|
||||
-> TypeConName
|
||||
-- ^ The template name.
|
||||
-> IO (Qualified TypeConName)
|
||||
findTemplate pkgs tem = maybe
|
||||
(outputError (UnknownTmpl tem) "Parsing phase finished with error: ")
|
||||
(\(pacid, mod) -> return $ Qualified (PRImport pacid) mod tem)
|
||||
(listToMaybe $ mapMaybe (templateInPackage tem) pkgs)
|
||||
|
||||
-- | Return the package id and the name of the module containing the given
|
||||
-- template, if it exists.
|
||||
templateInPackage :: TypeConName
|
||||
-- ^ The template to look for.
|
||||
-> (PackageId, (Package, Maybe PackageName))
|
||||
-- ^ The package to look in.
|
||||
-> Maybe (PackageId, ModuleName)
|
||||
templateInPackage tem (id, (pac,_)) =
|
||||
case templateInModules tem $ NM.toList $ packageModules pac of
|
||||
Nothing -> Nothing
|
||||
Just mod -> Just (id, mod)
|
||||
|
||||
-- | Return the name of the module containing the given template, if it
|
||||
-- exists.
|
||||
templateInModules :: TypeConName
|
||||
-- ^ The template to look for.
|
||||
-> [Module]
|
||||
-- ^ The modules to look in.
|
||||
-> Maybe ModuleName
|
||||
templateInModules tem mods =
|
||||
listToMaybe $
|
||||
mapMaybe ( \Module{..} ->
|
||||
let tmpls = NM.toList moduleTemplates
|
||||
in if not (any (\Template{..} -> tplTypeCon == tem) tmpls)
|
||||
then Nothing
|
||||
else Just moduleName )
|
||||
mods
|
||||
900
compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Context.hs
Normal file
900
compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Context.hs
Normal file
@ -0,0 +1,900 @@
|
||||
-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
-- | Contexts for DAML LF static verification
|
||||
module DA.Daml.LF.Verify.Context
|
||||
( Phase(..)
|
||||
, GenPhase
|
||||
, BoolExpr(..)
|
||||
, Cond(..)
|
||||
, Env(..)
|
||||
, Error(..)
|
||||
, MonadEnv
|
||||
, UpdateSet(..)
|
||||
, Upd(..)
|
||||
, ChoiceData(..)
|
||||
, UpdChoice(..)
|
||||
, Skolem(..)
|
||||
, getEnv
|
||||
, runEnv
|
||||
, genRenamedVar
|
||||
, emptyEnv
|
||||
, extVarEnv, extRecEnv, extValEnv, extChEnv, extDatsEnv, extCidEnv, extCtrRec
|
||||
, extRecEnvLvl1
|
||||
, lookupVar, lookupRec, lookupVal, lookupChoice, lookupDataCon, lookupCid
|
||||
, concatEnv
|
||||
, emptyUpdateSet
|
||||
, concatUpdateSet
|
||||
, addUpd
|
||||
, conditionalUpdateSet
|
||||
, solveValueReferences
|
||||
, solveChoiceReferences
|
||||
, fieldName2VarName
|
||||
, recTypConFields, recTypFields, recExpFields
|
||||
) where
|
||||
|
||||
import Control.Monad.Error.Class (MonadError (..), throwError)
|
||||
import Control.Monad.State.Lazy
|
||||
import Data.Hashable
|
||||
import GHC.Generics
|
||||
import Data.Maybe (isJust, fromMaybe)
|
||||
import Data.List (find)
|
||||
import Data.Bifunctor
|
||||
import qualified Data.HashMap.Strict as HM
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
|
||||
import DA.Daml.LF.Ast hiding (lookupChoice)
|
||||
import DA.Daml.LF.Verify.Subst
|
||||
|
||||
-- TODO: Move these data types to a seperate file?
|
||||
-- | Data type denoting the phase of the constraint generator.
|
||||
data Phase
|
||||
= ValueGathering
|
||||
-- ^ The value phase gathers all value and data type definitions across modules.
|
||||
| ChoiceGathering
|
||||
-- ^ The choice phase gathers the updates performed in choice definitions.
|
||||
| Solving
|
||||
-- ^ During the solving phase, all definitions have been loaded and updates
|
||||
-- have been inlined.
|
||||
|
||||
-- | Data type denoting a boolean condition expression. This data type was
|
||||
-- introduced as DAML-LF does not have build-in boolean operators, and using
|
||||
-- prelude functions gets messy.
|
||||
data BoolExpr
|
||||
= BExpr Expr
|
||||
-- ^ A daml-lf expression.
|
||||
| BAnd BoolExpr BoolExpr
|
||||
-- ^ And operator.
|
||||
| BNot BoolExpr
|
||||
-- ^ Not operator.
|
||||
deriving Show
|
||||
|
||||
-- | Data type denoting a potentially conditional value.
|
||||
data Cond a
|
||||
= Determined a
|
||||
-- ^ Non-conditional value.
|
||||
| Conditional BoolExpr [Cond a] [Cond a]
|
||||
-- ^ Conditional value, with a (Boolean) condition, at least one value in case
|
||||
-- the condition holds, and at least one value in case it doesn't.
|
||||
-- Note that these branch lists should not be empty.
|
||||
-- TODO: Encode this invariant in the type system?
|
||||
deriving (Show, Functor)
|
||||
|
||||
-- | Construct a simple conditional.
|
||||
createCond :: BoolExpr
|
||||
-- ^ The condition to depend on.
|
||||
-> a
|
||||
-- ^ The value in case the condition holds.
|
||||
-> a
|
||||
-- ^ The value in case the condition does not hold.
|
||||
-> Cond a
|
||||
createCond cond x y = Conditional cond [Determined x] [Determined y]
|
||||
|
||||
-- | Shift the conditional inside the update set.
|
||||
introCond :: Cond (UpdateSet ph) -> UpdateSet ph
|
||||
introCond (Determined upds) = upds
|
||||
introCond (Conditional e updx updy) = case getPhase updx of
|
||||
UpdateSetVG{} -> UpdateSetVG
|
||||
(buildCond updx updy _usvgUpdate)
|
||||
(buildCond updx updy _usvgChoice)
|
||||
(buildCond updx updy _usvgValue)
|
||||
UpdateSetCG{} -> UpdateSetCG
|
||||
(buildCond updx updy _uscgUpdate)
|
||||
(buildCond updx updy _uscgChoice)
|
||||
UpdateSetS{} -> UpdateSetS
|
||||
(buildCond updx updy _ussUpdate)
|
||||
where
|
||||
-- | Construct a single conditional, if the input is not empty.
|
||||
buildCond :: [Cond (UpdateSet ph)]
|
||||
-- ^ The input for the true case.
|
||||
-> [Cond (UpdateSet ph)]
|
||||
-- ^ The input for the false case.
|
||||
-> (UpdateSet ph -> [Cond a])
|
||||
-- ^ The fetch function.
|
||||
-> [Cond a]
|
||||
buildCond updx updy get =
|
||||
let xs = concatCond updx get
|
||||
ys = concatCond updy get
|
||||
in [Conditional e xs ys | not (null xs && null ys)]
|
||||
|
||||
-- TODO: Temporary solution. Make introCond a part of the GenPhase class instead.
|
||||
getPhase :: [Cond (UpdateSet ph)] -> UpdateSet ph
|
||||
getPhase lst = case head lst of
|
||||
Determined upds -> upds
|
||||
Conditional _ xs _ -> getPhase xs
|
||||
|
||||
-- | Fetch the conditionals from the conditional update set, and flatten the
|
||||
-- two layers into one.
|
||||
concatCond :: [Cond (UpdateSet ph)]
|
||||
-- ^ The conditional update set to fetch from.
|
||||
-> (UpdateSet ph -> [Cond a])
|
||||
-- ^ The fetch function.
|
||||
-> [Cond a]
|
||||
concatCond upds get =
|
||||
let upds' = map introCond upds
|
||||
in concatMap get upds'
|
||||
|
||||
-- | Data type denoting an update.
|
||||
data Upd
|
||||
= UpdCreate
|
||||
-- ^ Data type denoting a create update.
|
||||
{ _creTemp :: !(Qualified TypeConName)
|
||||
-- ^ Qualified type constructor corresponding to the contract template.
|
||||
, _creField :: ![(FieldName, Expr)]
|
||||
-- ^ The fields to be verified, together with their value.
|
||||
}
|
||||
| UpdArchive
|
||||
-- ^ Data type denoting an archive update.
|
||||
{ _arcTemp :: !(Qualified TypeConName)
|
||||
-- ^ Qualified type constructor corresponding to the contract template.
|
||||
, _arcField :: ![(FieldName, Expr)]
|
||||
-- ^ The fields to be verified, together with their value.
|
||||
}
|
||||
deriving Show
|
||||
|
||||
-- | Data type denoting an exercised choice.
|
||||
data UpdChoice = UpdChoice
|
||||
{ _choTemp :: !(Qualified TypeConName)
|
||||
-- ^ Qualified type constructor corresponding to the contract template.
|
||||
, _choName :: !ChoiceName
|
||||
-- ^ The name of the choice.
|
||||
}
|
||||
deriving (Eq, Generic, Hashable, Show)
|
||||
|
||||
-- | The collection of updates being performed.
|
||||
data UpdateSet (ph :: Phase) where
|
||||
UpdateSetVG ::
|
||||
{ _usvgUpdate :: ![Cond Upd]
|
||||
-- ^ The list of updates.
|
||||
, _usvgChoice :: ![Cond UpdChoice]
|
||||
-- ^ The list of exercised choices.
|
||||
, _usvgValue :: ![Cond (Qualified ExprValName)]
|
||||
-- ^ The list of referenced values.
|
||||
} -> UpdateSet 'ValueGathering
|
||||
UpdateSetCG ::
|
||||
{ _uscgUpdate :: ![Cond Upd]
|
||||
-- ^ The list of updates.
|
||||
, _uscgChoice :: ![Cond UpdChoice]
|
||||
-- ^ The list of exercised choices.
|
||||
} -> UpdateSet 'ChoiceGathering
|
||||
UpdateSetS ::
|
||||
{ _ussUpdate :: ![Cond Upd]
|
||||
-- ^ The list of updates.
|
||||
} -> UpdateSet 'Solving
|
||||
|
||||
class GenPhase ph where
|
||||
emptyUpdateSet :: UpdateSet ph
|
||||
emptyEnv :: Env ph
|
||||
|
||||
instance GenPhase 'ValueGathering where
|
||||
emptyUpdateSet = UpdateSetVG [] [] []
|
||||
emptyEnv = EnvVG [] HM.empty HM.empty HM.empty []
|
||||
|
||||
instance GenPhase 'ChoiceGathering where
|
||||
emptyUpdateSet = UpdateSetCG [] []
|
||||
emptyEnv = EnvCG [] HM.empty HM.empty HM.empty [] HM.empty
|
||||
|
||||
instance GenPhase 'Solving where
|
||||
emptyUpdateSet = UpdateSetS []
|
||||
emptyEnv = EnvS [] HM.empty HM.empty HM.empty [] HM.empty
|
||||
|
||||
-- | Combine two update sets.
|
||||
concatUpdateSet :: UpdateSet ph
|
||||
-- ^ The first update set to be combined.
|
||||
-> UpdateSet ph
|
||||
-- ^ The second update set to be combined.
|
||||
-> UpdateSet ph
|
||||
concatUpdateSet (UpdateSetVG upd1 cho1 val1) (UpdateSetVG upd2 cho2 val2) =
|
||||
UpdateSetVG (upd1 ++ upd2) (cho1 ++ cho2) (val1 ++ val2)
|
||||
concatUpdateSet (UpdateSetCG upd1 cho1) (UpdateSetCG upd2 cho2) =
|
||||
UpdateSetCG (upd1 ++ upd2) (cho1 ++ cho2)
|
||||
concatUpdateSet (UpdateSetS upd1) (UpdateSetS upd2) =
|
||||
UpdateSetS (upd1 ++ upd2)
|
||||
|
||||
-- | Add a single Upd to an UpdateSet
|
||||
addUpd :: UpdateSet ph
|
||||
-- ^ The update set to extend.
|
||||
-> Upd
|
||||
-- ^ The update to add.
|
||||
-> UpdateSet ph
|
||||
addUpd upds@UpdateSetVG{..} upd = upds{_usvgUpdate = Determined upd : _usvgUpdate}
|
||||
addUpd upds@UpdateSetCG{..} upd = upds{_uscgUpdate = Determined upd : _uscgUpdate}
|
||||
addUpd upds@UpdateSetS{..} upd = upds{_ussUpdate = Determined upd : _ussUpdate}
|
||||
|
||||
-- | Make an update set conditional. A second update set can also be introduced
|
||||
-- for the case where the condition does not hold.
|
||||
conditionalUpdateSet :: Expr
|
||||
-- ^ The condition on which to combine the two update sets.
|
||||
-> UpdateSet ph
|
||||
-- ^ The update set in case the condition holds.
|
||||
-> UpdateSet ph
|
||||
-- ^ The update set in case the condition does not hold.
|
||||
-> UpdateSet ph
|
||||
conditionalUpdateSet exp upd1 upd2 =
|
||||
introCond $ createCond (BExpr exp) upd1 upd2
|
||||
|
||||
-- | Refresh a given expression variable by producing a fresh renamed variable.
|
||||
-- TODO: when a renamed var gets renamed again, it might overlap again.
|
||||
-- We should have an additional field in VarName to denote its number.
|
||||
genRenamedVar :: MonadEnv m ph
|
||||
=> ExprVarName
|
||||
-- ^ The variable to be renamed.
|
||||
-> m ExprVarName
|
||||
genRenamedVar (ExprVarName x) = ExprVarName . T.append x . T.pack <$> fresh
|
||||
|
||||
-- | Data type denoting a skolemized variable.
|
||||
data Skolem
|
||||
= SkolVar ExprVarName
|
||||
-- ^ Skolemised term variable.
|
||||
| SkolRec ExprVarName [FieldName]
|
||||
-- ^ List of skolemised field names, with their variable.
|
||||
-- e.g. `this.field`
|
||||
deriving (Eq, Show)
|
||||
|
||||
-- | Data type denoting a contract id.
|
||||
data Cid
|
||||
= CidVar ExprVarName
|
||||
-- ^ An expression variable denoting a contract id.
|
||||
| CidRec ExprVarName FieldName
|
||||
-- ^ A record projection denoting a contract id.
|
||||
deriving (Generic, Hashable, Eq, Show)
|
||||
|
||||
-- | Convert an expression to a contract id, if possible.
|
||||
expr2cid :: MonadEnv m ph
|
||||
=> Expr
|
||||
-- ^ The expression to be converted.
|
||||
-> m Cid
|
||||
expr2cid (EVar x) = return $ CidVar x
|
||||
expr2cid (ERecProj _ f (EVar x)) = return $ CidRec x f
|
||||
expr2cid (EStructProj f (EVar x)) = return $ CidRec x f
|
||||
expr2cid _ = throwError ExpectCid
|
||||
|
||||
-- | Data type containing the data stored for a choice definition.
|
||||
data ChoiceData (ph :: Phase) = ChoiceData
|
||||
{ _cdSelf :: ExprVarName
|
||||
-- ^ The variable denoting `self`.
|
||||
, _cdThis :: ExprVarName
|
||||
-- ^ The variable denoting `this`.
|
||||
, _cdArgs :: ExprVarName
|
||||
-- ^ The variable denoting `args`.
|
||||
, _cdUpds :: Expr -> Expr -> Expr -> UpdateSet ph
|
||||
-- ^ Function from self, this and args to the updates performed by this choice.
|
||||
, _cdType :: Type
|
||||
-- ^ The return type of this choice.
|
||||
}
|
||||
|
||||
-- TODO: Could we alternatively just declare the variables that occur in the updates and drop the skolems?
|
||||
-- | The environment for the DAML-LF verifier
|
||||
data Env (ph :: Phase) where
|
||||
EnvVG ::
|
||||
{ _envvgskol :: ![Skolem]
|
||||
-- ^ The skolemised term variables and fields.
|
||||
, _envvgvals :: !(HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ValueGathering))
|
||||
-- ^ The bound values.
|
||||
, _envvgdats :: !(HM.HashMap TypeConName DefDataType)
|
||||
-- ^ The set of data constructors.
|
||||
, _envvgcids :: !(HM.HashMap Cid (ExprVarName, [ExprVarName]))
|
||||
-- ^ The set of fetched cid's mapped to their current variable name, along
|
||||
-- with a list of any potential old variable names.
|
||||
, _envvgctrs :: ![(Expr, Expr)]
|
||||
-- ^ Additional equality constraints.
|
||||
} -> Env 'ValueGathering
|
||||
EnvCG ::
|
||||
{ _envcgskol :: ![Skolem]
|
||||
-- ^ The skolemised term variables and fields.
|
||||
, _envcgvals :: !(HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ChoiceGathering))
|
||||
-- ^ The bound values.
|
||||
, _envcgdats :: !(HM.HashMap TypeConName DefDataType)
|
||||
-- ^ The set of data constructors.
|
||||
, _envcgcids :: !(HM.HashMap Cid (ExprVarName, [ExprVarName]))
|
||||
-- ^ The set of fetched cid's mapped to their current variable name, along
|
||||
-- with a list of any potential old variable names.
|
||||
, _envcgctrs :: ![(Expr, Expr)]
|
||||
-- ^ Additional equality constraints.
|
||||
, _envcgchs :: !(HM.HashMap UpdChoice (ChoiceData 'ChoiceGathering))
|
||||
-- ^ The set of relevant choices.
|
||||
} -> Env 'ChoiceGathering
|
||||
EnvS ::
|
||||
{ _envsskol :: ![Skolem]
|
||||
-- ^ The skolemised term variables and fields.
|
||||
, _envsvals :: !(HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'Solving))
|
||||
-- ^ The bound values.
|
||||
, _envsdats :: !(HM.HashMap TypeConName DefDataType)
|
||||
-- ^ The set of data constructors.
|
||||
, _envscids :: !(HM.HashMap Cid (ExprVarName, [ExprVarName]))
|
||||
-- ^ The set of fetched cid's mapped to their current variable name, along
|
||||
-- with a list of any potential old variable names.
|
||||
, _envsctrs :: ![(Expr, Expr)]
|
||||
-- ^ Additional equality constraints.
|
||||
, _envschs :: !(HM.HashMap UpdChoice (ChoiceData 'Solving))
|
||||
-- ^ The set of relevant choices.
|
||||
} -> Env 'Solving
|
||||
|
||||
-- | Combine two environments.
|
||||
concatEnv :: Env ph
|
||||
-- ^ The first environment to be combined.
|
||||
-> Env ph
|
||||
-- ^ The second environment to be combined.
|
||||
-> Env ph
|
||||
concatEnv (EnvVG vars1 vals1 dats1 cids1 ctrs1) (EnvVG vars2 vals2 dats2 cids2 ctrs2) =
|
||||
EnvVG (vars1 ++ vars2) (vals1 `HM.union` vals2) (dats1 `HM.union` dats2)
|
||||
(cids1 `HM.union` cids2) (ctrs1 ++ ctrs2)
|
||||
concatEnv (EnvCG vars1 vals1 dats1 cids1 ctrs1 chos1) (EnvCG vars2 vals2 dats2 cids2 ctrs2 chos2) =
|
||||
EnvCG (vars1 ++ vars2) (vals1 `HM.union` vals2) (dats1 `HM.union` dats2)
|
||||
(cids1 `HM.union` cids2) (ctrs1 ++ ctrs2) (chos1 `HM.union` chos2)
|
||||
concatEnv (EnvS vars1 vals1 dats1 cids1 ctrs1 chos1) (EnvS vars2 vals2 dats2 cids2 ctrs2 chos2) =
|
||||
EnvS (vars1 ++ vars2) (vals1 `HM.union` vals2) (dats1 `HM.union` dats2)
|
||||
(cids1 `HM.union` cids2) (ctrs1 ++ ctrs2) (chos1 `HM.union` chos2)
|
||||
-- TODO: union makes me slightly nervous, as it allows overlapping keys
|
||||
-- (and just uses the first). `unionWith concatUpdateSet` would indeed be better,
|
||||
-- but this still makes me nervous as the expr and exprvarnames wouldn't be merged.
|
||||
|
||||
-- | Convert a fieldname into an expression variable name.
|
||||
fieldName2VarName :: FieldName -> ExprVarName
|
||||
fieldName2VarName = ExprVarName . unFieldName
|
||||
|
||||
-- | Type class constraint with the required monadic effects for functions
|
||||
-- manipulating the verification environment.
|
||||
type MonadEnv m ph = (MonadError Error m, MonadState (Int,Env ph) m)
|
||||
|
||||
-- | Fetch the current environment.
|
||||
getEnv :: MonadEnv m ph => m (Env ph)
|
||||
getEnv = snd <$> get
|
||||
|
||||
-- | Set the current environment.
|
||||
putEnv :: MonadEnv m ph => Env ph -> m ()
|
||||
putEnv env = get >>= \(uni,_) -> put (uni,env)
|
||||
|
||||
-- | Generate a new unique name.
|
||||
fresh :: MonadEnv m ph => m String
|
||||
fresh = do
|
||||
(cur,env) <- get
|
||||
put (cur + 1,env)
|
||||
return $ show cur
|
||||
|
||||
-- | Evaluate the MonadEnv to produce an error message or the final environment.
|
||||
runEnv :: StateT (Int, Env ph) (Either Error) ()
|
||||
-- ^ The monadic computation to be evaluated.
|
||||
-> Env ph
|
||||
-- ^ The initial environment to start from.
|
||||
-> Either Error (Env ph)
|
||||
runEnv comp env0 = do
|
||||
(_res, (_uni,env1)) <- runStateT comp (0,env0)
|
||||
return env1
|
||||
|
||||
-- | Skolemise an expression variable and extend the environment.
|
||||
extVarEnv :: MonadEnv m ph
|
||||
=> ExprVarName
|
||||
-- ^ The expression variable to be skolemised.
|
||||
-> m ()
|
||||
extVarEnv x = extSkolEnv (SkolVar x)
|
||||
|
||||
-- | Skolemise a list of record projection and extend the environment.
|
||||
extRecEnv :: MonadEnv m ph
|
||||
=> ExprVarName
|
||||
-- ^ The variable on which is being projected.
|
||||
-> [FieldName]
|
||||
-- ^ The fields which should be skolemised.
|
||||
-> m ()
|
||||
extRecEnv x fs = extSkolEnv (SkolRec x fs)
|
||||
|
||||
-- | Extend the environment with a new skolem variable.
|
||||
extSkolEnv :: MonadEnv m ph
|
||||
=> Skolem
|
||||
-- ^ The skolem variable to add.
|
||||
-> m ()
|
||||
extSkolEnv skol = getEnv >>= \case
|
||||
env@EnvVG{..} -> putEnv env{_envvgskol = skol : _envvgskol}
|
||||
env@EnvCG{..} -> putEnv env{_envcgskol = skol : _envcgskol}
|
||||
env@EnvS{..} -> putEnv env{_envsskol = skol : _envsskol}
|
||||
|
||||
-- | Extend the environment with a new value definition.
|
||||
extValEnv :: MonadEnv m ph
|
||||
=> Qualified ExprValName
|
||||
-- ^ The name of the value being defined.
|
||||
-> Expr
|
||||
-- ^ The (partially) evaluated value definition.
|
||||
-> UpdateSet ph
|
||||
-- ^ The updates performed by this value.
|
||||
-> m ()
|
||||
extValEnv val expr upd = getEnv >>= \case
|
||||
env@EnvVG{..} -> putEnv env{_envvgvals = HM.insert val (expr, upd) _envvgvals}
|
||||
env@EnvCG{..} -> putEnv env{_envcgvals = HM.insert val (expr, upd) _envcgvals}
|
||||
env@EnvS{..} -> putEnv env{_envsvals = HM.insert val (expr, upd) _envsvals}
|
||||
|
||||
-- | Extends the environment with a new choice.
|
||||
extChEnv :: MonadEnv m ph
|
||||
=> Qualified TypeConName
|
||||
-- ^ The type of the template on which this choice is defined.
|
||||
-> ChoiceName
|
||||
-- ^ The name of the new choice.
|
||||
-> ExprVarName
|
||||
-- ^ Variable to bind the ContractId on which this choice is exercised on to.
|
||||
-> ExprVarName
|
||||
-- ^ Variable to bind the contract on which this choice is exercised on to.
|
||||
-> ExprVarName
|
||||
-- ^ Variable to bind the choice argument to.
|
||||
-> UpdateSet ph
|
||||
-- ^ The updates performed by the new choice.
|
||||
-> Type
|
||||
-- ^ The result type of the new choice.
|
||||
-> m ()
|
||||
extChEnv tc ch self this arg upd typ =
|
||||
let substUpd sExp tExp aExp = substituteTm (createExprSubst [(self,sExp),(this,tExp),(arg,aExp)]) upd
|
||||
in getEnv >>= \case
|
||||
EnvVG{} -> error "Impossible: extChEnv is not used in the value gathering phase"
|
||||
env@EnvCG{..} -> putEnv env{_envcgchs = HM.insert (UpdChoice tc ch) (ChoiceData self this arg substUpd typ) _envcgchs}
|
||||
env@EnvS{..} -> putEnv env{_envschs = HM.insert (UpdChoice tc ch) (ChoiceData self this arg substUpd typ) _envschs}
|
||||
|
||||
-- | Extend the environment with a list of new data type definitions.
|
||||
extDatsEnv :: MonadEnv m ph
|
||||
=> HM.HashMap TypeConName DefDataType
|
||||
-- ^ A hashmap of the data constructor names, with their corresponding definitions.
|
||||
-> m ()
|
||||
extDatsEnv hmap = getEnv >>= \case
|
||||
env@EnvVG{..} -> putEnv env{_envvgdats = hmap `HM.union` _envvgdats}
|
||||
env@EnvCG{..} -> putEnv env{_envcgdats = hmap `HM.union` _envcgdats}
|
||||
env@EnvS{..} -> putEnv env{_envsdats = hmap `HM.union` _envsdats}
|
||||
|
||||
-- | Extend the environment with a new contract id, and the variable to which
|
||||
-- the fetched contract is bound.
|
||||
extCidEnv :: MonadEnv m ph
|
||||
=> Expr
|
||||
-- ^ The contract id expression.
|
||||
-> ExprVarName
|
||||
-- ^ The variable name to which the fetched contract is bound.
|
||||
-> m ()
|
||||
extCidEnv exp var = do
|
||||
prev <- do
|
||||
{ (cur, old) <- lookupCid exp
|
||||
; return $ cur : old }
|
||||
`catchError` (\_ -> return [])
|
||||
cid <- expr2cid exp
|
||||
let new = (var, prev)
|
||||
getEnv >>= \case
|
||||
env@EnvVG{..} -> putEnv env{_envvgcids = HM.insert cid new _envvgcids}
|
||||
env@EnvCG{..} -> putEnv env{_envcgcids = HM.insert cid new _envcgcids}
|
||||
env@EnvS{..} -> putEnv env{_envscids = HM.insert cid new _envscids}
|
||||
|
||||
-- | Extend the environment with additional equality constraints, between a
|
||||
-- variable and its field values.
|
||||
extCtrRec :: MonadEnv m ph
|
||||
=> ExprVarName
|
||||
-- ^ The variable to be asserted.
|
||||
-> [(FieldName, Expr)]
|
||||
-- ^ The fields with their values.
|
||||
-> m ()
|
||||
extCtrRec var fields = do
|
||||
let ctrs = map (\(f, e) -> (EStructProj f (EVar var), e)) fields
|
||||
getEnv >>= \case
|
||||
env@EnvVG{..} -> putEnv env{_envvgctrs = ctrs ++ _envvgctrs}
|
||||
env@EnvCG{..} -> putEnv env{_envcgctrs = ctrs ++ _envcgctrs}
|
||||
env@EnvS{..} -> putEnv env{_envsctrs = ctrs ++ _envsctrs}
|
||||
|
||||
-- TODO: Is one layer of recursion enough?
|
||||
-- | Recursively skolemise the given record fields, when they have a record
|
||||
-- type. Note that this only works 1 level deep.
|
||||
extRecEnvLvl1 :: MonadEnv m ph
|
||||
=> [(FieldName, Type)]
|
||||
-- ^ The record fields to skolemise, together with their types.
|
||||
-> m ()
|
||||
extRecEnvLvl1 = mapM_ step
|
||||
where
|
||||
step :: MonadEnv m ph => (FieldName, Type) -> m ()
|
||||
step (f,typ) = do
|
||||
{ fsRec <- recTypFields typ
|
||||
; extRecEnv (fieldName2VarName f) fsRec
|
||||
}
|
||||
-- TODO: Temporary fix
|
||||
`catchError` (\_ -> return ())
|
||||
|
||||
-- | Lookup an expression variable in the environment. Returns `True` if this variable
|
||||
-- has been skolemised, or `False` otherwise.
|
||||
lookupVar :: MonadEnv m ph
|
||||
=> ExprVarName
|
||||
-- ^ The expression variable to look up.
|
||||
-> m Bool
|
||||
lookupVar x = getEnv >>= \case
|
||||
EnvVG{..} -> return $ elem (SkolVar x) _envvgskol
|
||||
EnvCG{..} -> return $ elem (SkolVar x) _envcgskol
|
||||
EnvS{..} -> return $ elem (SkolVar x) _envsskol
|
||||
|
||||
-- | Lookup a record project in the environment. Returns a boolean denoting
|
||||
-- whether or not the record projection has been skolemised.
|
||||
lookupRec :: MonadEnv m ph
|
||||
=> ExprVarName
|
||||
-- ^ The expression variable on which is being projected.
|
||||
-> FieldName
|
||||
-- ^ The field name which is being projected.
|
||||
-> m Bool
|
||||
lookupRec x f = do
|
||||
skols <- getEnv >>= \case
|
||||
EnvVG{..} -> return _envvgskol
|
||||
EnvCG{..} -> return _envcgskol
|
||||
EnvS{..} -> return _envsskol
|
||||
let fields = [ fs | SkolRec y fs <- skols, x == y ]
|
||||
if not (null fields)
|
||||
then return (elem f $ head fields)
|
||||
else return False
|
||||
|
||||
-- | Lookup a value name in the environment. Returns its (partially) evaluated
|
||||
-- definition, together with the updates it performs.
|
||||
lookupVal :: MonadEnv m ph
|
||||
=> Qualified ExprValName
|
||||
-- ^ The value name to lookup.
|
||||
-> m (Expr, UpdateSet ph)
|
||||
lookupVal val = do
|
||||
vals <- getEnv >>= \case
|
||||
EnvVG{..} -> return _envvgvals
|
||||
EnvCG{..} -> return _envcgvals
|
||||
EnvS{..} -> return _envsvals
|
||||
case HM.lookup val vals of
|
||||
Just res -> return res
|
||||
Nothing -> throwError (UnknownValue val)
|
||||
|
||||
-- | Lookup a choice name in the environment. Returns a function which, once
|
||||
-- self, this and args have been instantiated, returns the set of updates it
|
||||
-- performs. Also returns the return type of the choice.
|
||||
lookupChoice :: MonadEnv m ph
|
||||
=> Qualified TypeConName
|
||||
-- ^ The template name in which this choice is defined.
|
||||
-> ChoiceName
|
||||
-- ^ The choice name to lookup.
|
||||
-> m (Expr -> Expr -> Expr -> UpdateSet ph, Type)
|
||||
lookupChoice tem ch = do
|
||||
chs <- getEnv >>= \case
|
||||
EnvVG{..} -> return HM.empty
|
||||
EnvCG{..} -> return _envcgchs
|
||||
EnvS{..} -> return _envschs
|
||||
case HM.lookup (UpdChoice tem ch) chs of
|
||||
Nothing -> throwError (UnknownChoice ch)
|
||||
Just ChoiceData{..} -> return (_cdUpds, _cdType)
|
||||
|
||||
-- | Lookup a data type definition in the environment.
|
||||
lookupDataCon :: MonadEnv m ph
|
||||
=> TypeConName
|
||||
-- ^ The data constructor to lookup.
|
||||
-> m DefDataType
|
||||
lookupDataCon tc = do
|
||||
dats <- getEnv >>= \case
|
||||
EnvVG{..} -> return _envvgdats
|
||||
EnvCG{..} -> return _envcgdats
|
||||
EnvS{..} -> return _envsdats
|
||||
case HM.lookup tc dats of
|
||||
Nothing -> throwError (UnknownDataCons tc)
|
||||
Just def -> return def
|
||||
|
||||
-- | Lookup a contract id in the environment. Returns the variable its fetched
|
||||
-- contract is bound to, along with a list of any previous bindings.
|
||||
lookupCid :: MonadEnv m ph
|
||||
=> Expr
|
||||
-- ^ The contract id to lookup.
|
||||
-> m (ExprVarName, [ExprVarName])
|
||||
lookupCid exp = do
|
||||
cid <- expr2cid exp
|
||||
cids <- getEnv >>= \case
|
||||
EnvVG{..} -> return _envvgcids
|
||||
EnvCG{..} -> return _envcgcids
|
||||
EnvS{..} -> return _envscids
|
||||
case HM.lookup cid cids of
|
||||
Nothing -> throwError $ UnknownCid cid
|
||||
Just var -> return var
|
||||
|
||||
-- | Solves the value references by computing the closure of all referenced
|
||||
-- values, for each value in the environment.
|
||||
-- It thus empties `_usValue` by collecting all updates made by this closure.
|
||||
solveValueReferences :: Env 'ValueGathering -> Env 'ChoiceGathering
|
||||
solveValueReferences EnvVG{..} =
|
||||
let valhmap = foldl (\hmap ref -> snd $ solveReference lookup_ref get_refs ext_upds intro_cond empty_upds [] hmap ref) _envvgvals (HM.keys _envvgvals)
|
||||
in EnvCG _envvgskol (convertHMap valhmap) _envvgdats _envvgcids _envvgctrs HM.empty
|
||||
where
|
||||
lookup_ref :: Qualified ExprValName
|
||||
-> HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ValueGathering)
|
||||
-> (Expr, UpdateSet 'ValueGathering)
|
||||
lookup_ref ref hmap = fromMaybe (error "Impossible: Undefined value ref while solving")
|
||||
(HM.lookup ref hmap)
|
||||
|
||||
get_refs :: (Expr, UpdateSet 'ValueGathering)
|
||||
-> ([Cond (Qualified ExprValName)], (Expr, UpdateSet 'ValueGathering))
|
||||
get_refs (e, upds@UpdateSetVG{..}) = (_usvgValue, (e, upds{_usvgValue = []}))
|
||||
|
||||
ext_upds :: (Expr, UpdateSet 'ValueGathering) -> (Expr, UpdateSet 'ValueGathering)
|
||||
-> (Expr, UpdateSet 'ValueGathering)
|
||||
ext_upds (e, upds1) (_, upds2) = (e, concatUpdateSet upds1 upds2)
|
||||
|
||||
intro_cond :: Cond (Expr, UpdateSet 'ValueGathering)
|
||||
-> (Expr, UpdateSet 'ValueGathering)
|
||||
-- Note that the expression is not important here, as it will be ignored in
|
||||
-- `ext_upds` later on.
|
||||
intro_cond (Determined x) = x
|
||||
intro_cond (Conditional cond cx cy) =
|
||||
let xs = map intro_cond cx
|
||||
ys = map intro_cond cy
|
||||
e = fst $ head xs
|
||||
updx = foldl concatUpdateSet emptyUpdateSet $ map snd xs
|
||||
updy = foldl concatUpdateSet emptyUpdateSet $ map snd ys
|
||||
in (e, introCond $ createCond cond updx updy)
|
||||
|
||||
empty_upds :: (Expr, UpdateSet 'ValueGathering)
|
||||
-> (Expr, UpdateSet 'ValueGathering)
|
||||
empty_upds (e, _) = (e, emptyUpdateSet)
|
||||
|
||||
convertHMap :: HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ValueGathering)
|
||||
-> HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ChoiceGathering)
|
||||
convertHMap = HM.map (second updateSetVG2CG)
|
||||
|
||||
updateSetVG2CG :: UpdateSet 'ValueGathering -> UpdateSet 'ChoiceGathering
|
||||
updateSetVG2CG UpdateSetVG{..} = if null _usvgValue
|
||||
then UpdateSetCG _usvgUpdate _usvgChoice
|
||||
else error "Impossible: There should be no references remaining after value solving"
|
||||
|
||||
-- | Solves the choice references by computing the closure of all referenced
|
||||
-- choices, for each choice in the environment.
|
||||
-- It thus empties `_usChoice` by collecting all updates made by this closure.
|
||||
solveChoiceReferences :: Env 'ChoiceGathering -> Env 'Solving
|
||||
solveChoiceReferences EnvCG{..} =
|
||||
let chhmap = foldl (\hmap ref -> snd $ solveReference lookup_ref get_refs ext_upds intro_cond empty_upds [] hmap ref) _envcgchs (HM.keys _envcgchs)
|
||||
chshmap = convertChHMap chhmap
|
||||
valhmap = HM.map (inlineChoices chshmap) _envcgvals
|
||||
in EnvS _envcgskol valhmap _envcgdats _envcgcids _envcgctrs chshmap
|
||||
where
|
||||
lookup_ref :: UpdChoice
|
||||
-> HM.HashMap UpdChoice (ChoiceData 'ChoiceGathering)
|
||||
-> ChoiceData 'ChoiceGathering
|
||||
lookup_ref upd hmap = fromMaybe (error "Impossible: Undefined choice ref while solving")
|
||||
(HM.lookup upd hmap)
|
||||
|
||||
get_refs :: ChoiceData 'ChoiceGathering
|
||||
-> ([Cond UpdChoice], ChoiceData 'ChoiceGathering)
|
||||
-- TODO: This is gonna result in a ton of substitutions
|
||||
get_refs chdat@ChoiceData{..} =
|
||||
-- TODO: This seems to be a rather common pattern. Abstract to reduce duplication.
|
||||
let chos = _uscgChoice $ _cdUpds (EVar _cdSelf) (EVar _cdThis) (EVar _cdArgs)
|
||||
updfunc1 (selfexp :: Expr) (thisexp :: Expr) (argsexp :: Expr) =
|
||||
let upds@UpdateSetCG{..} = _cdUpds selfexp thisexp argsexp
|
||||
in upds{_uscgChoice = []}
|
||||
in (chos, chdat{_cdUpds = updfunc1})
|
||||
|
||||
ext_upds :: ChoiceData 'ChoiceGathering
|
||||
-> ChoiceData 'ChoiceGathering
|
||||
-> ChoiceData 'ChoiceGathering
|
||||
ext_upds chdat1 chdat2 =
|
||||
let updfunc (selfexp :: Expr) (thisexp :: Expr) (argsexp :: Expr) =
|
||||
_cdUpds chdat1 selfexp thisexp argsexp `concatUpdateSet`
|
||||
_cdUpds chdat2 selfexp thisexp argsexp
|
||||
in chdat1{_cdUpds = updfunc}
|
||||
|
||||
intro_cond :: GenPhase ph
|
||||
=> Cond (ChoiceData ph)
|
||||
-> ChoiceData ph
|
||||
-- Note that the expression and return type is not important here, as it
|
||||
-- will be ignored in `ext_upds` later on.
|
||||
intro_cond (Determined x) = x
|
||||
intro_cond (Conditional cond cdatxs cdatys) =
|
||||
let datxs = map intro_cond cdatxs
|
||||
datys = map intro_cond cdatys
|
||||
updfunc (selfexp :: Expr) (thisexp :: Expr) (argsexp :: Expr) =
|
||||
introCond (createCond cond
|
||||
(foldl
|
||||
(\upd dat -> upd `concatUpdateSet` _cdUpds dat selfexp thisexp argsexp)
|
||||
emptyUpdateSet datxs)
|
||||
(foldl
|
||||
(\upd dat -> upd `concatUpdateSet` _cdUpds dat selfexp thisexp argsexp)
|
||||
emptyUpdateSet datys))
|
||||
in (head datxs){_cdUpds = updfunc}
|
||||
|
||||
empty_upds :: ChoiceData 'ChoiceGathering
|
||||
-> ChoiceData 'ChoiceGathering
|
||||
empty_upds dat = dat{_cdUpds = \ _ _ _ -> emptyUpdateSet}
|
||||
|
||||
inlineChoices :: HM.HashMap UpdChoice (ChoiceData 'Solving)
|
||||
-> (Expr, UpdateSet 'ChoiceGathering)
|
||||
-> (Expr, UpdateSet 'Solving)
|
||||
inlineChoices chshmap (exp, UpdateSetCG{..}) =
|
||||
let lookupRes = map
|
||||
(intro_cond . fmap (\ch -> fromMaybe (error "Impossible: missing choice while solving") (HM.lookup ch chshmap)))
|
||||
_uscgChoice
|
||||
chupds = concatMap (\ChoiceData{..} -> _ussUpdate $ _cdUpds (EVar _cdSelf) (EVar _cdThis) (EVar _cdArgs)) lookupRes
|
||||
in (exp, UpdateSetS (_uscgUpdate ++ chupds))
|
||||
|
||||
convertChHMap :: HM.HashMap UpdChoice (ChoiceData 'ChoiceGathering)
|
||||
-> HM.HashMap UpdChoice (ChoiceData 'Solving)
|
||||
convertChHMap = HM.map (\chdat@ChoiceData{..} ->
|
||||
chdat{_cdUpds = \(selfExp :: Expr) (thisExp :: Expr) (argsExp :: Expr) ->
|
||||
updateSetCG2S $ _cdUpds selfExp thisExp argsExp})
|
||||
|
||||
updateSetCG2S :: UpdateSet 'ChoiceGathering -> UpdateSet 'Solving
|
||||
updateSetCG2S UpdateSetCG{..} = if null _uscgChoice
|
||||
then UpdateSetS _uscgUpdate
|
||||
else error "Impossible: There should be no references remaining after choice solving"
|
||||
|
||||
-- | Solves a single reference by recursively inlining the references into updates.
|
||||
solveReference :: forall updset ref. (Eq ref, Hashable ref)
|
||||
=> (ref -> HM.HashMap ref updset -> updset)
|
||||
-- ^ Function for looking up references in the update set.
|
||||
-> (updset -> ([Cond ref], updset))
|
||||
-- ^ Function popping the references from the update set.
|
||||
-> (updset -> updset -> updset)
|
||||
-- ^ Function for concatinating update sets.
|
||||
-> (Cond updset -> updset)
|
||||
-- ^ Function for moving conditionals inside the update set.
|
||||
-> (updset -> updset)
|
||||
-- ^ Function for emptying a given update set of all updates.
|
||||
-> [ref]
|
||||
-- ^ The references which have already been visited.
|
||||
-> HM.HashMap ref updset
|
||||
-- ^ The hashmap mapping references to update sets.
|
||||
-> ref
|
||||
-- ^ The reference to be solved.
|
||||
-> (updset, HM.HashMap ref updset)
|
||||
solveReference lookup getRefs extUpds introCond emptyUpds vis hmap0 ref0 =
|
||||
-- Lookup updates performed by the given reference, and split in new
|
||||
-- references and reference-free updates.
|
||||
let upd0 = lookup ref0 hmap0
|
||||
(refs, upd1) = getRefs upd0
|
||||
-- Check for loops. If the references has already been visited, then the
|
||||
-- reference should be flagged as recursive.
|
||||
in if ref0 `elem` vis
|
||||
-- TODO: Recursion!
|
||||
then trace "Recursion!" (upd1, hmap0) -- TODO: At least remove the references?
|
||||
-- When no recursion has been detected, continue inlining the references.
|
||||
else let (upd2, hmap1) = foldl handle_ref (upd1, hmap0) refs
|
||||
in (upd1, HM.insert ref0 upd2 hmap1)
|
||||
where
|
||||
-- | Extend the closure by computing and adding the reference closure for
|
||||
-- the given reference.
|
||||
handle_ref :: (updset, HM.HashMap ref updset)
|
||||
-- ^ The current closure (update set) and the current map for reference to update.
|
||||
-> Cond ref
|
||||
-- ^ The reference to be computed and added.
|
||||
-> (updset, HM.HashMap ref updset)
|
||||
-- For a simple reference, the closure is computed straightforwardly.
|
||||
handle_ref (upd_i0, hmap_i0) (Determined ref_i) =
|
||||
let (upd_i1, hmap_i1) =
|
||||
solveReference lookup getRefs extUpds introCond emptyUpds (ref0:vis) hmap_i0 ref_i
|
||||
in (extUpds upd_i0 upd_i1, hmap_i1)
|
||||
-- A conditional reference is more involved, as the conditional needs to be
|
||||
-- preserved in the computed closure (update set).
|
||||
handle_ref (upd_i0, hmap_i0) (Conditional cond refs_ia refs_ib) =
|
||||
-- Construct an update set without any updates.
|
||||
let upd_i0_empty = emptyUpds upd_i0
|
||||
-- Compute the closure for the true-case.
|
||||
(upd_ia, hmap_ia) = foldl handle_ref (upd_i0_empty, hmap_i0) refs_ia
|
||||
-- Compute the closure for the false-case.
|
||||
(upd_ib, hmap_ib) = foldl handle_ref (upd_i0_empty, hmap_ia) refs_ib
|
||||
-- Move the conditional inwards, in the update set.
|
||||
upd_i1 = extUpds upd_i0 $ introCond $ createCond cond upd_ia upd_ib
|
||||
in (upd_i1, hmap_ib)
|
||||
|
||||
-- TODO: This should work recursively
|
||||
-- | Lookup the field names and corresponding types, for a given record type
|
||||
-- constructor name.
|
||||
recTypConFields :: MonadEnv m ph
|
||||
=> TypeConName
|
||||
-- ^ The record type constructor name to lookup.
|
||||
-> m [(FieldName,Type)]
|
||||
recTypConFields tc = lookupDataCon tc >>= \dat -> case dataCons dat of
|
||||
DataRecord fields -> return fields
|
||||
_ -> throwError ExpectRecord
|
||||
|
||||
-- | Lookup the fields for a given record type.
|
||||
recTypFields :: MonadEnv m ph
|
||||
=> Type
|
||||
-- ^ The type to lookup.
|
||||
-> m [FieldName]
|
||||
recTypFields (TCon tc) = do
|
||||
fields <- recTypConFields $ qualObject tc
|
||||
return $ map fst fields
|
||||
recTypFields (TStruct fs) = return $ map fst fs
|
||||
recTypFields _ = throwError ExpectRecord
|
||||
|
||||
-- | Lookup the record fields and corresponding values from a given expression.
|
||||
recExpFields :: MonadEnv m ph
|
||||
=> Expr
|
||||
-- ^ The expression to lookup.
|
||||
-> m [(FieldName, Expr)]
|
||||
recExpFields (EVar x) = do
|
||||
skols <- getEnv >>= \case
|
||||
EnvVG{..} -> return _envvgskol
|
||||
EnvCG{..} -> return _envcgskol
|
||||
EnvS{..} -> return _envsskol
|
||||
let fss = [ fs | SkolRec y fs <- skols, x == y ]
|
||||
if not (null fss)
|
||||
-- TODO: I would prefer `this.amount` here
|
||||
then return $ zip (head fss) (map (EVar . fieldName2VarName) $ head fss)
|
||||
else throwError $ UnboundVar x
|
||||
recExpFields (ERecCon _ fs) = return fs
|
||||
recExpFields (EStructCon fs) = return fs
|
||||
recExpFields (ERecUpd _ f recExp fExp) = do
|
||||
fs <- recExpFields recExp
|
||||
unless (isJust $ find (\(n, _) -> n == f) fs) (throwError $ UnknownRecField f)
|
||||
return $ (f, fExp) : [(n, e) | (n, e) <- fs, n /= f]
|
||||
recExpFields (ERecProj _ f e) = do
|
||||
fields <- recExpFields e
|
||||
case lookup f fields of
|
||||
Just e' -> recExpFields e'
|
||||
Nothing -> throwError $ UnknownRecField f
|
||||
recExpFields (EStructProj f e) = do
|
||||
fields <- recExpFields e
|
||||
case lookup f fields of
|
||||
Just e' -> recExpFields e'
|
||||
Nothing -> throwError $ UnknownRecField f
|
||||
recExpFields _ = throwError ExpectRecord
|
||||
|
||||
instance SubstTm BoolExpr where
|
||||
substituteTm s (BExpr e) = BExpr (substituteTm s e)
|
||||
substituteTm s (BAnd e1 e2) = BAnd (substituteTm s e1) (substituteTm s e2)
|
||||
substituteTm s (BNot e) = BNot (substituteTm s e)
|
||||
|
||||
instance SubstTm a => SubstTm (Cond a) where
|
||||
substituteTm s (Determined x) = Determined $ substituteTm s x
|
||||
substituteTm s (Conditional e x y) =
|
||||
Conditional (substituteTm s e) (map (substituteTm s) x) (map (substituteTm s) y)
|
||||
|
||||
instance SubstTm (UpdateSet ph) where
|
||||
substituteTm s UpdateSetVG{..} = UpdateSetVG susUpdate _usvgChoice _usvgValue
|
||||
where susUpdate = map (substituteTm s) _usvgUpdate
|
||||
substituteTm s UpdateSetCG{..} = UpdateSetCG susUpdate _uscgChoice
|
||||
where susUpdate = map (substituteTm s) _uscgUpdate
|
||||
substituteTm s UpdateSetS{..} = UpdateSetS susUpdate
|
||||
where susUpdate = map (substituteTm s) _ussUpdate
|
||||
|
||||
instance SubstTm Upd where
|
||||
substituteTm s UpdCreate{..} = UpdCreate _creTemp
|
||||
(map (second (substituteTm s)) _creField)
|
||||
substituteTm s UpdArchive{..} = UpdArchive _arcTemp
|
||||
(map (second (substituteTm s)) _arcField)
|
||||
|
||||
-- | Data type representing an error.
|
||||
data Error
|
||||
= UnknownValue (Qualified ExprValName)
|
||||
| UnknownDataCons TypeConName
|
||||
| UnknownChoice ChoiceName
|
||||
| UnboundVar ExprVarName
|
||||
| UnknownRecField FieldName
|
||||
| UnknownCid Cid
|
||||
| UnknownTmpl TypeConName
|
||||
| ExpectRecord
|
||||
| ExpectCid
|
||||
| CyclicModules [ModuleName]
|
||||
|
||||
instance Show Error where
|
||||
show (UnknownValue qname) = "Impossible: Unknown value definition: "
|
||||
++ (show $ unExprValName $ qualObject qname)
|
||||
show (UnknownDataCons tc) = "Impossible: Unknown data constructor: " ++ show tc
|
||||
show (UnknownChoice ch) = "Impossible: Unknown choice definition: " ++ show ch
|
||||
show (UnboundVar name) = "Impossible: Unbound term variable: " ++ show name
|
||||
show (UnknownRecField f) = "Impossible: Unknown record field: " ++ show f
|
||||
show (UnknownCid cid) = "Impossible: Unknown contract id: " ++ show cid
|
||||
show (UnknownTmpl tem) = "Impossible: Unknown template: " ++ show tem
|
||||
show ExpectRecord = "Impossible: Expected a record type"
|
||||
show ExpectCid = "Impossible: Expected a contract id"
|
||||
show (CyclicModules mods) = "Cyclic modules: " ++ show mods
|
||||
487
compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs
Normal file
487
compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs
Normal file
@ -0,0 +1,487 @@
|
||||
-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
|
||||
-- | Constraint generator for DAML LF static verification
|
||||
module DA.Daml.LF.Verify.Generate
|
||||
( genPackages
|
||||
, Phase(..)
|
||||
) where
|
||||
|
||||
import Control.Monad.Error.Class (throwError)
|
||||
import Data.Maybe (listToMaybe)
|
||||
import qualified Data.NameMap as NM
|
||||
|
||||
import DA.Daml.LF.Ast hiding (lookupChoice)
|
||||
import DA.Daml.LF.Verify.Context
|
||||
import DA.Daml.LF.Verify.Subst
|
||||
|
||||
-- | Data type denoting the output of the constraint generator.
|
||||
data Output (ph :: Phase) = Output
|
||||
{ _oExpr :: Expr
|
||||
-- ^ The expression, evaluated as far as possible.
|
||||
, _oUpdate :: UpdateSet ph
|
||||
-- ^ The updates, performed by this expression.
|
||||
}
|
||||
|
||||
-- | Construct an output with no updates.
|
||||
emptyOut :: GenPhase ph
|
||||
=> Expr
|
||||
-- ^ The evaluated expression.
|
||||
-> Output ph
|
||||
emptyOut expr = Output expr emptyUpdateSet
|
||||
|
||||
-- | Extend a generator output with the updates of the second generator output.
|
||||
-- Note that the end result will contain only the first expression.
|
||||
combineOut :: Output ph -> Output ph -> Output ph
|
||||
combineOut out1 out2 = extendOutUpds (_oUpdate out2) out1
|
||||
|
||||
-- | Update an output with a new evaluated expression.
|
||||
updateOutExpr :: Expr
|
||||
-- ^ The new output expression.
|
||||
-> Output ph
|
||||
-- ^ The generator output to be updated.
|
||||
-> Output ph
|
||||
updateOutExpr expr out = out{_oExpr = expr}
|
||||
|
||||
-- | Update an output with additional updates.
|
||||
extendOutUpds :: UpdateSet ph
|
||||
-- ^ The extension of the update set.
|
||||
-> Output ph
|
||||
-- ^ The generator output to be updated.
|
||||
-> Output ph
|
||||
extendOutUpds upds out@Output{..} = out{_oUpdate = concatUpdateSet upds _oUpdate}
|
||||
|
||||
-- | Update an output with an additional Archive update.
|
||||
addArchiveUpd :: Qualified TypeConName
|
||||
-- ^ The template to be archived.
|
||||
-> [(FieldName, Expr)]
|
||||
-- ^ The fields to be archived, with their respective values.
|
||||
-> Output 'ChoiceGathering
|
||||
-- ^ The generator output to be updated.
|
||||
-> Output 'ChoiceGathering
|
||||
addArchiveUpd temp fs (Output expr upds) =
|
||||
Output expr (addUpd upds $ UpdArchive temp fs)
|
||||
|
||||
-- | Generate an environment for a given list of packages.
|
||||
-- Depending on the generator phase, this either adds all value and data type
|
||||
-- definitions to the environment, or all template definitions with their
|
||||
-- respective choices.
|
||||
genPackages :: (GenPhase ph, MonadEnv m ph)
|
||||
=> [(PackageId, (Package, Maybe PackageName))]
|
||||
-- ^ The list of packages, as produced by `readPackages`.
|
||||
-> m ()
|
||||
genPackages inp = mapM_ genPackage inp
|
||||
|
||||
-- | Generate an environment for a given package.
|
||||
-- Depending on the generator phase, this either adds all value and data type
|
||||
-- definitions to the environment, or all template definitions with their
|
||||
-- respective choices.
|
||||
genPackage :: (GenPhase ph, MonadEnv m ph)
|
||||
=> (PackageId, (Package, Maybe PackageName))
|
||||
-- ^ The package, as produced by `readPackages`.
|
||||
-> m ()
|
||||
genPackage (id, (pac, _)) = mapM_ (genModule (PRImport id)) (NM.toList $ packageModules pac)
|
||||
|
||||
-- | Generate an environment for a given module.
|
||||
-- Depending on the generator phase, this either adds all value and data type
|
||||
-- definitions to the environment, or all template definitions with their
|
||||
-- respective choices.
|
||||
genModule :: (GenPhase ph, MonadEnv m ph)
|
||||
=> PackageRef
|
||||
-- ^ A reference to the package in which this module is defined.
|
||||
-> Module
|
||||
-- ^ The module to analyse.
|
||||
-> m ()
|
||||
genModule pac mod = getEnv >>= \case
|
||||
EnvVG{} -> do
|
||||
extDatsEnv (NM.toHashMap (moduleDataTypes mod))
|
||||
mapM_ (genValue pac (moduleName mod)) (NM.toList $ moduleValues mod)
|
||||
EnvCG{} ->
|
||||
mapM_ (genTemplate pac (moduleName mod)) (NM.toList $ moduleTemplates mod)
|
||||
EnvS{} -> error "Impossible: genModule can't be used in the solving phase"
|
||||
|
||||
-- | Analyse a value definition and add to the environment.
|
||||
genValue :: (GenPhase ph, MonadEnv m ph)
|
||||
=> PackageRef
|
||||
-- ^ A reference to the package in which this value is defined.
|
||||
-> ModuleName
|
||||
-- ^ The name of the module in which this value is defined.
|
||||
-> DefValue
|
||||
-- ^ The value to be analysed and added.
|
||||
-> m ()
|
||||
genValue pac mod val = do
|
||||
expOut <- genExpr True (instPRSelf pac $ dvalBody val)
|
||||
let qname = Qualified pac mod (fst $ dvalBinder val)
|
||||
extValEnv qname (_oExpr expOut) (_oUpdate expOut)
|
||||
|
||||
-- | Analyse a choice definition and add to the environment.
|
||||
-- TODO: Handle annotated choices, by returning a set of annotations.
|
||||
genChoice :: MonadEnv m 'ChoiceGathering
|
||||
=> PackageRef
|
||||
-- ^ A reference to the package in which this choice is defined.
|
||||
-> Qualified TypeConName
|
||||
-- ^ The template in which this choice is defined.
|
||||
-> (ExprVarName,ExprVarName)
|
||||
-- ^ The original and renamed variable `this` referencing the contract on
|
||||
-- which this choice is called.
|
||||
-> [FieldName]
|
||||
-- ^ The list of fields available in the template.
|
||||
-> TemplateChoice
|
||||
-- ^ The choice to be analysed and added.
|
||||
-> m ()
|
||||
genChoice pac tem (this',this) temFs TemplateChoice{..} = do
|
||||
let self' = chcSelfBinder
|
||||
arg' = fst chcArgBinder
|
||||
self <- genRenamedVar self'
|
||||
arg <- genRenamedVar arg'
|
||||
extVarEnv self
|
||||
extVarEnv arg
|
||||
argFs <- recTypFields (snd chcArgBinder)
|
||||
extRecEnv arg argFs
|
||||
expOut <- genExpr True
|
||||
$ substituteTm (createExprSubst [(self',EVar self),(this',EVar this),(arg',EVar arg)])
|
||||
$ instPRSelf pac chcUpdate
|
||||
let out = if chcConsuming
|
||||
then addArchiveUpd tem fields expOut
|
||||
else expOut
|
||||
extChEnv tem chcName self this arg (_oUpdate out) chcReturnType
|
||||
where
|
||||
fields = map (\f -> (f, ERecProj (TypeConApp tem []) f (EVar this))) temFs
|
||||
|
||||
-- | Analyse a template definition and add all choices to the environment.
|
||||
genTemplate :: MonadEnv m 'ChoiceGathering
|
||||
=> PackageRef
|
||||
-- ^ A reference to the package in which this template is defined.
|
||||
-> ModuleName
|
||||
-- ^ The module in which this template is defined.
|
||||
-> Template
|
||||
-- ^ The template to be analysed and added.
|
||||
-> m ()
|
||||
-- TODO: Take preconditions into account?
|
||||
genTemplate pac mod Template{..} = do
|
||||
let name = Qualified pac mod tplTypeCon
|
||||
fields <- recTypConFields tplTypeCon
|
||||
let fs = map fst fields
|
||||
this <- genRenamedVar tplParam
|
||||
extVarEnv this
|
||||
extRecEnv this fs
|
||||
extRecEnvLvl1 fields
|
||||
mapM_ (genChoice pac name (tplParam,this) fs) (archive : NM.toList tplChoices)
|
||||
where
|
||||
archive :: TemplateChoice
|
||||
archive = TemplateChoice Nothing (ChoiceName "Archive") True
|
||||
(ENil (TBuiltin BTParty)) (ExprVarName "self")
|
||||
(ExprVarName "arg", TStruct []) (TBuiltin BTUnit)
|
||||
(EUpdate $ UPure (TBuiltin BTUnit) (EBuiltin BEUnit))
|
||||
|
||||
-- | Analyse an expression, and produce an Output storing its (partial)
|
||||
-- evaluation result and the set of performed updates.
|
||||
genExpr :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Bool
|
||||
-- ^ Argument denoting whether updates should be analysed.
|
||||
-> Expr
|
||||
-- ^ The expression to be analysed.
|
||||
-> m (Output ph)
|
||||
genExpr updFlag = \case
|
||||
ETmApp fun arg -> genForTmApp updFlag fun arg
|
||||
ETyApp expr typ -> genForTyApp updFlag expr typ
|
||||
ELet bind body -> genForLet updFlag bind body
|
||||
EVar name -> genForVar updFlag name
|
||||
EVal w -> genForVal updFlag w
|
||||
ERecProj tc f e -> genForRecProj updFlag tc f e
|
||||
EStructProj f e -> genForStructProj updFlag f e
|
||||
ELocation _ expr -> genExpr updFlag expr
|
||||
ECase e cs -> genForCase updFlag e cs
|
||||
EUpdate upd -> if updFlag
|
||||
then do
|
||||
(out, _, _) <- genUpdate upd
|
||||
return out
|
||||
else return $ emptyOut $ EUpdate upd
|
||||
-- TODO: Extend additional cases
|
||||
e -> return $ emptyOut e
|
||||
|
||||
-- | Analyse an update expression, and produce both an Output, its return type
|
||||
-- and potentially the field values of any created contracts.
|
||||
genUpdate :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Update
|
||||
-- ^ The update expression to be analysed.
|
||||
-> m (Output ph, Type, Maybe Expr)
|
||||
genUpdate = \case
|
||||
UCreate tem arg -> genForCreate tem arg
|
||||
UExercise tem ch cid par arg -> genForExercise tem ch cid par arg
|
||||
UBind bind expr -> genForBind bind expr
|
||||
UPure typ expr -> do
|
||||
out <- genExpr True expr
|
||||
return (out, typ, Nothing)
|
||||
-- TODO: Extend additional cases
|
||||
UGetTime -> return (emptyOut (EUpdate UGetTime), TBuiltin BTTimestamp, Nothing)
|
||||
u -> error ("Update not implemented yet: " ++ show u)
|
||||
|
||||
-- | Analyse a term application expression.
|
||||
genForTmApp :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Bool
|
||||
-- ^ Flag denoting whether updates should be analysed.
|
||||
-> Expr
|
||||
-- ^ The function expression.
|
||||
-> Expr
|
||||
-- ^ The argument expression.
|
||||
-> m (Output ph)
|
||||
genForTmApp updFlag fun arg = do
|
||||
funOut <- genExpr updFlag fun
|
||||
arout <- genExpr updFlag arg
|
||||
case _oExpr funOut of
|
||||
-- TODO: Should we rename here?
|
||||
ETmLam bndr body -> do
|
||||
let subst = singleExprSubst (fst bndr) (_oExpr arout)
|
||||
resExpr = substituteTm subst body
|
||||
resOut <- genExpr updFlag resExpr
|
||||
return $ combineOut resOut
|
||||
$ combineOut funOut arout
|
||||
fun' -> return $ updateOutExpr (ETmApp fun' (_oExpr arout))
|
||||
$ combineOut funOut arout
|
||||
|
||||
-- | Analyse a type application expression.
|
||||
genForTyApp :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Bool
|
||||
-- ^ Flag denoting whether updates should be analysed.
|
||||
-> Expr
|
||||
-- ^ The function expression.
|
||||
-> Type
|
||||
-- ^ The argument type.
|
||||
-> m (Output ph)
|
||||
genForTyApp updFlag expr typ = do
|
||||
exprOut <- genExpr updFlag expr
|
||||
case _oExpr exprOut of
|
||||
ETyLam bndr body -> do
|
||||
let subst = singleTypeSubst (fst bndr) typ
|
||||
resExpr = substituteTy subst body
|
||||
resOut <- genExpr updFlag resExpr
|
||||
return $ combineOut resOut exprOut
|
||||
expr' -> return $ updateOutExpr (ETyApp expr' typ) exprOut
|
||||
|
||||
-- | Analyse a let binding expression.
|
||||
genForLet :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Bool
|
||||
-- ^ Flag denoting whether updates should be analysed.
|
||||
-> Binding
|
||||
-- ^ The binding to be bound.
|
||||
-> Expr
|
||||
-- ^ The expression in which the binding should be available.
|
||||
-> m (Output ph)
|
||||
genForLet updFlag bind body = do
|
||||
bindOut <- genExpr updFlag (bindingBound bind)
|
||||
let subst = singleExprSubst (fst $ bindingBinder bind) (_oExpr bindOut)
|
||||
resExpr = substituteTm subst body
|
||||
resOut <- genExpr updFlag resExpr
|
||||
return $ combineOut resOut bindOut
|
||||
|
||||
-- | Analyse an expression variable.
|
||||
genForVar :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Bool
|
||||
-- ^ Flag denoting whether updates should be analysed.
|
||||
-> ExprVarName
|
||||
-- ^ The expression variable to be analysed.
|
||||
-> m (Output ph)
|
||||
genForVar _updFlag name = lookupVar name >> return (emptyOut (EVar name))
|
||||
|
||||
-- | Analyse a value reference.
|
||||
genForVal :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Bool
|
||||
-- ^ Flag denoting whether updates should be analysed.
|
||||
-> Qualified ExprValName
|
||||
-- ^ The value reference to be analysed.
|
||||
-> m (Output ph)
|
||||
genForVal _updFlag w = getEnv >>= \case
|
||||
EnvVG{} -> return $ Output (EVal w) (emptyUpdateSet{_usvgValue = [Determined w]})
|
||||
EnvCG{} -> lookupVal w >>= \ (expr, upds) -> return (Output expr upds)
|
||||
EnvS{} -> error "Impossible: genForVal can't be used in the solving phase"
|
||||
|
||||
-- | Analyse a record projection expression.
|
||||
genForRecProj :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Bool
|
||||
-- ^ Flag denoting whether updates should be analysed.
|
||||
-> TypeConApp
|
||||
-- ^ The type constructor of the record which is projected.
|
||||
-> FieldName
|
||||
-- ^ The field which is projected.
|
||||
-> Expr
|
||||
-- ^ The record expression which is projected.
|
||||
-> m (Output ph)
|
||||
genForRecProj updFlag tc f body = do
|
||||
bodyOut <- genExpr updFlag body
|
||||
case _oExpr bodyOut of
|
||||
-- TODO: I think we can reduce duplication a bit more here
|
||||
EVar x -> do
|
||||
skol <- lookupRec x f
|
||||
if skol
|
||||
then return $ updateOutExpr (ERecProj tc f (EVar x)) bodyOut
|
||||
else error ("Impossible: expected skolem record: " ++ show x ++ "." ++ show f)
|
||||
expr -> do
|
||||
fs <- recExpFields expr
|
||||
case lookup f fs of
|
||||
Just expr -> genExpr updFlag expr
|
||||
Nothing -> throwError $ UnknownRecField f
|
||||
|
||||
-- | Analyse a struct projection expression.
|
||||
genForStructProj :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Bool
|
||||
-- ^ Flag denoting whether updates should be analysed.
|
||||
-> FieldName
|
||||
-- ^ The field which is projected.
|
||||
-> Expr
|
||||
-- ^ The record expression which is projected.
|
||||
-> m (Output ph)
|
||||
genForStructProj updFlag f body = do
|
||||
bodyOut <- genExpr updFlag body
|
||||
case _oExpr bodyOut of
|
||||
-- TODO: I think we can reduce duplication a bit more here
|
||||
EVar x -> do
|
||||
skol <- lookupRec x f
|
||||
if skol
|
||||
then return $ updateOutExpr (EStructProj f (EVar x)) bodyOut
|
||||
else error ("Impossible: expected skolem record: " ++ show x ++ "." ++ show f)
|
||||
expr -> do
|
||||
fs <- recExpFields expr
|
||||
case lookup f fs of
|
||||
Just expr -> genExpr updFlag expr
|
||||
Nothing -> throwError $ UnknownRecField f
|
||||
|
||||
-- | Analyse a case expression.
|
||||
-- TODO: Atm only boolean cases are supported
|
||||
genForCase :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Bool
|
||||
-- ^ Flag denoting whether updates should be analysed.
|
||||
-> Expr
|
||||
-- ^ The expression to match on.
|
||||
-> [CaseAlternative]
|
||||
-- ^ The list of alternatives.
|
||||
-> m (Output ph)
|
||||
genForCase updFlag exp cs = do
|
||||
expOut <- genExpr updFlag exp
|
||||
case findBool True of
|
||||
Just tru -> do
|
||||
truOut <- genExpr updFlag tru
|
||||
case findBool False of
|
||||
Just fal -> do
|
||||
falOut <- genExpr updFlag fal
|
||||
let resExp = ECase (_oExpr expOut)
|
||||
[ CaseAlternative (CPBool True) (_oExpr truOut)
|
||||
, CaseAlternative (CPBool False) (_oExpr falOut) ]
|
||||
resUpd = _oUpdate expOut `concatUpdateSet`
|
||||
conditionalUpdateSet (_oExpr expOut) (_oUpdate truOut) (_oUpdate falOut)
|
||||
return $ Output resExp resUpd
|
||||
Nothing -> error "Impossible: Missing False-case in if statement"
|
||||
Nothing -> return $ emptyOut (ECase exp cs)
|
||||
where
|
||||
findBool :: Bool -> Maybe Expr
|
||||
findBool b1 = listToMaybe $ [e | CaseAlternative (CPBool b2) e <- cs, b1 == b2]
|
||||
|
||||
-- | Analyse a create update expression.
|
||||
-- Returns both the generator output and the return type.
|
||||
genForCreate :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Qualified TypeConName
|
||||
-- ^ The template of which a new instance is being created.
|
||||
-> Expr
|
||||
-- ^ The argument expression.
|
||||
-> m (Output ph, Type, Maybe Expr)
|
||||
genForCreate tem arg = do
|
||||
arout <- genExpr True arg
|
||||
fs <- recExpFields (_oExpr arout)
|
||||
return ( Output (EUpdate (UCreate tem $ _oExpr arout)) $ addUpd emptyUpdateSet (UpdCreate tem fs)
|
||||
, TCon tem
|
||||
, Just $ EStructCon fs )
|
||||
-- TODO: We could potentially filter here to only store the interesting fields?
|
||||
|
||||
-- | Analyse an exercise update expression.
|
||||
-- Returns both the generator output and the return type of the choice.
|
||||
genForExercise :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Qualified TypeConName
|
||||
-- ^ The template on which a choice is being exercised.
|
||||
-> ChoiceName
|
||||
-- ^ The choice which is being exercised.
|
||||
-> Expr
|
||||
-- ^ The contract id on which the choice is being exercised.
|
||||
-> Maybe Expr
|
||||
-- ^ The party which exercises the choice.
|
||||
-> Expr
|
||||
-- ^ The arguments with which the choice is being exercised.
|
||||
-> m (Output ph, Type, Maybe Expr)
|
||||
genForExercise tem ch cid par arg = do
|
||||
cidOut <- genExpr True cid
|
||||
arout <- genExpr True arg
|
||||
(updSubst, resType) <- lookupChoice tem ch
|
||||
this <- fst <$> lookupCid (_oExpr cidOut)
|
||||
-- TODO: Should we further eval after subst? But how to eval an update set?
|
||||
let updSet = updSubst (_oExpr cidOut) (EVar this) (_oExpr arout)
|
||||
return ( Output (EUpdate (UExercise tem ch (_oExpr cidOut) par (_oExpr arout))) updSet
|
||||
, resType
|
||||
, Nothing ) -- TODO!
|
||||
|
||||
-- | Analyse a bind update expression.
|
||||
-- Returns both the generator output and the return type.
|
||||
genForBind :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Binding
|
||||
-- ^ The binding being bound with this update.
|
||||
-> Expr
|
||||
-- ^ The expression in which this binding is being made available.
|
||||
-> m (Output ph, Type, Maybe Expr)
|
||||
genForBind bind body = do
|
||||
bindOut <- genExpr False (bindingBound bind)
|
||||
bindUpd <- case _oExpr bindOut of
|
||||
EUpdate (UFetch tc cid) -> do
|
||||
bindCids (TContractId (TCon tc)) cid (EVar $ fst $ bindingBinder bind) Nothing
|
||||
return emptyUpdateSet
|
||||
EUpdate upd -> do
|
||||
(updOut, updTyp, creFs) <- genUpdate upd
|
||||
this <- genRenamedVar (ExprVarName "this")
|
||||
bindCids updTyp (EVar $ fst $ bindingBinder bind) (EVar this) creFs
|
||||
return $ _oUpdate updOut
|
||||
_ -> return emptyUpdateSet
|
||||
extVarEnv (fst $ bindingBinder bind)
|
||||
bodyOut <- genExpr False body
|
||||
case _oExpr bodyOut of
|
||||
EUpdate bodyUpd -> do
|
||||
(bodyUpdOut, bodyTyp, creFs) <- genUpdate bodyUpd
|
||||
return ( Output
|
||||
(_oExpr bodyUpdOut)
|
||||
(_oUpdate bindOut
|
||||
`concatUpdateSet` bindUpd
|
||||
`concatUpdateSet` _oUpdate bodyOut
|
||||
`concatUpdateSet` _oUpdate bodyUpdOut)
|
||||
, bodyTyp
|
||||
, creFs )
|
||||
_ -> error "Impossible: The body of a bind should be an update expression"
|
||||
|
||||
bindCids :: (GenPhase ph, MonadEnv m ph)
|
||||
=> Type
|
||||
-- ^ The type of the contract id's being bound.
|
||||
-> Expr
|
||||
-- ^ The contract id's being bound.
|
||||
-> Expr
|
||||
-- ^ The variables to bind them to.
|
||||
-> Maybe Expr
|
||||
-- ^ The field values for any created contracts, if available.
|
||||
-> m ()
|
||||
bindCids (TContractId (TCon tc)) cid (EVar this) fsExp = do
|
||||
fs <- recTypConFields $ qualObject tc
|
||||
extRecEnv this (map fst fs)
|
||||
cidOut <- genExpr True cid
|
||||
extCidEnv (_oExpr cidOut) this
|
||||
creFs <- maybe (pure []) recExpFields fsExp
|
||||
extCtrRec this creFs
|
||||
bindCids (TCon tc) cid (EVar this) fsExp = do
|
||||
fs <- recTypConFields $ qualObject tc
|
||||
extRecEnv this (map fst fs)
|
||||
cidOut <- genExpr True cid
|
||||
extCidEnv (_oExpr cidOut) this
|
||||
creFs <- maybe (pure []) recExpFields fsExp
|
||||
extCtrRec this creFs
|
||||
bindCids (TBuiltin BTUnit) _ _ _ = return ()
|
||||
bindCids (TBuiltin BTTimestamp) _ _ _ = return ()
|
||||
-- TODO: Extend additional cases, like tuples.
|
||||
bindCids typ _ _ _ =
|
||||
error ("Binding contract id's for this particular type has not been implemented yet: " ++ show typ)
|
||||
77
compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs
Normal file
77
compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs
Normal file
@ -0,0 +1,77 @@
|
||||
|
||||
-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
-- TODO: There is a lot of copying going on here from TsCodeGenMain.hs.
|
||||
-- A nicer alternative would be to just change the exports from this module.
|
||||
|
||||
-- | Reading dar files for DAML LF verification.
|
||||
module DA.Daml.LF.Verify.Read
|
||||
( readPackages
|
||||
, optionsParserInfo
|
||||
, Options(..)
|
||||
) where
|
||||
|
||||
import qualified DA.Daml.LF.Proto3.Archive as Archive
|
||||
import qualified DA.Daml.LF.Reader as DAR
|
||||
import qualified Data.ByteString as B
|
||||
import qualified Data.ByteString.Lazy as BSL
|
||||
import qualified Data.Text.Extended as T
|
||||
import qualified "zip-archive" Codec.Archive.Zip as Zip
|
||||
import Control.Monad.Extra
|
||||
import Options.Applicative
|
||||
|
||||
import DA.Daml.LF.Ast
|
||||
|
||||
data Options = Options
|
||||
{ optInputDar :: FilePath
|
||||
, optChoiceTmpl :: String
|
||||
, optChoiceName :: String
|
||||
, optFieldTmpl :: String
|
||||
, optFieldName :: String
|
||||
}
|
||||
|
||||
optionsParser :: Parser Options
|
||||
optionsParser = Options
|
||||
<$> argument str
|
||||
( metavar "DAR-FILE"
|
||||
<> help "DAR file to analyse"
|
||||
)
|
||||
<*> argument str
|
||||
( metavar "CHOICE-TEMPLATE"
|
||||
<> help "Template of the choice to analyse"
|
||||
)
|
||||
<*> argument str
|
||||
( metavar "CHOICE-NAME"
|
||||
<> help "Name of the choice to analyse"
|
||||
)
|
||||
<*> argument str
|
||||
( metavar "FIELD-TEMPLATE"
|
||||
<> help "Template of the field to verify"
|
||||
)
|
||||
<*> argument str
|
||||
( metavar "FIELD-NAME"
|
||||
<> help "Name of the field to verify"
|
||||
)
|
||||
|
||||
optionsParserInfo :: ParserInfo Options
|
||||
optionsParserInfo = info (optionsParser <**> helper)
|
||||
( fullDesc
|
||||
<> progDesc "Perform static analysis on a DAR"
|
||||
)
|
||||
|
||||
-- Build a list of packages from a list of DAR file paths.
|
||||
readPackages :: [FilePath] -> IO [(PackageId, (Package, Maybe PackageName))]
|
||||
readPackages dars = concatMapM darToPackages dars
|
||||
where
|
||||
darToPackages :: FilePath -> IO [(PackageId, (Package, Maybe PackageName))]
|
||||
darToPackages dar = do
|
||||
dar <- B.readFile dar
|
||||
let archive = Zip.toArchive $ BSL.fromStrict dar
|
||||
dalfs <- either fail pure $ DAR.readDalfs archive
|
||||
DAR.DalfManifest{packageName} <- either fail pure $ DAR.readDalfManifest archive
|
||||
packageName <- pure (PackageName . T.pack <$> packageName)
|
||||
forM ((DAR.mainDalf dalfs, packageName) : map (, Nothing) (DAR.dalfs dalfs)) $
|
||||
\(dalf, mbPkgName) -> do
|
||||
(pkgId, pkg) <- either (fail . show) pure $ Archive.decodeArchive Archive.DecodeAsMain (BSL.toStrict dalf)
|
||||
pure (pkgId, (pkg, mbPkgName))
|
||||
402
compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs
Normal file
402
compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs
Normal file
@ -0,0 +1,402 @@
|
||||
-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
|
||||
-- | Constraint solver for DAML LF static verification
|
||||
module DA.Daml.LF.Verify.Solve
|
||||
( constructConstr
|
||||
, solveConstr
|
||||
, ConstraintSet(..)
|
||||
, Result(..)
|
||||
) where
|
||||
|
||||
import Data.Bifunctor
|
||||
import Data.Maybe
|
||||
import Data.List
|
||||
import Data.List.Extra (nubOrd)
|
||||
import Data.Tuple.Extra (both)
|
||||
import Data.Text.Prettyprint.Doc
|
||||
import qualified Data.HashMap.Strict as HM
|
||||
import qualified Data.Text as T
|
||||
import qualified SimpleSMT as S
|
||||
|
||||
import DA.Daml.LF.Ast.Base
|
||||
import DA.Daml.LF.Ast.Numeric
|
||||
import DA.Daml.LF.Verify.Context
|
||||
|
||||
-- TODO: Since S.SExpr is so similar, we could just drop this.
|
||||
-- | A simple form of expressions featuring basic arithmetic.
|
||||
data ConstraintExpr
|
||||
-- | Boolean value.
|
||||
= CBool !Bool
|
||||
-- | Integer value.
|
||||
| CInt !Integer
|
||||
-- | Real value.
|
||||
| CReal !Rational
|
||||
-- | Reference to an expression variable.
|
||||
| CVar !ExprVarName
|
||||
-- | Sum of two expressions.
|
||||
| CAdd !ConstraintExpr !ConstraintExpr
|
||||
-- | Subtraction of two expressions.
|
||||
| CSub !ConstraintExpr !ConstraintExpr
|
||||
-- | Equals operator.
|
||||
| CEq !ConstraintExpr !ConstraintExpr
|
||||
-- | Boolean and operator.
|
||||
| CAnd !ConstraintExpr !ConstraintExpr
|
||||
-- | Boolean not operator.
|
||||
| CNot !ConstraintExpr
|
||||
-- | If then else expression.
|
||||
| CIf !ConstraintExpr !ConstraintExpr !ConstraintExpr
|
||||
deriving Show
|
||||
|
||||
instance Pretty ConstraintExpr where
|
||||
pretty (CBool b) = pretty b
|
||||
pretty (CInt i) = pretty i
|
||||
pretty (CReal i) = pretty $ show i
|
||||
pretty (CVar x) = pretty $ unExprVarName x
|
||||
pretty (CAdd e1 e2) = pretty e1 <+> " <+> " <+> pretty e2
|
||||
pretty (CSub e1 e2) = pretty e1 <+> " - " <+> pretty e2
|
||||
pretty (CEq e1 e2) = pretty e1 <+> " == " <+> pretty e2
|
||||
pretty (CAnd e1 e2) = pretty e1 <+> " and " <+> pretty e2
|
||||
pretty (CNot e) = "not " <+> pretty e
|
||||
pretty (CIf e1 e2 e3) = "if " <+> pretty e1 <+> " then " <+> pretty e2
|
||||
<+> " else " <+> pretty e3
|
||||
|
||||
-- | Add a bunch of constraint expressions.
|
||||
addMany :: [ConstraintExpr] -> ConstraintExpr
|
||||
addMany [] = CReal 0.0
|
||||
addMany [x] = x
|
||||
addMany (x:xs) = CAdd x (addMany xs)
|
||||
|
||||
-- | Class covering the types convertible to constraint expressions.
|
||||
class ConstrExpr a where
|
||||
-- | Convert the given data type to a constraint expression.
|
||||
toCExp :: [(ExprVarName, ExprVarName)]
|
||||
-- ^ The contract name synonyms, along with their current alias.
|
||||
-> a
|
||||
-- ^ The data to convert to a constraint expression.
|
||||
-> ConstraintExpr
|
||||
|
||||
instance ConstrExpr BoolExpr where
|
||||
toCExp syns (BExpr e) = toCExp syns e
|
||||
toCExp syns (BAnd b1 b2) = CAnd (toCExp syns b1) (toCExp syns b2)
|
||||
toCExp syns (BNot b) = CNot (toCExp syns b)
|
||||
|
||||
instance ConstrExpr Expr where
|
||||
toCExp syns (EVar x) = case lookup x syns of
|
||||
Just y -> CVar y
|
||||
Nothing -> CVar x
|
||||
toCExp syns (ERecProj _ f (EVar x)) = case lookup x syns of
|
||||
Just y -> CVar $ recProj2Var y f
|
||||
Nothing -> CVar $ recProj2Var x f
|
||||
toCExp syns (EStructProj f (EVar x)) = case lookup x syns of
|
||||
Just y -> CVar $ recProj2Var y f
|
||||
Nothing -> CVar $ recProj2Var x f
|
||||
toCExp syns (ETmApp (ETmApp op e1) e2) = case op of
|
||||
(EBuiltin (BEEqual _)) -> CEq (toCExp syns e1) (toCExp syns e2)
|
||||
(EBuiltin BEAddInt64) -> CAdd (toCExp syns e1) (toCExp syns e2)
|
||||
(EBuiltin BESubInt64) -> CSub (toCExp syns e1) (toCExp syns e2)
|
||||
(ETyApp (EBuiltin BEAddNumeric) _) -> CAdd (toCExp syns e1) (toCExp syns e2)
|
||||
(ETyApp (EBuiltin BESubNumeric) _) -> CSub (toCExp syns e1) (toCExp syns e2)
|
||||
(ETmApp (ETyApp (EVal (Qualified _ _ (ExprValName "+"))) _) _) ->
|
||||
CAdd (toCExp syns e1) (toCExp syns e2)
|
||||
(ETmApp (ETyApp (EVal (Qualified _ _ (ExprValName "-"))) _) _) ->
|
||||
CSub (toCExp syns e1) (toCExp syns e2)
|
||||
_ -> error ("Builtin: " ++ show op)
|
||||
toCExp syns (ELocation _ e) = toCExp syns e
|
||||
toCExp _syns (EBuiltin (BEBool b)) = CBool b
|
||||
toCExp _syns (EBuiltin (BEInt64 i)) = CInt $ toInteger i
|
||||
toCExp _syns (EBuiltin (BENumeric i)) = CReal $ toRational $ numericDecimal i
|
||||
toCExp _syns e = error ("Conversion: " ++ show e)
|
||||
|
||||
instance ConstrExpr a => ConstrExpr (Cond a) where
|
||||
toCExp syns (Determined x) = toCExp syns x
|
||||
-- TODO: Can we assume this should always be a sum?
|
||||
toCExp syns (Conditional b x y) = CIf (toCExp syns b)
|
||||
(addMany $ map (toCExp syns) x)
|
||||
(addMany $ map (toCExp syns) y)
|
||||
|
||||
-- | Gather all free variables in a constraint expression.
|
||||
gatherFreeVars :: ConstraintExpr
|
||||
-- ^ The constraint expression to traverse.
|
||||
-> [ExprVarName]
|
||||
gatherFreeVars (CBool _) = []
|
||||
gatherFreeVars (CInt _) = []
|
||||
gatherFreeVars (CReal _) = []
|
||||
gatherFreeVars (CVar x) = [x]
|
||||
gatherFreeVars (CAdd e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2
|
||||
gatherFreeVars (CSub e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2
|
||||
gatherFreeVars (CEq e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2
|
||||
gatherFreeVars (CAnd e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2
|
||||
gatherFreeVars (CNot e) = gatherFreeVars e
|
||||
gatherFreeVars (CIf e1 e2 e3) = gatherFreeVars e1 `union`
|
||||
gatherFreeVars e2 `union` gatherFreeVars e3
|
||||
|
||||
-- | Gather the variable names bound within a skolem variable.
|
||||
skol2var :: Skolem
|
||||
-- ^ The skolem variable to handle.
|
||||
-> [ExprVarName]
|
||||
skol2var (SkolVar x) = [x]
|
||||
skol2var (SkolRec x fs) = map (recProj2Var x) fs
|
||||
|
||||
-- | Squash a record projection into a single variable name.
|
||||
recProj2Var :: ExprVarName
|
||||
-- ^ The variable on which is being projected.
|
||||
-> FieldName
|
||||
-- ^ The field name which is being projected.
|
||||
-> ExprVarName
|
||||
recProj2Var (ExprVarName x) (FieldName f) = ExprVarName (x `T.append` "." `T.append` f)
|
||||
|
||||
-- | The set of constraints to be solved.
|
||||
data ConstraintSet = ConstraintSet
|
||||
{ _cVars :: ![ExprVarName]
|
||||
-- ^ The variables to be declared.
|
||||
, _cCres :: ![ConstraintExpr]
|
||||
-- ^ The field values of all newly created contracts.
|
||||
, _cArcs :: ![ConstraintExpr]
|
||||
-- ^ The field values of all archived contracts.
|
||||
, _cCtrs :: ![(ConstraintExpr, ConstraintExpr)]
|
||||
-- ^ Additional equality constraints.
|
||||
}
|
||||
deriving Show
|
||||
|
||||
-- | Filters a single update to match the given template, and takes out the
|
||||
-- field of interest. The update gets converted into a constraint expression.
|
||||
-- It returns either a create or an archive update.
|
||||
filterUpd :: Qualified TypeConName
|
||||
-- ^ The template name to filter against.
|
||||
-> [(ExprVarName, ExprVarName)]
|
||||
-- ^ The contract name synonyms, along with their current alias.
|
||||
-> FieldName
|
||||
-- ^ The field name to be verified.
|
||||
-> Upd
|
||||
-- ^ The update expression to convert and filter.
|
||||
-> (Maybe ConstraintExpr, Maybe ConstraintExpr)
|
||||
filterUpd tem syns f UpdCreate{..} = if tem == _creTemp
|
||||
then (Just (toCExp syns $ fromJust $ lookup f _creField), Nothing)
|
||||
else (Nothing, Nothing)
|
||||
filterUpd tem syns f UpdArchive{..} = if tem == _arcTemp
|
||||
then (Nothing, Just (toCExp syns $ fromJust $ lookup f _arcField))
|
||||
else (Nothing, Nothing)
|
||||
|
||||
-- | Filters and converts a conditional update into (possibly two) constraint
|
||||
-- expressions, while splitting it into create and archive updates.
|
||||
filterCondUpd :: Qualified TypeConName
|
||||
-- ^ The template name to filter against
|
||||
-> [(ExprVarName, ExprVarName)]
|
||||
-- ^ The contract name synonyms, along with their current alias.
|
||||
-> FieldName
|
||||
-- ^ The field name to be verified.
|
||||
-> Cond Upd
|
||||
-- ^ The conditional update expression to convert and filter.
|
||||
-> ([ConstraintExpr], [ConstraintExpr])
|
||||
filterCondUpd tem syns f (Determined x) = both maybeToList $ filterUpd tem syns f x
|
||||
filterCondUpd tem syns f (Conditional b xs ys) =
|
||||
let cb = toCExp syns b
|
||||
(cxcre,cxarc) = both (addMany . concat) $ unzip $ map (filterCondUpd tem syns f) xs
|
||||
(cycre,cyarc) = both (addMany . concat) $ unzip $ map (filterCondUpd tem syns f) ys
|
||||
in ( [CIf cb cxcre cycre]
|
||||
, [CIf cb cxarc cyarc] )
|
||||
|
||||
-- | Filter the given set of skolems, to only include those that occur in the
|
||||
-- given constraint expressions. Remove duplicates in the process.
|
||||
filterVars :: [ExprVarName]
|
||||
-- ^ The list of skolems to filter.
|
||||
-> [ConstraintExpr]
|
||||
-- ^ The constraint expressions in which the skolems should occur.
|
||||
-> [ExprVarName]
|
||||
filterVars vars cexprs =
|
||||
let freevars = foldl' (\fv e -> fv `union` gatherFreeVars e) [] cexprs
|
||||
in freevars `intersect` vars
|
||||
|
||||
-- | Construct a list of all contract name synonyms, along with their current
|
||||
-- alias.
|
||||
constructSynonyms :: [(ExprVarName, [ExprVarName])]
|
||||
-- ^ The current contract names, along with any previous synonyms.
|
||||
-> [(ExprVarName, ExprVarName)]
|
||||
constructSynonyms = foldl step []
|
||||
where
|
||||
step :: [(ExprVarName, ExprVarName)] -> (ExprVarName, [ExprVarName])
|
||||
-> [(ExprVarName, ExprVarName)]
|
||||
step acc (cur, prevs) = acc ++ map (, cur) prevs
|
||||
|
||||
-- | Constructs a constraint set from the generator environment, together with
|
||||
-- the template name, the choice and field to be verified.
|
||||
constructConstr :: Env 'Solving
|
||||
-- ^ The generator environment to convert.
|
||||
-> Qualified TypeConName
|
||||
-- ^ The template name of the choice to be verified.
|
||||
-> ChoiceName
|
||||
-- ^ The choice name to be verified.
|
||||
-> Qualified TypeConName
|
||||
-- ^ The template name of the field to be verified.
|
||||
-> FieldName
|
||||
-- ^ The field name to be verified.
|
||||
-> ConstraintSet
|
||||
constructConstr env chtem ch ftem f =
|
||||
case HM.lookup (UpdChoice chtem ch) (_envschs env) of
|
||||
Just ChoiceData{..} ->
|
||||
let upds = _ussUpdate $ _cdUpds (EVar _cdSelf) (EVar _cdThis) (EVar _cdArgs)
|
||||
vars = concatMap skol2var (_envsskol env)
|
||||
syns = constructSynonyms $ HM.elems $ _envscids env
|
||||
ctrs = map (both (toCExp syns)) $ _envsctrs env
|
||||
(cres, arcs) = foldl
|
||||
(\(cs,as) upd -> let (cs',as') = filterCondUpd ftem syns f upd in (cs ++ cs',as ++ as'))
|
||||
([],[]) upds
|
||||
in ConstraintSet vars cres arcs ctrs
|
||||
Nothing -> error ("Choice not found " ++ show ch)
|
||||
|
||||
-- | Convert a constraint expression into an SMT expression from the solving library.
|
||||
cexp2sexp :: [(ExprVarName,S.SExpr)]
|
||||
-- ^ The set of variable names, mapped to their corresponding SMT counterparts.
|
||||
-> ConstraintExpr
|
||||
-- ^ The constraint expression to convert.
|
||||
-> IO S.SExpr
|
||||
cexp2sexp _vars (CBool b) = return $ S.bool b
|
||||
cexp2sexp _vars (CInt i) = return $ S.int i
|
||||
cexp2sexp _vars (CReal i) = return $ S.real i
|
||||
cexp2sexp vars (CVar x) = case lookup x vars of
|
||||
Just exp -> return exp
|
||||
Nothing -> error ("Impossible: variable not found " ++ show x)
|
||||
cexp2sexp vars (CAdd ce1 ce2) = do
|
||||
se1 <- cexp2sexp vars ce1
|
||||
se2 <- cexp2sexp vars ce2
|
||||
return $ S.add se1 se2
|
||||
cexp2sexp vars (CSub ce1 ce2) = do
|
||||
se1 <- cexp2sexp vars ce1
|
||||
se2 <- cexp2sexp vars ce2
|
||||
return $ S.sub se1 se2
|
||||
cexp2sexp vars (CEq ce1 ce2) = do
|
||||
se1 <- cexp2sexp vars ce1
|
||||
se2 <- cexp2sexp vars ce2
|
||||
return $ S.eq se1 se2
|
||||
cexp2sexp vars (CAnd ce1 ce2) = do
|
||||
se1 <- cexp2sexp vars ce1
|
||||
se2 <- cexp2sexp vars ce2
|
||||
return $ S.and se1 se2
|
||||
cexp2sexp vars (CNot ce) = do
|
||||
se <- cexp2sexp vars ce
|
||||
return $ S.not se
|
||||
cexp2sexp vars (CIf ce1 ce2 ce3) = do
|
||||
se1 <- cexp2sexp vars ce1
|
||||
se2 <- cexp2sexp vars ce2
|
||||
se3 <- cexp2sexp vars ce3
|
||||
return $ S.ite se1 se2 se3
|
||||
|
||||
-- | Declare a list of variables for the SMT solver. Returns a list of the
|
||||
-- declared variables, together with their corresponding SMT counterparts.
|
||||
declareVars :: S.Solver
|
||||
-- ^ The SMT solver.
|
||||
-> [ExprVarName]
|
||||
-- ^ The variables to be declared.
|
||||
-> IO [(ExprVarName,S.SExpr)]
|
||||
declareVars s xs = zip xs <$> mapM (\x -> S.declare s (var2str x) S.tReal) xs
|
||||
where
|
||||
var2str :: ExprVarName -> String
|
||||
var2str (ExprVarName x) = T.unpack x
|
||||
|
||||
-- | Assert the additional equality constraints. Binds and returns any
|
||||
-- additional required variables.
|
||||
declareCtrs :: S.Solver
|
||||
-- ^ The SMT solver.
|
||||
-> (String -> IO ())
|
||||
-- ^ Function for debugging printouts.
|
||||
-> [(ExprVarName,S.SExpr)]
|
||||
-- ^ The set of variable names, mapped to their corresponding SMT counterparts.
|
||||
-> [(ConstraintExpr, ConstraintExpr)]
|
||||
-- ^ The equality constraints to be declared.
|
||||
-> IO [(ExprVarName,S.SExpr)]
|
||||
declareCtrs sol debug cvars1 ctrs = do
|
||||
let edges = map (\(l,r) -> (l,r,gatherFreeVars l ++ gatherFreeVars r)) ctrs
|
||||
components = conn_comp edges
|
||||
useful_nodes = map fst cvars1
|
||||
useful_components = filter
|
||||
(\comp -> let comp_vars = concatMap (\(_,_,vars) -> vars) comp
|
||||
in not $ null $ intersect comp_vars useful_nodes)
|
||||
components
|
||||
useful_equalities = concatMap (map (\(l,r,_) -> (l,r))) useful_components
|
||||
required_vars =
|
||||
nubOrd (concatMap (concatMap (\(_,_,vars) -> vars)) useful_components)
|
||||
\\ useful_nodes
|
||||
cvars2 <- declareVars sol required_vars
|
||||
mapM_ (declare $ cvars1 ++ cvars2) useful_equalities
|
||||
return cvars2
|
||||
where
|
||||
-- | Compute connected components of the equality constraints graph.
|
||||
-- Two edges are adjacent when at least one of their nodes shares a variable.
|
||||
conn_comp :: [(ConstraintExpr,ConstraintExpr,[ExprVarName])]
|
||||
-- ^ The edges of the graph, annotated with the contained variables.
|
||||
-> [[(ConstraintExpr,ConstraintExpr,[ExprVarName])]]
|
||||
conn_comp [] = []
|
||||
conn_comp (edge:edges) = let (comp,rem) = cc_step edges edge
|
||||
in comp : conn_comp rem
|
||||
|
||||
-- | Compute the strongly connected component containing a given edge from
|
||||
-- the graph, as well as the remaining edges which do not belong to this
|
||||
-- component.
|
||||
cc_step :: [(ConstraintExpr,ConstraintExpr,[ExprVarName])]
|
||||
-- ^ The edges of the graph, which do not yet belong to any component.
|
||||
-> (ConstraintExpr,ConstraintExpr,[ExprVarName])
|
||||
-- ^ The current edge for which the component is being computed.
|
||||
-> ( [(ConstraintExpr,ConstraintExpr,[ExprVarName])]
|
||||
-- ^ The computed connected component.
|
||||
, [(ConstraintExpr,ConstraintExpr,[ExprVarName])] )
|
||||
-- ^ The remaining edges which do not belong to the connected component.
|
||||
cc_step [] _ = ([],[])
|
||||
cc_step edges0 (l,r,vars) =
|
||||
let (neighbors,edges1) = partition (\(_,_,vars') -> not $ null $ intersect vars vars') edges0
|
||||
in foldl (\(conn,edges2) edge -> first (conn ++) $ cc_step edges2 edge)
|
||||
((l,r,vars):neighbors,edges1) neighbors
|
||||
|
||||
declare :: [(ExprVarName,S.SExpr)] -> (ConstraintExpr, ConstraintExpr) -> IO ()
|
||||
declare vars (cexp1, cexp2) = do
|
||||
sexp1 <- cexp2sexp vars cexp1
|
||||
sexp2 <- cexp2sexp vars cexp2
|
||||
debug ("Assert: " ++ S.ppSExpr sexp1 (" = " ++ S.ppSExpr sexp2 ""))
|
||||
S.assert sol (sexp1 `S.eq` sexp2)
|
||||
|
||||
-- | Data type denoting the outcome of the solver.
|
||||
data Result
|
||||
= Success
|
||||
-- ^ The total field amount remains preserved.
|
||||
| Fail [(S.SExpr, S.Value)]
|
||||
-- ^ The total field amound does not remain the same. A counter example is
|
||||
-- provided.
|
||||
| Unknown
|
||||
-- ^ The result is inconclusive.
|
||||
deriving Eq
|
||||
|
||||
instance Show Result where
|
||||
show Success = "Success!"
|
||||
show (Fail cs) = "Fail. Counter example:" ++ foldl (flip step) "" cs
|
||||
where
|
||||
step :: (S.SExpr, S.Value) -> String -> String
|
||||
step (var, val) str = ("\n" ++) $ S.ppSExpr var $ (" = " ++) $ S.ppSExpr (S.value val) str
|
||||
show Unknown = "Inconclusive."
|
||||
|
||||
-- | Solve a give constraint set. Prints 'unsat' when the constraint set is
|
||||
-- valid. It asserts that the set of created and archived contracts are not
|
||||
-- equal.
|
||||
solveConstr :: FilePath
|
||||
-- ^ The path to the constraint solver.
|
||||
-> (String -> IO ())
|
||||
-- ^ Function for debugging printouts.
|
||||
-> ConstraintSet
|
||||
-- ^ The constraint set to solve.
|
||||
-> IO Result
|
||||
solveConstr spath debug ConstraintSet{..} = do
|
||||
log <- S.newLogger 1
|
||||
sol <- S.newSolver spath ["-in"] (Just log)
|
||||
vars1 <- declareVars sol $ filterVars _cVars (_cCres ++ _cArcs)
|
||||
vars2 <- declareCtrs sol debug vars1 _cCtrs
|
||||
let vars = vars1 ++ vars2
|
||||
cre <- foldl S.add (S.real 0.0) <$> mapM (cexp2sexp vars) _cCres
|
||||
arc <- foldl S.add (S.real 0.0) <$> mapM (cexp2sexp vars) _cArcs
|
||||
S.assert sol (S.not (cre `S.eq` arc))
|
||||
S.check sol >>= \case
|
||||
S.Sat -> do
|
||||
counter <- S.getExprs sol $ map snd vars
|
||||
return $ Fail counter
|
||||
S.Unsat -> return Success
|
||||
S.Unknown -> return Unknown
|
||||
211
compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Subst.hs
Normal file
211
compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Subst.hs
Normal file
@ -0,0 +1,211 @@
|
||||
-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
-- | Term substitions for DAML LF static verification
|
||||
module DA.Daml.LF.Verify.Subst
|
||||
( ExprSubst
|
||||
, singleExprSubst
|
||||
, singleTypeSubst
|
||||
, createExprSubst
|
||||
, SubstTm(..)
|
||||
, SubstTy(..)
|
||||
, InstPR(..)
|
||||
) where
|
||||
|
||||
import Control.Lens hiding (Context)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import DA.Daml.LF.Ast
|
||||
import DA.Daml.LF.Ast.Type
|
||||
|
||||
-- | Substitution of expressions for expression variables.
|
||||
type ExprSubst = Map.Map ExprVarName Expr
|
||||
|
||||
-- | Create an expression substitution from a single variable and expression.
|
||||
singleExprSubst :: ExprVarName
|
||||
-- ^ The expression variable to substitute.
|
||||
-> Expr
|
||||
-- ^ The expression to substitute with.
|
||||
-> ExprSubst
|
||||
singleExprSubst = Map.singleton
|
||||
|
||||
-- | Create a type substitution from a single type variable and type.
|
||||
singleTypeSubst :: TypeVarName
|
||||
-- ^ The type variable to substitute.
|
||||
-> Type
|
||||
-- ^ The type to substitute with.
|
||||
-> Subst
|
||||
singleTypeSubst = Map.singleton
|
||||
|
||||
-- | Create an expression substitution from a list of variables and expressions.
|
||||
createExprSubst :: [(ExprVarName,Expr)]
|
||||
-- ^ The variables to substitute, together with the expressions to replace them with.
|
||||
-> ExprSubst
|
||||
createExprSubst = Map.fromList
|
||||
|
||||
-- | Get the domain from an expression substitution.
|
||||
substDom :: ExprSubst
|
||||
-- ^ The substitution to analyse.
|
||||
-> [ExprVarName]
|
||||
substDom = Map.keys
|
||||
|
||||
-- | A class covering the data types to which an expression substitution can be applied.
|
||||
class SubstTm a where
|
||||
-- | Apply an expression substitution.
|
||||
substituteTm :: ExprSubst
|
||||
-- ^ The expression substitution to apply.
|
||||
-> a
|
||||
-- ^ The data to apply the substitution to.
|
||||
-> a
|
||||
|
||||
-- | A class covering the data types to which a type substitution can be applied.
|
||||
class SubstTy a where
|
||||
-- | Apply an type substitution.
|
||||
substituteTy :: Subst
|
||||
-- ^ The type substitution to apply.
|
||||
-> a
|
||||
-- ^ The data to apply the substitution to.
|
||||
-> a
|
||||
|
||||
-- TODO: We assume that for any substitution x |-> e : x notin e
|
||||
-- and a |-> t : a notin t.
|
||||
instance SubstTm Expr where
|
||||
substituteTm s = \case
|
||||
EVar x
|
||||
| Just e <- Map.lookup x s -> e
|
||||
| otherwise -> EVar x
|
||||
ERecCon t fs -> ERecCon t $ map (over _2 (substituteTm s)) fs
|
||||
ERecProj t f e -> ERecProj t f $ substituteTm s e
|
||||
ERecUpd t f e1 e2 -> ERecUpd t f (substituteTm s e1) (substituteTm s e2)
|
||||
EVariantCon t v e -> EVariantCon t v (substituteTm s e)
|
||||
EStructCon fs -> EStructCon $ map (over _2 (substituteTm s)) fs
|
||||
EStructProj f e -> EStructProj f (substituteTm s e)
|
||||
EStructUpd f e1 e2 -> EStructUpd f (substituteTm s e1) (substituteTm s e2)
|
||||
ETmApp e1 e2 -> ETmApp (substituteTm s e1) (substituteTm s e2)
|
||||
ETyApp e t -> ETyApp (substituteTm s e) t
|
||||
ETmLam (x,t) e -> if x `elem` substDom s
|
||||
then ETmLam (x,t) e
|
||||
else ETmLam (x,t) (substituteTm s e)
|
||||
ETyLam (a,k) e -> ETyLam (a,k) (substituteTm s e)
|
||||
ECase e cs -> ECase (substituteTm s e)
|
||||
$ map (\CaseAlternative{..} -> CaseAlternative altPattern (substituteTm s altExpr)) cs
|
||||
ELet Binding{..} e -> ELet (Binding bindingBinder $ substituteTm s bindingBound)
|
||||
(substituteTm s e)
|
||||
ECons t e1 e2 -> ECons t (substituteTm s e1) (substituteTm s e2)
|
||||
ESome t e -> ESome t (substituteTm s e)
|
||||
EToAny t e -> EToAny t (substituteTm s e)
|
||||
EFromAny t e -> EFromAny t (substituteTm s e)
|
||||
EUpdate u -> EUpdate $ substituteTm s u
|
||||
ELocation l e -> ELocation l (substituteTm s e)
|
||||
e -> e
|
||||
|
||||
instance SubstTm Update where
|
||||
substituteTm s = \case
|
||||
UPure t e -> UPure t $ substituteTm s e
|
||||
UBind Binding{..} e -> UBind (Binding bindingBinder $ substituteTm s bindingBound)
|
||||
(substituteTm s e)
|
||||
UCreate t e -> UCreate t $ substituteTm s e
|
||||
UExercise t c e1 a e2 -> UExercise t c (substituteTm s e1) a (substituteTm s e2)
|
||||
UFetch t e -> UFetch t $ substituteTm s e
|
||||
UEmbedExpr t e -> UEmbedExpr t $ substituteTm s e
|
||||
u -> u
|
||||
|
||||
instance SubstTm a => SubstTm (Maybe a) where
|
||||
substituteTm s m = substituteTm s <$> m
|
||||
|
||||
instance SubstTy Expr where
|
||||
substituteTy s = \case
|
||||
ERecCon t fs -> ERecCon (substituteTy s t) $ map (over _2 (substituteTy s)) fs
|
||||
ERecProj t f e -> ERecProj (substituteTy s t) f $ substituteTy s e
|
||||
ERecUpd t f e1 e2 -> ERecUpd (substituteTy s t) f (substituteTy s e1)
|
||||
(substituteTy s e2)
|
||||
EVariantCon t v e -> EVariantCon (substituteTy s t) v (substituteTy s e)
|
||||
EStructCon fs -> EStructCon $ map (over _2 (substituteTy s)) fs
|
||||
EStructProj f e -> EStructProj f $ substituteTy s e
|
||||
EStructUpd f e1 e2 -> EStructUpd f (substituteTy s e1) (substituteTy s e2)
|
||||
ETmApp e1 e2 -> ETmApp (substituteTy s e1) (substituteTy s e2)
|
||||
ETyApp e t -> ETyApp (substituteTy s e) (substitute s t)
|
||||
ETmLam (n, t) e -> ETmLam (n, substitute s t) (substituteTy s e)
|
||||
ETyLam b e -> ETyLam b $ substituteTy s e
|
||||
ECase e cs -> ECase (substituteTy s e) (map (substituteTy s) cs)
|
||||
ELet Binding{..} e -> ELet (Binding (over _2 (substitute s) bindingBinder) (substituteTy s bindingBound))
|
||||
(substituteTy s e)
|
||||
ENil t -> ENil (substitute s t)
|
||||
ECons t e1 e2 -> ECons (substitute s t) (substituteTy s e1) (substituteTy s e2)
|
||||
ESome t e -> ESome (substitute s t) (substituteTy s e)
|
||||
ENone t -> ENone (substitute s t)
|
||||
EToAny t e -> EToAny (substitute s t) (substituteTy s e)
|
||||
EFromAny t e -> EFromAny (substitute s t) (substituteTy s e)
|
||||
ETypeRep t -> ETypeRep (substitute s t)
|
||||
EUpdate u -> EUpdate (substituteTy s u)
|
||||
ELocation l e -> ELocation l (substituteTy s e)
|
||||
e -> e
|
||||
|
||||
instance SubstTy Update where
|
||||
substituteTy s = \case
|
||||
UPure t e -> UPure (substitute s t) (substituteTy s e)
|
||||
UBind Binding{..} e -> UBind (Binding (over _2 (substitute s) bindingBinder) (substituteTy s bindingBound))
|
||||
(substituteTy s e)
|
||||
UCreate n e -> UCreate n (substituteTy s e)
|
||||
UExercise n c e1 a e2 -> UExercise n c (substituteTy s e1) a (substituteTy s e2)
|
||||
UFetch n e -> UFetch n (substituteTy s e)
|
||||
UEmbedExpr t e -> UEmbedExpr (substitute s t) (substituteTy s e)
|
||||
u -> u
|
||||
|
||||
instance SubstTy TypeConApp where
|
||||
substituteTy s (TypeConApp n ts) = TypeConApp n (map (substitute s) ts)
|
||||
|
||||
instance SubstTy CaseAlternative where
|
||||
substituteTy s (CaseAlternative p e) = CaseAlternative p (substituteTy s e)
|
||||
|
||||
-- | A class covering the data types containing package references which can be
|
||||
-- instantiated..
|
||||
class InstPR a where
|
||||
-- | Instantiate `PRSelf` with the given package reference.
|
||||
instPRSelf :: PackageRef
|
||||
-- ^ The package reference to substitute with.
|
||||
-> a
|
||||
-- ^ The data type to substitute in.
|
||||
-> a
|
||||
|
||||
instance InstPR (Qualified a) where
|
||||
instPRSelf pac qx@(Qualified pac' mod x) = case pac' of
|
||||
PRSelf -> Qualified pac mod x
|
||||
_ -> qx
|
||||
|
||||
instance InstPR Expr where
|
||||
instPRSelf pac = \case
|
||||
EVal val -> EVal (instPRSelf pac val)
|
||||
ERecCon t fs -> ERecCon t $ map (over _2 (instPRSelf pac)) fs
|
||||
ERecProj t f e -> ERecProj t f $ instPRSelf pac e
|
||||
ERecUpd t f e1 e2 -> ERecUpd t f (instPRSelf pac e1) (instPRSelf pac e2)
|
||||
EVariantCon t v e -> EVariantCon t v (instPRSelf pac e)
|
||||
EStructCon fs -> EStructCon $ map (over _2 (instPRSelf pac)) fs
|
||||
EStructProj f e -> EStructProj f (instPRSelf pac e)
|
||||
EStructUpd f e1 e2 -> EStructUpd f (instPRSelf pac e1) (instPRSelf pac e2)
|
||||
ETmApp e1 e2 -> ETmApp (instPRSelf pac e1) (instPRSelf pac e2)
|
||||
ETyApp e t -> ETyApp (instPRSelf pac e) t
|
||||
ETmLam b e -> ETmLam b (instPRSelf pac e)
|
||||
ETyLam b e -> ETyLam b (instPRSelf pac e)
|
||||
ECase e cs -> ECase (instPRSelf pac e)
|
||||
$ map (\CaseAlternative{..} -> CaseAlternative altPattern (instPRSelf pac altExpr)) cs
|
||||
ELet Binding{..} e -> ELet (Binding bindingBinder $ instPRSelf pac bindingBound)
|
||||
(instPRSelf pac e)
|
||||
ECons t e1 e2 -> ECons t (instPRSelf pac e1) (instPRSelf pac e2)
|
||||
ESome t e -> ESome t (instPRSelf pac e)
|
||||
EToAny t e -> EToAny t (instPRSelf pac e)
|
||||
EFromAny t e -> EFromAny t (instPRSelf pac e)
|
||||
EUpdate u -> EUpdate $ instPRSelf pac u
|
||||
ELocation l e -> ELocation l (instPRSelf pac e)
|
||||
e -> e
|
||||
|
||||
instance InstPR Update where
|
||||
instPRSelf pac = \case
|
||||
UPure t e -> UPure t (instPRSelf pac e)
|
||||
UBind Binding{..} e -> UBind (Binding bindingBinder $ instPRSelf pac bindingBound)
|
||||
(instPRSelf pac e)
|
||||
UCreate tem arg -> UCreate (instPRSelf pac tem) (instPRSelf pac arg)
|
||||
UExercise tem ch cid act arg -> UExercise (instPRSelf pac tem) ch
|
||||
(instPRSelf pac cid) (instPRSelf pac <$> act) (instPRSelf pac arg)
|
||||
UFetch tem cid -> UFetch (instPRSelf pac tem) (instPRSelf pac cid)
|
||||
UEmbedExpr t e -> UEmbedExpr t (instPRSelf pac e)
|
||||
u -> u
|
||||
98
compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs
Normal file
98
compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs
Normal file
@ -0,0 +1,98 @@
|
||||
-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
module DA.Daml.LF.Verify.Tests
|
||||
( mainTest
|
||||
) where
|
||||
|
||||
import System.FilePath
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
|
||||
import DA.Daml.LF.Ast.Base
|
||||
import DA.Daml.LF.Verify
|
||||
import DA.Daml.LF.Verify.Solve
|
||||
import DA.Bazel.Runfiles
|
||||
|
||||
mainTest :: IO ()
|
||||
mainTest = defaultMain $ testGroup "DA.Daml.LF.Verify"
|
||||
[ quickstartTests
|
||||
, conditionalTests
|
||||
]
|
||||
|
||||
quickstartTests :: TestTree
|
||||
quickstartTests = testGroup "Quickstart"
|
||||
[ testCase "Iou_Split" $ do
|
||||
quickstartDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/quickstart.dar")
|
||||
let tmpl = TypeConName ["Iou"]
|
||||
choice = ChoiceName "Iou_Split"
|
||||
field = FieldName "amount"
|
||||
result <- verify quickstartDar debug tmpl choice tmpl field
|
||||
assertEqual "Verification failed for Iou_Split - amount"
|
||||
Success result
|
||||
, testCase "Iou_Merge" $ do
|
||||
quickstartDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/quickstart.dar")
|
||||
let tmpl = TypeConName ["Iou"]
|
||||
choice = ChoiceName "Iou_Merge"
|
||||
field = FieldName "amount"
|
||||
result <- verify quickstartDar debug tmpl choice tmpl field
|
||||
assertEqual "Verification failed for Iou_Merge - amount"
|
||||
Success result
|
||||
]
|
||||
|
||||
conditionalTests :: TestTree
|
||||
conditionalTests = testGroup "Conditionals"
|
||||
[ testCase "Success A" $ do
|
||||
condDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/conditionals.dar")
|
||||
let tmpl = TypeConName ["Iou"]
|
||||
choice = ChoiceName "SuccA"
|
||||
field = FieldName "content"
|
||||
result <- verify condDar debug tmpl choice tmpl field
|
||||
assertEqual "Verification failed for SuccA - content"
|
||||
Success result
|
||||
, testCase "Success B" $ do
|
||||
condDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/conditionals.dar")
|
||||
let tmpl = TypeConName ["Iou"]
|
||||
choice = ChoiceName "SuccB"
|
||||
field = FieldName "content"
|
||||
result <- verify condDar debug tmpl choice tmpl field
|
||||
assertEqual "Verification failed for SuccB - content"
|
||||
Success result
|
||||
, testCase "Success C" $ do
|
||||
condDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/conditionals.dar")
|
||||
let tmpl = TypeConName ["Iou"]
|
||||
choice = ChoiceName "SuccC"
|
||||
field = FieldName "content"
|
||||
result <- verify condDar debug tmpl choice tmpl field
|
||||
assertEqual "Verification failed for SuccC - content"
|
||||
Success result
|
||||
, testCase "Success D" $ do
|
||||
condDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/conditionals.dar")
|
||||
let tmpl = TypeConName ["Iou"]
|
||||
choice = ChoiceName "SuccD"
|
||||
field = FieldName "content"
|
||||
result <- verify condDar debug tmpl choice tmpl field
|
||||
assertEqual "Verification failed for SuccD - content"
|
||||
Success result
|
||||
, testCase "Fail A" $ do
|
||||
condDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/conditionals.dar")
|
||||
let tmpl = TypeConName ["Iou"]
|
||||
choice = ChoiceName "FailA"
|
||||
field = FieldName "content"
|
||||
verify condDar debug tmpl choice tmpl field >>= \case
|
||||
Success -> assertFailure "Verification wrongfully passed for FailA - content"
|
||||
Unknown -> assertFailure "Verification inconclusive for FailA - content"
|
||||
Fail _ -> return ()
|
||||
, testCase "Fail B" $ do
|
||||
condDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/conditionals.dar")
|
||||
let tmpl = TypeConName ["Iou"]
|
||||
choice = ChoiceName "FailB"
|
||||
field = FieldName "content"
|
||||
verify condDar debug tmpl choice tmpl field >>= \case
|
||||
Success -> assertFailure "Verification wrongfully passed for FailB - content"
|
||||
Unknown -> assertFailure "Verification inconclusive for FailB - content"
|
||||
Fail _ -> return ()
|
||||
]
|
||||
|
||||
debug :: String -> IO ()
|
||||
debug _ = return ()
|
||||
@ -116,6 +116,8 @@ let shared = rec {
|
||||
;
|
||||
};
|
||||
|
||||
z3 = pkgs.z3;
|
||||
|
||||
bazel-cc-toolchain = pkgs.callPackage ./tools/bazel-cc-toolchain {};
|
||||
};
|
||||
in shared // (if pkgs.stdenv.isLinux then {
|
||||
|
||||
@ -28,6 +28,7 @@ packages:
|
||||
- regex-base-0.94.0.0
|
||||
- regex-tdfa-1.3.1.0
|
||||
- shake-0.18.5
|
||||
- simple-smt-0.9.4
|
||||
# Core packages, need to be listed for integer-simple flags.
|
||||
- integer-simple-0.1.1.1
|
||||
- text-1.2.3.1
|
||||
|
||||
Loading…
Reference in New Issue
Block a user