SCP-952 - Find a good way of showing the result of reachability analy…

…sis (#2487)

* Rearrange dependencies to avoid cycles
* Add results from reachability analysis to linter
* Refresh editor on reachability analysis change so that markers are recalculated
* Fix initial step in reachability analysis

marlowe-playground-client/src/MainFrame/State.purs

@@ -73,7 +73,7 @@ import Simulation.Types as ST
 import StaticData (bufferLocalStorageKey, gistIdLocalStorageKey, jsBufferLocalStorageKey, marloweBufferLocalStorageKey)
 import StaticData as StaticData
 import Types (WebData)
-import Wallet as Wallet
+import WalletSimulation.Types as Wallet
 import Web.HTML (window) as Web
 import Web.HTML.HTMLDocument (toEventTarget)
 import Web.HTML.Window (document) as Web

marlowe-playground-client/src/MainFrame/Types.purs

@@ -33,7 +33,7 @@ import Router (Route)
 import SaveAs.Types as SaveAs
 import Simulation.Types as Simulation
 import Types (WebData)
-import Wallet as Wallet
+import WalletSimulation.Types as Wallet
 import Web.UIEvent.KeyboardEvent (KeyboardEvent)
 
 data ModalView

marlowe-playground-client/src/Marlowe/Linter.purs

@@ -23,6 +23,7 @@ import Data.Bifunctor (bimap)
 import Data.BigInteger (BigInteger)
 import Data.Either (Either(..), hush)
 import Data.Foldable (foldM)
+import Data.FoldableWithIndex (traverseWithIndex_)
 import Data.Function (on)
 import Data.Functor (mapFlipped)
 import Data.Generic.Rep (class Generic)
@@ -34,7 +35,7 @@ import Data.Lens.Record (prop)
 import Data.List (List(..))
 import Data.Map (Map)
 import Data.Map as Map
-import Data.Maybe (Maybe(..), fromMaybe, maybe)
+import Data.Maybe (Maybe(..), fromMaybe, isNothing, maybe)
 import Data.Newtype (class Newtype)
 import Data.Ord (abs)
 import Data.Set (Set)
@@ -43,7 +44,6 @@ import Data.String (codePointFromChar, fromCodePointArray, length, takeWhile, to
 import Data.String.Regex (match, regex)
 import Data.String.Regex.Flags (noFlags)
 import Data.Symbol (SProxy(..))
-import Data.Traversable (traverse_)
 import Data.Tuple (Tuple(..))
 import Data.Tuple.Nested (type (/\), (/\))
 import Help (holeText)
@@ -53,7 +53,8 @@ import Marlowe.Semantics (Rational(..), Slot(..), _accounts, _boundValues, _choi
 import Marlowe.Semantics as Semantics
 import Monaco (CodeAction, CompletionItem, IMarkerData, IRange, TextEdit, Uri, markerSeverity)
 import Monaco as Monaco
-import Simulation.Types (ContractPath)
+import Reachability (initialisePrefixMap, stepPrefixMap)
+import Simulation.Types (ContractPath, ContractPathStep(..), PrefixMap)
 import Text.Pretty (hasArgs, pretty)
 
 newtype MaxTimeout
@@ -223,6 +224,7 @@ newtype LintEnv
   , letBindings :: Set Semantics.ValueId
   , maxTimeout :: MaxTimeout
   , isReachable :: Boolean
+  , unreachablePaths :: Maybe PrefixMap
   }
 
 derive instance newtypeLintEnv :: Newtype LintEnv _
@@ -242,16 +244,40 @@ _deposits = _Newtype <<< prop (SProxy :: SProxy "deposits")
 _isReachable :: Lens' LintEnv Boolean
 _isReachable = _Newtype <<< prop (SProxy :: SProxy "isReachable")
 
-emptyEnvironment :: LintEnv
-emptyEnvironment =
+emptyEnvironment :: List ContractPath -> LintEnv
+emptyEnvironment unreachablePathList =
   LintEnv
     { choicesMade: mempty
     , deposits: mempty
     , letBindings: mempty
     , maxTimeout: mempty
     , isReachable: true
+    , unreachablePaths: Just $ initialisePrefixMap unreachablePathList
     }
 
+-- Generic wrapper for stepPrefixMap. It steps the results of reachability analysis to see
+-- if the current node is unreachable, if it is unreachable it calls `markUnreachable`
+stepPrefixMapEnvGeneric :: LintEnv -> CMS.State State Unit -> ContractPathStep -> CMS.State State LintEnv
+stepPrefixMapEnvGeneric (LintEnv env@{ unreachablePaths: Nothing }) markUnreachable cp = do
+  pure $ LintEnv env { unreachablePaths = Nothing, isReachable = false }
+
+stepPrefixMapEnvGeneric (LintEnv env@{ unreachablePaths: Just upOld, isReachable: oldReachable }) markUnreachable cp = do
+  mUpNew <- stepPrefixMap markUnreachable upOld cp
+  pure $ LintEnv env { unreachablePaths = mUpNew, isReachable = oldReachable && (not $ isNothing mUpNew) }
+
+-- Wrapper for stepPrefixMap that marks unreachable code with a warning
+stepPrefixMapEnv :: forall a. Show a => LintEnv -> a -> Range -> ContractPathStep -> CMS.State State LintEnv
+stepPrefixMapEnv env t pos cp = stepPrefixMapEnvGeneric env markUnreachable cp
+  where
+  markUnreachable = addWarning UnreachableContract t pos
+
+-- Simpler version of the wrapper for places for where we know we won't get a root of unreachable code
+-- See isValidSubproblem in Reachability.purs for a list of roots of possible unreachable nodes
+stepPrefixMapEnv_ :: LintEnv -> ContractPathStep -> CMS.State State LintEnv
+stepPrefixMapEnv_ env cp = stepPrefixMapEnvGeneric env dontMarkUnreachable cp
+  where
+  dontMarkUnreachable = pure unit
+
 data TemporarySimplification a b
   = ConstantSimp
     Range
@@ -341,7 +367,7 @@ lint unreachablePaths contractState contract = state
 
   deposits = contractState ^. (_accounts <<< to (Map.mapMaybe (Just <<< Just)))
 
-  env = (set _letBindings bindings <<< set _deposits deposits <<< set _choicesMade choices) emptyEnvironment
+  env = (set _letBindings bindings <<< set _deposits deposits <<< set _choicesMade choices) (emptyEnvironment unreachablePaths)
 
   state = CMS.execState (lintContract env contract) mempty
 
@@ -361,7 +387,7 @@ lintContract env t@(Term (Pay acc payee token payment cont) pos) = do
       | otherwise -> pure (Just c)
     _ -> pure Nothing
   markSimplification constToVal SimplifiableValue payment sa
-  newEnv <- case (fromTerm acc /\ fromTerm token) of
+  tmpEnv <- case (fromTerm acc /\ fromTerm token) of
     Just accTerm /\ Just tokenTerm -> do
       let
         deposits = view _deposits env
@@ -384,49 +410,58 @@ lintContract env t@(Term (Pay acc payee token payment cont) pos) = do
         Nothing /\ _ -> pure env
         _ -> pure (over _deposits (Map.insert key Nothing) env)
     _ -> pure env
+  newEnv <- stepPrefixMapEnv_ tmpEnv PayContPath
   lintContract newEnv cont
 
 lintContract env (Term (If obs c1 c2) _) = do
   sa <- lintObservation env obs
+  c1Env <- stepPrefixMapEnv env c1 (getRange c1) IfTruePath
+  c2Env <- stepPrefixMapEnv env c2 (getRange c2) IfFalsePath
   let
-    currReachable = view _isReachable env
+    reachable = view _isReachable
 
-    newEnv reach = if reach then env else set _isReachable false env
-  c1Env /\ c2Env <-
-    bimap newEnv newEnv
+    c1Reachable = reachable c1Env
+
+    c2Reachable = reachable c2Env
+
+    updateEnv lEnv reach = if reach then lEnv else set _isReachable false lEnv
+  c1NewEnv /\ c2NewEnv <-
+    bimap (updateEnv c1Env) (updateEnv c2Env)
       <$> ( case sa of
             (ConstantSimp _ _ c) ->
               if c then do
-                when currReachable $ addWarning UnreachableContract c2 (getRange c2)
-                pure (currReachable /\ false)
+                when c2Reachable $ addWarning UnreachableContract c2 (getRange c2)
+                pure (c1Reachable /\ false)
               else do
-                when currReachable $ addWarning UnreachableContract c1 (getRange c1)
-                pure (false /\ currReachable)
+                when c1Reachable $ addWarning UnreachableContract c1 (getRange c1)
+                pure (false /\ c2Reachable)
             _ -> do
               markSimplification constToObs SimplifiableObservation obs sa
-              pure (currReachable /\ currReachable)
+              pure (c1Reachable /\ c2Reachable)
         )
-  lintContract c1Env c1
-  lintContract c2Env c2
+  lintContract c1NewEnv c1
+  lintContract c2NewEnv c2
 
 lintContract env (Term (When cases timeout@(TermWrapper slot pos) cont) _) = do
-  let
-    newEnv = (over _maxTimeout (max timeout)) env
-  traverse_ (lintCase newEnv) cases
   when (timeout <= view _maxTimeout env) (addWarning TimeoutNotIncreasing slot pos)
+  let
+    tmpEnv = (over _maxTimeout (max timeout)) env
+  traverseWithIndex_ (lintCase tmpEnv) cases
+  newEnv <- stepPrefixMapEnv_ tmpEnv WhenTimeoutPath
   lintContract newEnv cont
   pure unit
 
 lintContract env (Term (Let (TermWrapper valueId pos) value cont) _) = do
-  newEnv <- case fromTerm valueId of
+  tmpEnv <- case fromTerm valueId of
     Just valueIdSem -> do
       let
-        newEnv = over _letBindings (Set.insert valueIdSem) env
+        tmpEnv = over _letBindings (Set.insert valueIdSem) env
       when (Set.member valueIdSem (view _letBindings env)) $ addWarning ShadowedLet valueId pos
-      pure newEnv
+      pure tmpEnv
     Nothing -> pure env
   sa <- lintValue env value
   markSimplification constToVal SimplifiableValue value sa
+  newEnv <- stepPrefixMapEnv_ tmpEnv LetPath
   lintContract newEnv cont
 
 lintContract env hole@(Hole _ _ _) = do
@@ -435,7 +470,8 @@ lintContract env hole@(Hole _ _ _) = do
 
 lintContract env (Term (Assert obs cont) _) = do
   sa <- lintObservation env obs
-  lintContract env cont
+  newEnv <- stepPrefixMapEnv_ env AssertPath
+  lintContract newEnv cont
   markSimplification constToObs SimplifiableObservation obs sa
   pure unit
 
@@ -669,8 +705,9 @@ data Effect
   | ChoiceMade Semantics.ChoiceId
   | NoEffect
 
-lintCase :: LintEnv -> Term Case -> CMS.State State Unit
-lintCase env t@(Term (Case action contract) pos) = do
+lintCase :: LintEnv -> Int -> Term Case -> CMS.State State Unit
+lintCase iniEnv n t@(Term (Case action contract) pos) = do
+  env <- stepPrefixMapEnv iniEnv t pos $ WhenCasePath n
   effect /\ isReachable <- lintAction env action
   let
     tempEnv = case effect of
@@ -683,7 +720,7 @@ lintCase env t@(Term (Case action contract) pos) = do
   lintContract newEnv contract
   pure unit
 
-lintCase env hole@(Hole _ _ _) = do
+lintCase env n hole@(Hole _ _ _) = do
   modifying _holes (insertHole hole)
   pure unit
 

marlowe-playground-client/src/Reachability.purs

@@ -1,17 +1,22 @@
-module Reachability (areContractAndStateTheOnesAnalysed, getUnreachableContracts, startReachabilityAnalysis, updateWithResponse) where
+module Reachability (areContractAndStateTheOnesAnalysed, getUnreachableContracts, initialisePrefixMap, startReachabilityAnalysis, stepPrefixMap, updateWithResponse) where
 
 import Control.Monad.Except (ExceptT, runExceptT)
 import Control.Monad.Reader (runReaderT)
-import Data.Function (flip)
+import Control.Monad.State as CMS
+import Data.Foldable (for_)
+import Data.Function (flip, identity)
 import Data.Lens (assign)
-import Data.List (List(..), foldl, fromFoldable, length, snoc, toUnfoldable)
-import Data.List.NonEmpty (NonEmptyList(..), toList)
+import Data.List (List(..), any, catMaybes, foldl, fromFoldable, length, null, snoc, toUnfoldable)
+import Data.List.NonEmpty (NonEmptyList(..), fromList, head, tail, toList)
+import Data.Map (fromFoldableWith, lookup, unionWith)
 import Data.Maybe (Maybe(..))
 import Data.NonEmpty ((:|))
+import Data.Set (singleton, union)
 import Data.Tuple.Nested (type (/\), (/\))
 import Effect.Aff.Class (class MonadAff)
-import Halogen (HalogenM)
-import MainFrame.Types (ChildSlots)
+import Halogen (HalogenM, query)
+import Halogen.Monaco as Monaco
+import MainFrame.Types (ChildSlots, _marloweEditorSlot)
 import Marlowe (SPParams_)
 import Marlowe as Server
 import Marlowe.Semantics (Case(..), Contract(..), Observation(..))
@@ -20,10 +25,10 @@ import Marlowe.Symbolic.Types.Request as MSReq
 import Marlowe.Symbolic.Types.Response (Result(..))
 import Network.RemoteData (RemoteData(..))
 import Network.RemoteData as RemoteData
-import Prelude (Void, bind, discard, map, pure, ($), (&&), (+), (-), (/=), (<$>), (<>), (==))
+import Prelude (Unit, Void, bind, discard, map, mempty, pure, unit, void, when, ($), (&&), (+), (-), (/=), (<$>), (<>), (==), (>))
 import Servant.PureScript.Ajax (AjaxError(..))
 import Servant.PureScript.Settings (SPSettings_)
-import Simulation.Types (Action, AnalysisState(..), ContractPath, ContractPathStep(..), ContractZipper(..), ReachabilityAnalysisData(..), RemainingSubProblemInfo, State, WebData, InProgressRecord, _analysisState)
+import Simulation.Types (Action, AnalysisState(..), ContractPath, ContractPathStep(..), ContractZipper(..), InProgressRecord, ReachabilityAnalysisData(..), RemainingSubProblemInfo, State, WebData, PrefixMap, _analysisState)
 
 splitArray :: forall a. List a -> List (List a /\ a /\ List a)
 splitArray x = splitArrayAux Nil x
@@ -153,7 +158,7 @@ startReachabilityAnalysis ::
 startReachabilityAnalysis settings contract state = do
   case getNextSubproblem isValidSubproblem initialSubproblems Nil of
     Nothing -> pure AllReachable
-    Just ((contractZipper /\ subcontract /\ newChildren) /\ newSubproblems) -> do
+    Just ((contractZipper /\ _ /\ newChildren) /\ newSubproblems) -> do
       let
         numSubproblems = countSubproblems isValidSubproblem (newChildren <> newSubproblems)
 
@@ -173,7 +178,7 @@ startReachabilityAnalysis settings contract state = do
               }
           )
       assign _analysisState (ReachabilityAnalysis progress)
-      response <- checkContractForReachability settings subcontract state
+      response <- checkContractForReachability settings newContract state
       result <- updateWithResponse settings progress response
       pure result
   where
@@ -265,13 +270,24 @@ stepAnalysis :: forall m. MonadAff m => SPSettings_ SPParams_ -> Boolean -> InPr
 stepAnalysis settings isReachable rad =
   let
     thereAreMore /\ newRad = stepSubproblem isReachable rad
+
+    thereAreNewCounterExamples = length newRad.unreachableSubcontracts > length rad.unreachableSubcontracts
   in
     if thereAreMore then do
       assign _analysisState (ReachabilityAnalysis (InProgress newRad))
+      when thereAreNewCounterExamples refreshEditor
       response <- checkContractForReachability settings (newRad.currContract) (newRad.originalState)
       updateWithResponse settings (InProgress newRad) response
-    else
-      pure $ finishAnalysis newRad
+    else do
+      let
+        result = finishAnalysis newRad
+      assign _analysisState (ReachabilityAnalysis result)
+      when thereAreNewCounterExamples refreshEditor
+      pure result
+  where
+  refreshEditor = do
+    mContent <- query _marloweEditorSlot unit (Monaco.GetText identity)
+    for_ mContent (\content -> void $ query _marloweEditorSlot unit $ Monaco.SetText content unit)
 
 updateWithResponse ::
   forall m.
@@ -302,3 +318,21 @@ areContractAndStateTheOnesAnalysed (ReachabilityAnalysis (InProgress ipr)) (Just
 areContractAndStateTheOnesAnalysed (ReachabilityAnalysis (UnreachableSubcontract us)) (Just contract) state = us.originalContract == contract && us.originalState == state
 
 areContractAndStateTheOnesAnalysed _ _ _ = false
+
+-- It groups the contract paths by their head, discards empty contract paths
+initialisePrefixMap :: List ContractPath -> PrefixMap
+initialisePrefixMap unreachablePathList = fromFoldableWith union $ map (\x -> (head x /\ singleton x)) $ catMaybes $ map fromList unreachablePathList
+
+-- Returns Nothing when the path is unreachable according to one of the paths, otherwise it returns the updated PrefixMap for the subpath
+stepPrefixMap :: forall a. CMS.State a Unit -> PrefixMap -> ContractPathStep -> CMS.State a (Maybe PrefixMap)
+stepPrefixMap markUnreachable prefixMap contractPath = case lookup contractPath prefixMap of
+  Just pathSet ->
+    let
+      tails = map tail $ fromFoldable pathSet
+    in
+      if any null tails then do
+        markUnreachable
+        pure Nothing
+      else
+        pure $ Just $ unionWith union (initialisePrefixMap tails) mempty
+  Nothing -> pure (Just mempty)

marlowe-playground-client/src/Simulation/State.purs

@@ -5,9 +5,7 @@ import Control.Monad.State (class MonadState)
 import Data.Array (fromFoldable, mapMaybe, sort, toUnfoldable, uncons)
 import Data.Either (Either(..))
 import Data.FoldableWithIndex (foldlWithIndex)
-import Data.Lens (Lens', has, modifying, nearly, over, previewOn, set, to, use, view, (^.))
-import Data.Lens.NonEmptyList (_Head)
-import Data.Lens.Record (prop)
+import Data.Lens (has, modifying, nearly, over, previewOn, set, to, use, view, (^.))
 import Data.List (List(..))
 import Data.List as List
 import Data.List.Types (NonEmptyList)
@@ -18,7 +16,6 @@ import Data.Newtype (unwrap, wrap)
 import Data.NonEmpty (foldl1, (:|))
 import Data.NonEmptyList.Extra (extendWith)
 import Data.NonEmptyList.Lens (_Tail)
-import Data.Symbol (SProxy(..))
 import Data.Tuple (Tuple(..))
 import Marlowe.Holes (fromTerm)
 import Marlowe.Linter (lint)
@@ -27,7 +24,7 @@ import Marlowe.Parser (parseContract)
 import Marlowe.Semantics (Action(..), Bound(..), ChoiceId(..), ChosenNum, Contract(..), Environment(..), Input, IntervalResult(..), Observation, Party, Slot, SlotInterval(..), State, TransactionInput(..), TransactionOutput(..), _minSlot, boundFrom, computeTransaction, emptyState, evalValue, extractRequiredActionsWithTxs, fixInterval, moneyInContract, timeouts)
 import Marlowe.Semantics as S
 import Prelude (class HeytingAlgebra, class Ord, Unit, add, append, map, max, mempty, min, one, otherwise, zero, (#), ($), (<<<), (<>), (==), (>), (>=))
-import Simulation.Types (ActionInput(..), ActionInputId(..), ExecutionState(..), ExecutionStateRecord, MarloweEvent(..), MarloweState, Parties, _SimulationRunning, _contract, _editorErrors, _executionState, _holes, _log, _moneyInContract, _moveToAction, _pendingInputs, _possibleActions, _slot, _state, _transactionError, _transactionWarnings, otherActionsParty)
+import Simulation.Types (ActionInput(..), ActionInputId(..), ExecutionState(..), ExecutionStateRecord, MarloweEvent(..), MarloweState, Parties, _SimulationRunning, _contract, _currentMarloweState, _editorErrors, _executionState, _holes, _log, _marloweState, _moneyInContract, _moveToAction, _pendingInputs, _possibleActions, _slot, _state, _transactionError, _transactionWarnings, otherActionsParty)
 
 minimumBound :: Array Bound -> ChosenNum
 minimumBound bnds = case uncons (map boundFrom bnds) of
@@ -222,15 +219,6 @@ stateToTxInput executionState =
   in
     TransactionInput { interval: interval, inputs: (List.fromFoldable inputs) }
 
---
--- Functions that can be used by records that contain MarloweState
---
-_marloweState :: forall s. Lens' { marloweState :: NonEmptyList MarloweState | s } (NonEmptyList MarloweState)
-_marloweState = prop (SProxy :: SProxy "marloweState")
-
-_currentMarloweState :: forall s. Lens' { marloweState :: NonEmptyList MarloweState | s } MarloweState
-_currentMarloweState = _marloweState <<< _Head
-
 updateMarloweState :: forall s m. MonadState { marloweState :: NonEmptyList MarloweState | s } m => (MarloweState -> MarloweState) -> m Unit
 updateMarloweState f = modifying _marloweState (extendWith (updatePossibleActions <<< f))