271 recursive simplification of constraints during evaluation

README.md

@@ -79,7 +79,7 @@ To get HLS working in VSCode, install these two extensions:
 https://marketplace.visualstudio.com/items?itemName=arrterian.nix-env-selector
 https://marketplace.visualstudio.com/items?itemName=haskell.haskell
 
-The `nix-env-selector` extension may prompt for the workspace to be re-loaded. Once re-loaded, HLS should start working. 
+The `nix-env-selector` extension may prompt for the workspace to be re-loaded. Once re-loaded, HLS should start working.
 
 ## Eventlog tracing
 
@@ -112,4 +112,4 @@ There is a simple utility called pretty which can be used to pretty print a KORE
 
 ```
 cabal run pretty -- ../definition.kore <(jq '.result.state' XXX_response.json)
-```
+```

library/Booster/JsonRpc.hs

@@ -767,6 +767,19 @@ mkLogRewriteTrace
                                     , origin = Booster
                                     , result = Failure{reason = "Loop detected", _ruleId = Nothing}
                                     }
+                            ApplyEquations.TooManyRecursions stk ->
+                                Simplification
+                                    { originalTerm = Nothing
+                                    , originalTermIndex = Nothing
+                                    , origin = Booster
+                                    , result =
+                                        Failure
+                                            { reason =
+                                                "Reached recursion limit of "
+                                                    <> pack (show $ length stk)
+                                            , _ruleId = Nothing
+                                            }
+                                    }
                             ApplyEquations.InternalError err ->
                                 Simplification
                                     { originalTerm = Nothing

library/Booster/Pattern/ApplyEquations.hs

@@ -70,14 +70,45 @@ newtype EquationT io a
 throw :: MonadLoggerIO io => EquationFailure -> EquationT io a
 throw = EquationT . lift . throwE
 
+catch_ ::
+    MonadLoggerIO io => EquationT io a -> (EquationFailure -> EquationT io a) -> EquationT io a
+catch_ (EquationT op) hdlr = EquationT $ do
+    cfg <- ask
+    lift (runReaderT op cfg `catchE` (\e -> let EquationT fallBack = hdlr e in runReaderT fallBack cfg))
+
 data EquationFailure
     = IndexIsNone Term
     | TooManyIterations Int Term Term
     | EquationLoop [Term]
+    | TooManyRecursions [Term]
     | SideConditionFalse Predicate
     | InternalError Text
     deriving stock (Eq, Show)
 
+instance Pretty EquationFailure where
+    pretty = \case
+        IndexIsNone t ->
+            "Index 'None' for term " <> pretty t
+        TooManyIterations count start end ->
+            vsep
+                [ "Unable to finish evaluation in " <> pretty count <> " iterations"
+                , "Started with: " <> pretty start
+                , "Stopped at: " <> pretty end
+                ]
+        EquationLoop ts ->
+            vsep $ "Evaluation produced a loop:" : map pretty ts
+        TooManyRecursions ts ->
+            vsep $
+                "Recursion limit exceeded. The following terms were evaluated:"
+                    : map pretty ts
+        SideConditionFalse p ->
+            vsep
+                [ "A side condition was found to be false during evaluation (pruning)"
+                , pretty p
+                ]
+        InternalError msg ->
+            "Internal error during evaluation: " <> pretty msg
+
 data EquationConfig = EquationConfig
     { definition :: KoreDefinition
     , llvmApi :: Maybe LLVM.API
@@ -87,6 +118,7 @@ data EquationConfig = EquationConfig
 
 data EquationState = EquationState
     { termStack :: [Term]
+    , recursionStack :: [Term]
     , changed :: Bool
     , predicates :: Set Predicate
     , trace :: Seq EquationTrace
@@ -171,10 +203,20 @@ isSuccess _ = False
 
 startState :: Map Term Term -> EquationState
 startState cache =
-    EquationState{termStack = [], changed = False, predicates = mempty, trace = mempty, cache}
+    EquationState
+        { termStack = []
+        , recursionStack = []
+        , changed = False
+        , predicates = mempty
+        , trace = mempty
+        , cache
+        }
+
+eqState :: MonadLoggerIO io => StateT EquationState io a -> EquationT io a
+eqState = EquationT . lift . lift
 
 getState :: MonadLoggerIO io => EquationT io EquationState
-getState = EquationT (lift $ lift get)
+getState = eqState get
 
 getConfig :: MonadLoggerIO io => EquationT io EquationConfig
 getConfig = EquationT ask
@@ -183,23 +225,36 @@ countSteps :: MonadLoggerIO io => EquationT io Int
 countSteps = length . (.termStack) <$> getState
 
 pushTerm :: MonadLoggerIO io => Term -> EquationT io ()
-pushTerm t = EquationT . lift . lift . modify $ \s -> s{termStack = t : s.termStack}
+pushTerm t = eqState . modify $ \s -> s{termStack = t : s.termStack}
 
 pushConstraints :: MonadLoggerIO io => Set Predicate -> EquationT io ()
-pushConstraints ps = EquationT . lift . lift . modify $ \s -> s{predicates = s.predicates <> ps}
+pushConstraints ps = eqState . modify $ \s -> s{predicates = s.predicates <> ps}
 
 setChanged, resetChanged :: MonadLoggerIO io => EquationT io ()
-setChanged = EquationT . lift . lift . modify $ \s -> s{changed = True}
-resetChanged = EquationT . lift . lift . modify $ \s -> s{changed = False}
+setChanged = eqState . modify $ \s -> s{changed = True}
+resetChanged = eqState . modify $ \s -> s{changed = False}
 
 getChanged :: MonadLoggerIO io => EquationT io Bool
-getChanged = EquationT . lift . lift $ gets (.changed)
+getChanged = eqState $ gets (.changed)
+
+pushRecursion :: MonadLoggerIO io => Term -> EquationT io Int
+pushRecursion t = eqState $ do
+    stk <- gets (.recursionStack)
+    modify $ \s -> s{recursionStack = t : stk}
+    pure (1 + length stk)
+
+popRecursion :: MonadLoggerIO io => EquationT io ()
+popRecursion = do
+    s <- getState
+    if null s.recursionStack
+        then throw $ InternalError "Trying to pop an empty recursion stack"
+        else eqState $ put s{recursionStack = tail s.recursionStack}
 
 toCache :: MonadLoggerIO io => Term -> Term -> EquationT io ()
-toCache orig result = EquationT . lift . lift . modify $ \s -> s{cache = Map.insert orig result s.cache}
+toCache orig result = eqState . modify $ \s -> s{cache = Map.insert orig result s.cache}
 
 fromCache :: MonadLoggerIO io => Term -> EquationT io (Maybe Term)
-fromCache t = EquationT . lift . lift $ Map.lookup t <$> gets (.cache)
+fromCache t = eqState $ Map.lookup t <$> gets (.cache)
 
 checkForLoop :: MonadLoggerIO io => Term -> EquationT io ()
 checkForLoop t = do
@@ -232,16 +287,22 @@ runEquationT doTracing definition llvmApi smtSolver sCache (EquationT m) = do
 iterateEquations ::
     MonadLoggerIO io =>
     Int ->
+    Int ->
     Direction ->
     EquationPreference ->
     Term ->
     EquationT io Term
-iterateEquations maxIterations direction preference startTerm = do
+iterateEquations maxRecursion maxIterations direction preference startTerm = do
     logOther (LevelOther "Simplify") $ "Evaluating " <> renderText (pretty startTerm)
-    result <- go startTerm
+    result <- pushRecursion startTerm >>= checkCounter >> go startTerm <* popRecursion
     logOther (LevelOther "Simplify") $ "Result: " <> renderText (pretty result)
     pure result
   where
+    checkCounter counter
+        | counter > maxRecursion =
+            throw . TooManyRecursions . (.recursionStack) =<< getState
+        | otherwise = pure ()
+
     go :: MonadLoggerIO io => Term -> EquationT io Term
     go currentTerm
         | (getAttributes currentTerm).isEvaluated = pure currentTerm
@@ -281,7 +342,7 @@ evaluateTerm' ::
     Direction ->
     Term ->
     EquationT io Term
-evaluateTerm' direction = iterateEquations 100 direction PreferFunctions
+evaluateTerm' direction = iterateEquations 5 100 direction PreferFunctions
 
 {- | Simplify a Pattern, processing its constraints independently.
      Returns either the first failure or the new pattern if no failure was encountered
@@ -317,7 +378,7 @@ evaluatePattern' Pattern{term, constraints, ceilConditions} = do
     simplifyAssumedPredicate p = do
         allPs <- predicates <$> getState
         let otherPs = Set.delete p allPs
-        EquationT $ lift $ lift $ modify $ \s -> s{predicates = otherPs}
+        eqState $ modify $ \s -> s{predicates = otherPs}
         newP <- simplifyConstraint' True $ coerce p
         pushConstraints $ Set.singleton $ coerce newP
 
@@ -578,7 +639,7 @@ traceRuleApplication t loc lbl uid res = do
         _ -> pure ()
     config <- getConfig
     when config.doTracing $
-        EquationT . lift . lift . modify $
+        eqState . modify $
             \s -> s{trace = s.trace :|> newTraceItem}
 
 applyEquation ::
@@ -632,17 +693,29 @@ applyEquation term rule = fmap (either id Success) $ runExceptT $ do
                     pure $ substituteInTerm subst rule.rhs
                 unclearConditions -> throwE $ IndeterminateCondition unclearConditions
   where
-    -- evaluate/simplify a predicate, cut the operation short when it
-    -- is Bottom.
+    -- Simplify given predicate in a nested EquationT execution.
+    -- Call 'whenBottom' if it is Bottom, return Nothing if it is Top,
+    -- otherwise return the simplified remaining predicate.
     checkConstraint ::
         (Predicate -> ApplyEquationResult) ->
         Predicate ->
         ExceptT ApplyEquationResult (EquationT io) (Maybe Predicate)
-    checkConstraint whenBottom (Predicate p) =
-        lift (simplifyConstraint' False p) >>= \case
-            FalseBool -> throwE $ whenBottom $ coerce p
+    checkConstraint whenBottom (Predicate p) = do
+        logOther (LevelOther "Simplify") $
+            "Recursive simplification of predicate: " <> pack (renderDefault (pretty p))
+        let fallBackToUnsimplified :: EquationFailure -> EquationT io Term
+            fallBackToUnsimplified e = do
+                logOther (LevelOther "Simplify") . pack . renderDefault $
+                    "Aborting recursive simplification:" <> pretty e
+                pure p
+        -- exceptions need to be handled differently in the recursion,
+        -- falling back to the unsimplified constraint instead of aborting.
+        simplified <-
+            lift $ simplifyConstraint' True p `catch_` fallBackToUnsimplified
+        case simplified of
+            FalseBool -> throwE . whenBottom $ coerce p
             TrueBool -> pure Nothing
-            _other -> pure $ Just $ coerce p
+            other -> pure . Just $ coerce other
 
     allMustBeConcrete (AllConstrained Concrete) = True
     allMustBeConcrete _ = False
@@ -748,6 +821,7 @@ simplifyConstraint' recurseIntoEvalBool = \case
     evalBool :: MonadLoggerIO io => Term -> EquationT io Term
     evalBool t = do
         prior <- getState -- save prior state so we can revert
-        result <- iterateEquations 100 BottomUp PreferFunctions t
-        EquationT $ lift $ lift $ put prior
+        eqState $ put prior{termStack = [], changed = False}
+        result <- iterateEquations 5 100 BottomUp PreferFunctions t
+        eqState $ put prior
         pure result

scripts/integration-tests.sh

@@ -45,9 +45,12 @@ for dir in $(ls -d test-*); do
         "compute-ceil" | "no-evaluator")
             SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
             ;;
+        "simplify")
+            SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
+            ;;
         "foundry-bug-report")
             SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time $@
-            SERVER=$KORE_RPC_BOOSTER SERVER_OPTS="--interim-simplification 100" ./runDirectoryTest.sh test-$name --time $@
+            SERVER=$KORE_RPC_BOOSTER SERVER_OPTS="--interim-simplification 100" ./runDirectoryTest.sh test-$name $@
             ;;
         "imp")
             SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time $@

test/rpc-integration/resources/simplify.k

@@ -1,9 +1,29 @@
 module SIMPLIFY
   imports INT
+  imports BOOL
   imports ID-SYNTAX
   imports K-EQUAL
 
   syntax Int ::= f ( Int ) [function, no-evaluators] // a non-concrete value
+               | g ( Int ) [function, klabel("g"), symbol] // for simplification purposes
+
+  syntax Bool ::= p1 ( Int ) [function, total, no-evaluators, klabel("p1"), symbol]
+                | p2 ( Int ) [function, total, no-evaluators, klabel("p2"), symbol]
+                | p3 ( Int ) [function, total, klabel("p3"), symbol]
+
+  // an indirect simplifiation loop
+  rule [p1-if-p2]: p1(X) => true requires p2(X) [simplification]
+  rule [p2-if-p1]: p2(X) => true requires p1(X) [simplification]
+  // simplification of terms involving p1(_someInt) or p2(_someInt) will enter
+  // a loop of p1, p2, p1, p2... until the maximum recursion depth is reached
+  // and then bail out in booster. Simplification in kore-rpc _loops to infinity_.
+
+  // a set of function equations that require recursive evaluation of side condition p3
+  rule [eval-g]: g(X) => X requires p3(X)
+
+  rule [p3-true]: p3(1) => true
+  rule [p3-false]: p3(_) => false [owise]
+
 
 /* Simplification rules from domains.md, reproduced here for documentation
 

test/rpc-integration/test-internalise-symbols/state-incorrect-argument-sort.execute

@@ -1,7 +1,7 @@
 {
       "format": "KORE",
       "version": 1,
-      "term": 
+      "term":
         {
           "tag": "App",
           "name": "Lbl'-LT-'int'-GT-'",
@@ -18,4 +18,4 @@
             }
           ]
         }
-    }
+    }

test/rpc-integration/test-simplify/README.md

@@ -0,0 +1,50 @@
+# Tests for simplification in `booster` (executed with `booster-dev` only)
+
+This integration test runs a few simplification requests with `Int`
+expressions. It is expected that known rules from `domains.md` apply,
+which will, e.g., move symbolic terms in additions and subtractions to
+the left.
+
+Since `booster-dev` is used without an llvm backend library, no
+integer evaluation is expected in the results.
+
+Some additional functions and predicates were defined to test the
+behaviour for recursive evaluation (when an evaluation or
+simplification has a requirement which must be simplified/evaluated
+before it is found to be true). See `simplify.k` for details.
+
+* Integer evaluation and simplification
+
+  | Name                      | Input             | Expected output   | rules in `domains.md` which |
+  |-------------------------- | ----------------- | ----------------- |---------------------------- |
+  | _no-simplification_       | `123`             | `123`             | n/a                         |
+  | _plus-null-removed_       | `0 + f(34)`       | `f(34)`           | remove the zero addition    |
+  | _symbolic-first_          | `12 + f(34)`      | `f(34) + 12`      | move symbolic values left   |
+  | _symbolic-first-of-3_     | `12 + f(34) + 56` | `f(34) + 12 + 56` | move symbolic values left   |
+  | _evaluate-under-function_ | `f(12 + 0)`       | `f(12)`           | remove the zero addition    |
+
+  - _with-logging_ is the same as _symbolic-first-of-3_ but with simplification logging enabled.
+
+
+* Recursive evaluation of equation constraints
+
+  | Name                      | Input    | Expected output | because                               |
+  |-------------------------- | -------- | --------------- |-------------------------------------- |
+  | _evaluate-two-stage-fail_ | `g(2)`   | `g(2)`          | no evaluation rule applies            |
+  | _evaluate-two-stage_      | `g(1)`   | `1`             | applying rule `eval-g`                |
+  |                           |          |                 | after evaluating `p3(1)` to `true`    |
+  | _simplification-loop_     | `p1(42)` | `p1(42)`        | simplification attempt detects a loop |
+  |                           |          |                 | and returns the original              |
+
+  - **The _simplification_loop_ test loops forever in `kore-rpc-booster` and `kore-rpc-dev`.**
+
+* Tests for the `#if-#then-#else` hook
+
+  | Name                         | Input (paraphrased)                    | Expected output |
+  |----------------------------- | -------------------------------------- | --------------- |
+  | _if-then-else-true_          | `#if true #then 1 #else 0 #fi`         |  `1`            |
+  | _if-then-else-false_         | `#if false #then 1 #else 0 #fi`        |  `0`            |
+  | _if-then-else-eval_          | `#if (false => X) #then 1 #else 0 #fi` |  `1`            |
+  | _if-then-else-indeterminate_ | `#if true #then 1 #else 0 #fi`         |  `1`            |
+  | _if-then-else-sort-error_    | `#if 42 #then 1 #else 0 #fi`           | _Error (sort)_  |
+  | _if-then-else-arity-error_   | `#if_#then_#else(true, 0)`             | _Error (arity)_ |

test/rpc-integration/test-simplify/response-evaluate-two-stage-fail.json

@@ -0,0 +1,26 @@
+{
+    "jsonrpc": "2.0",
+    "id": 1,
+    "result": {
+        "state": {
+            "format": "KORE",
+            "version": 1,
+            "term": {
+                "tag": "App",
+                "name": "Lblg",
+                "sorts": [],
+                "args": [
+                    {
+                        "tag": "DV",
+                        "sort": {
+                            "tag": "SortApp",
+                            "name": "SortInt",
+                            "args": []
+                        },
+                        "value": "2"
+                    }
+                ]
+            }
+        }
+    }
+}