Working testing framework, with some basic test cases

digital-asset · Gertjan423 · May 20, 2020 · Apr 7, 2020 · Apr 8, 2020 · Apr 9, 2020
commit a33365cb7621aff9ee6e795304a3a56c9b8189ac
diff --git a/compiler/daml-lf-verify/BUILD.bazel b/compiler/daml-lf-verify/BUILD.bazel
@@ -1,7 +1,7 @@
 # Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
 # SPDX-License-Identifier: Apache-2.0
 
-load("//bazel_tools:haskell.bzl", "da_haskell_binary")
+load("//bazel_tools:haskell.bzl", "da_haskell_binary", "da_haskell_library", "da_haskell_test")
 
 da_haskell_binary(
     name = "daml-lf-verify",
@@ -45,3 +45,69 @@ da_haskell_binary(
         "//libs-haskell/da-hs-base",
     ],
 )
+
+da_haskell_library(
+    name = "daml-lf-verify-lib",
+    srcs = glob(["src/**/*.hs"]),
+    data = [
+        "@z3_nix//:bin/z3",
+    ],
+    hackage_deps = [
+        "aeson",
+        "base",
+        "bytestring",
+        "containers",
+        "deepseq",
+        "Decimal",
+        "extra",
+        "filepath",
+        "ghc-lib-parser",
+        "hashable",
+        "lens",
+        "mtl",
+        "optparse-applicative",
+        "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",
+    ],
+)
+
+da_haskell_test(
+    name = "verify-tests",
+    srcs = glob(["tests/**/*.hs"]),
+    data = glob(["data/*.dar"]),
+    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",
+    ],
+)
+
diff --git a/compiler/daml-lf-verify/data/conditionals.dar b/compiler/daml-lf-verify/data/conditionals.dar
diff --git a/compiler/daml-lf-verify/data/quickstart.dar b/compiler/daml-lf-verify/data/quickstart.dar
diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs
@@ -9,6 +9,7 @@ module DA.Daml.LF.Verify
   , verify
   ) where
 
+import Control.Monad (when)
 import Data.Text
 import Options.Applicative
 
@@ -19,22 +20,24 @@ 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 [pack optChoiceTmpl]
       choiceName = ChoiceName (pack optChoiceName)
       fieldTmpl = TypeConName [pack optFieldTmpl]
       fieldName = FieldName (pack optFieldName)
-  solver <- locateRunfiles "z3_nix/bin/z3"
-  pkgs <- readPackages [optInputDar]
-  verify pkgs solver choiceTmpl choiceName fieldTmpl fieldName >>= print
+  result <- verify optInputDar True choiceTmpl choiceName fieldTmpl fieldName
+  print result
 
 -- | Execute the full verification pipeline.
-verify :: [(PackageId, (Package, Maybe PackageName))]
-  -- ^ The packages to load.
-  -> FilePath
-  -- ^ The solver to use.
+verify :: FilePath
+  -- ^ The DAR file to load.
+  -> Bool
+  -- ^ Enable print outs.
   -> TypeConName
   -- ^ The template in which the given choice is defined.
   -> ChoiceName
@@ -44,27 +47,29 @@ verify :: [(PackageId, (Package, Maybe PackageName))]
   -> FieldName
   -- ^ The field to be verified.
   -> IO Result
-verify pkgs solver choiceTmpl choiceName fieldTmpl fieldName = do
-  putStrLn "Start value gathering"
+verify dar verbose choiceTmpl choiceName fieldTmpl fieldName = do
+  pkgs <- readPackages [dar]
+  solver <- getSolver
+  when verbose $ putStrLn "Start value gathering"
   case runEnv (genPackages pkgs) (emptyEnv :: Env 'ValueGathering) of
     Left err-> do
       putStrLn "Value phase finished with error: "
       print err
       return Unknown
     Right env1 -> do
-      putStrLn "Start value solving"
+      when verbose $ putStrLn "Start value solving"
       let env2 = solveValueReferences env1
-      putStrLn "Start choice gathering"
+      when verbose $ putStrLn "Start choice gathering"
       case runEnv (genPackages pkgs) env2 of
         Left err -> do
           putStrLn "Choice phase finished with error: "
           print err
           return Unknown
         Right env3 -> do
-          putStrLn "Start choice solving"
+          when verbose $ putStrLn "Start choice solving"
           let env4 = solveChoiceReferences env3
-          putStrLn "Start constraint solving phase"
+          when verbose $ putStrLn "Start constraint solving phase"
           let cset = constructConstr env4 choiceTmpl choiceName fieldTmpl fieldName
-          putStr "Create: " >> print (_cCres cset)
-          putStr "Archive: " >> print (_cArcs cset)
+          when verbose $ putStr "Create: " >> print (_cCres cset)
+          when verbose $ putStr "Archive: " >> print (_cArcs cset)
           solveConstr solver cset
diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs
@@ -14,7 +14,6 @@ module DA.Daml.LF.Verify.Generate
 import Control.Monad.Error.Class (catchError, throwError)
 import Data.Maybe (listToMaybe)
 import qualified Data.NameMap as NM
-import Debug.Trace
 
 import DA.Daml.LF.Ast hiding (lookupChoice)
 import DA.Daml.LF.Verify.Context
@@ -377,9 +376,10 @@ genForExercise tem ch cid par arg = do
   cidOut <- genExpr cid
   arout <- genExpr arg
   updSubst <- lookupChoice tem ch
-  -- TODO: Temporary solution
+  -- TODO: Temporary solution. To be fixed urgently.
   this <- lookupCid (_oExpr cidOut) `catchError`
-    (\_ -> trace ("Not found: " ++ show (_oExpr cidOut)) $ return $ ExprVarName "this")
+    -- (\_ -> trace ("Not found: " ++ show (_oExpr cidOut)) $ return $ ExprVarName "this")
+    (\_ -> return $ ExprVarName "this")
   -- 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)

diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs
@@ -276,6 +276,7 @@ data Result
   -- provided.
   | Unknown
   -- ^ The result is inconclusive.
+  deriving Eq
 
 instance Show Result where
   show Success = "Success!"

diff --git a/compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs b/compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs
@@ -0,0 +1,97 @@
+-- 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
+
+-- TODO: Build the dar files from within bazel, instead of passing them in manually.
+
+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/data/quickstart.dar")
+      let tmpl = TypeConName ["Iou"]
+          choice = ChoiceName "Iou_Split"
+          field = FieldName "amount"
+      result <- verify quickstartDar False tmpl choice tmpl field
+      assertEqual "Verification failed for Iou_Split - amount"
+        Success result
+  , testCase "Iou_Merge" $ do
+      quickstartDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/data/quickstart.dar")
+      let tmpl = TypeConName ["Iou"]
+          choice = ChoiceName "Iou_Merge"
+          field = FieldName "amount"
+      result <- verify quickstartDar False 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/data/conditionals.dar")
+      let tmpl = TypeConName ["Iou"]
+          choice = ChoiceName "SuccA"
+          field = FieldName "content"
+      result <- verify condDar False tmpl choice tmpl field
+      assertEqual "Verification failed for SuccA - content"
+        Success result
+  , testCase "Success B" $ do
+      condDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/data/conditionals.dar")
+      let tmpl = TypeConName ["Iou"]
+          choice = ChoiceName "SuccB"
+          field = FieldName "content"
+      result <- verify condDar False tmpl choice tmpl field
+      assertEqual "Verification failed for SuccB - content"
+        Success result
+  , testCase "Success C" $ do
+      condDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/data/conditionals.dar")
+      let tmpl = TypeConName ["Iou"]
+          choice = ChoiceName "SuccC"
+          field = FieldName "content"
+      result <- verify condDar False tmpl choice tmpl field
+      assertEqual "Verification failed for SuccC - content"
+        Success result
+  , testCase "Success D" $ do
+      condDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/data/conditionals.dar")
+      let tmpl = TypeConName ["Iou"]
+          choice = ChoiceName "SuccD"
+          field = FieldName "content"
+      result <- verify condDar False tmpl choice tmpl field
+      assertEqual "Verification failed for SuccD - content"
+        Success result
+  , testCase "Fail A" $ do
+      condDar <- locateRunfiles (mainWorkspace </> "compiler/daml-lf-verify/data/conditionals.dar")
+      let tmpl = TypeConName ["Iou"]
+          choice = ChoiceName "FailA"
+          field = FieldName "content"
+      verify condDar False 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/data/conditionals.dar")
+      let tmpl = TypeConName ["Iou"]
+          choice = ChoiceName "FailB"
+          field = FieldName "content"
+      verify condDar False tmpl choice tmpl field >>= \case
+        Success -> assertFailure "Verification wrongfully passed for FailB - content"
+        Unknown -> assertFailure "Verification inconclusive for FailB - content"
+        Fail _ -> return ()
+  ]