Merge pull request #758 from ramsay-t/main

Added Regression tests for Static Analysis before creating Incremental Static Analysis

marlowe-test/changelog.d/20231121_151418_ramsay.md

@@ -0,0 +1,4 @@
+### Added
+
+- Regression tests for Static Analysis. Specifically: explicit tests for each of the warning types, plus reachability and payouts on close. 
+

marlowe-test/marlowe-test.cabal

@@ -192,6 +192,8 @@ test-suite marlowe-test
     Spec.Marlowe.Serialization.CoreJson
     Spec.Marlowe.Serialization.ExtendedJson
     Spec.Marlowe.Service.Isabelle
+    Spec.Marlowe.StaticAnalysis
+    Spec.Marlowe.StaticAnalysis.Regression
 
   build-depends:
     , aeson >=2 && <3

marlowe-test/test/Spec.hs

@@ -21,6 +21,7 @@ import qualified Spec.Marlowe.Plutus (tests)
 import qualified Spec.Marlowe.Semantics (tests)
 import qualified Spec.Marlowe.Serialization (tests)
 import qualified Spec.Marlowe.Service.Isabelle (tests)
+import qualified Spec.Marlowe.StaticAnalysis (tests)
 
 -- | Timeout seconds for static analysis, which can take so much time on a complex contract
 --   that it exceeds hydra/CI resource limits, see SCP-4267.
@@ -49,4 +50,5 @@ tests =
     , Spec.Marlowe.Semantics.tests
     , Spec.Marlowe.Plutus.tests
     , Spec.Marlowe.Service.Isabelle.tests
+    , Spec.Marlowe.StaticAnalysis.tests
     ]

marlowe-test/test/Spec/Marlowe/StaticAnalysis.hs

@@ -0,0 +1,28 @@
+-----------------------------------------------------------------------------
+--
+-- Module      :  Spec.Marlowe.StaticAnalysis
+-- License     :  Apache 2.0
+--
+-- Stability   :  Experimental
+-- Portability :  Portable
+--
+
+-----------------------------------------------------------------------------
+
+-- | Tests of Marlowe semantics.
+module Spec.Marlowe.StaticAnalysis (
+  -- * Testing
+  tests,
+) where
+
+import Test.Tasty (TestTree, testGroup)
+
+import qualified Spec.Marlowe.StaticAnalysis.Regression (tests)
+
+-- | Run the tests.
+tests :: TestTree
+tests =
+  testGroup
+    "StaticAnalysis"
+    [ Spec.Marlowe.StaticAnalysis.Regression.tests
+    ]

marlowe-test/test/Spec/Marlowe/StaticAnalysis/Regression.hs

@@ -0,0 +1,211 @@
+-----------------------------------------------------------------------------
+--
+-- Module      :  Spec.Marlowe.StaticAnalysis.Regression
+-- License     :  Apache 2.0
+--
+-- Stability   :  Experimental
+-- Portability :  Portable
+--
+-----------------------------------------------------------------------------
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | Regression tests for the important behaviour of the Static Analysis functions.
+module Spec.Marlowe.StaticAnalysis.Regression (
+  -- * Testing
+  tests,
+) where
+
+import Language.Marlowe.Util (ada)
+import Test.Tasty (TestTree, testGroup)
+import Prelude
+
+import Data.Either (fromRight, isRight)
+import Data.Maybe (isNothing)
+import Language.Marlowe (
+  Action (..),
+  Case (..),
+  Contract (..),
+  Observation (..),
+  Payee (..),
+  Token (..),
+  TransactionWarning (..),
+  Value (..),
+ )
+import Language.Marlowe.Analysis.FSSemantics (warningsTrace)
+import Spec.Marlowe.Common (alicePk)
+import Test.Tasty.HUnit (assertBool, assertEqual, testCase)
+
+isTransactionPartialPay :: TransactionWarning -> Bool
+isTransactionPartialPay (TransactionPartialPay{}) = True
+isTransactionPartialPay _ = False
+
+isTransactionNonPositivePay :: TransactionWarning -> Bool
+isTransactionNonPositivePay (TransactionNonPositivePay{}) = True
+isTransactionNonPositivePay _ = False
+
+isTransactionNonPositiveDeposit :: TransactionWarning -> Bool
+isTransactionNonPositiveDeposit (TransactionNonPositiveDeposit{}) = True
+isTransactionNonPositiveDeposit _ = False
+
+isTransactionShadowing :: TransactionWarning -> Bool
+isTransactionShadowing (TransactionShadowing{}) = True
+isTransactionShadowing _ = False
+
+isTransactionAssertionFailed :: TransactionWarning -> Bool
+isTransactionAssertionFailed (TransactionAssertionFailed{}) = True
+isTransactionAssertionFailed _ = False
+
+getWarning :: Contract -> IO (Maybe TransactionWarning)
+getWarning contract =
+  do
+    res <- warningsTrace contract
+    return $ case res of
+      Right (Just (_, _, w : _)) -> Just w
+      _ -> Nothing
+
+analysisWorks :: IO ()
+analysisWorks = do
+  let contract n d =
+        If
+          (DivValue (Constant n) (Constant d) `ValueGE` Constant 5)
+          Close
+          (Pay alicePk (Party alicePk) Language.Marlowe.Util.ada (Constant (-100)) Close)
+  result <- warningsTrace (contract 10 11)
+  assertBool "Analyse a contract" $ isRight result
+
+emptyTrace :: IO ()
+emptyTrace = do
+  let contract = Close
+  result <- warningsTrace contract
+  assertBool "Close passes static analysis" $ isRight result && isNothing (fromRight Nothing result)
+
+nonPositivePay :: IO ()
+nonPositivePay = do
+  let contract n = Pay alicePk (Party alicePk) Language.Marlowe.Util.ada (Constant n) Close
+  result <- getWarning $ contract (-100)
+  assertBool "Detect negative pay" $ maybe False isTransactionNonPositivePay result
+  result2 <- getWarning $ contract 0
+  assertBool "Detect zero pay" $ maybe False isTransactionNonPositivePay result2
+
+partialPay :: IO ()
+partialPay = do
+  let contract = Pay alicePk (Party alicePk) Language.Marlowe.Util.ada (Constant 100) Close
+  result <- getWarning contract
+  assertBool "Detect partial pay" $ maybe False isTransactionPartialPay result
+
+nonPositiveDeposit :: IO ()
+nonPositiveDeposit = do
+  let contract v =
+        When
+          [ Case
+              ( Deposit
+                  alicePk
+                  alicePk
+                  (Token "" "")
+                  (Constant v)
+              )
+              Close
+          ]
+          1699974289397
+          Close
+  result <- getWarning (contract (-100))
+  assertBool "Negative deposit" $ maybe False isTransactionNonPositiveDeposit result
+  result2 <- getWarning (contract 0)
+  assertBool "Zero deposit" $ maybe False isTransactionNonPositiveDeposit result2
+
+transactionShadowing :: IO ()
+transactionShadowing = do
+  let contract = Let "x" (Constant 1) (Let "x" (Constant 2) Close)
+  result <- getWarning contract
+  assertBool "Shadowing x" $ maybe False isTransactionShadowing result
+
+assertionFailed :: IO ()
+assertionFailed = do
+  let contract = Let "x" (Constant 1) (Assert (ValueEQ (UseValue "x") (Constant 2)) Close)
+  result <- getWarning contract
+  assertBool "Detect wrong assertion" $ maybe False isTransactionAssertionFailed result
+
+-- The current UI drops in instrumentation in the form of assertions and then checks for AssertionFailed
+reachability :: IO ()
+reachability = do
+  let contract =
+        Let
+          "x"
+          (Constant 1)
+          ( If
+              ( ValueGE
+                  (UseValue "x")
+                  (Constant 2)
+              )
+              ( Assert
+                  ( ValueGE
+                      (UseValue "x")
+                      (Constant 2)
+                  )
+                  Close
+              )
+              ( Assert
+                  ( ValueLT
+                      (UseValue "x")
+                      (Constant 2)
+                  )
+                  (Assert FalseObs Close)
+              )
+          )
+  result <- getWarning contract
+  assertBool "Detect reachable path" $ maybe False isTransactionAssertionFailed result
+  let contract2 =
+        Let
+          "x"
+          (Constant 1)
+          ( If
+              ( ValueGE
+                  (UseValue "x")
+                  (Constant 2)
+              )
+              ( Assert
+                  ( ValueGE
+                      (UseValue "x")
+                      (Constant 2)
+                  )
+                  (Assert FalseObs Close)
+              )
+              ( Assert
+                  ( ValueLT
+                      (UseValue "x")
+                      (Constant 2)
+                  )
+                  Close
+              )
+          )
+  result2 <- getWarning contract2
+  assertEqual "Don't trigger a warning on the unreachable path" result2 Nothing
+
+-- The current UI drops in instrumentation in the form of assertions and then checks for AssertionFailed
+fundsOnClose :: IO ()
+fundsOnClose = do
+  let contract =
+        When
+          [ Case
+              (Deposit alicePk alicePk Language.Marlowe.Util.ada (Constant 100))
+              (Assert (ValueEQ (AvailableMoney alicePk Language.Marlowe.Util.ada) (Constant 0)) Close)
+          ]
+          1699974289397
+          Close
+  result <- getWarning contract
+  assertBool "Detect funds on close" $ maybe False isTransactionAssertionFailed result
+
+tests :: TestTree
+tests =
+  testGroup
+    "Static Analysis Regression"
+    [ testCase "Analysis works" analysisWorks
+    , testCase "Empty trace" emptyTrace
+    , testCase "Partial Pay" partialPay
+    , testCase "Non-Positive Pay" nonPositivePay
+    , testCase "Non-Positive Deposit" nonPositiveDeposit
+    , testCase "Transaction shadowing" transactionShadowing
+    , testCase "Assertion failed" assertionFailed
+    , testCase "Reachability checks" reachability
+    , testCase "Funds on Close" fundsOnClose
+    ]