Skip to content

Commit

Permalink
kore-rpc - Return branch rule id and condition (#3716)
Browse files Browse the repository at this point in the history 
This PR adds new fields to the `next-states` objects, namely:

* new `rule-id` and `rule-predicate`and `rule-substitution` fields

The `rule-predicate` term is a subterm of `predicate` and signals the
requires clause predicate that was undecidable and thus caused
branching.
  • Loading branch information
@goodlyrottenapple
goodlyrottenapple authored Feb 7, 2024
1 parent 3779155 commit 7e2b8b3
Show file tree
Hide file tree
Showing 10 changed files with 3,529 additions and 115 deletions.
5 changes: 4 additions & 1 deletion kore-rpc-types/src/Kore/JsonRpc/Types.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,8 +107,11 @@ instance FromRequest (API 'Req) where

data ExecuteState = ExecuteState
{ term :: KoreJson
, substitution :: Maybe KoreJson
, predicate :: Maybe KoreJson
, substitution :: Maybe KoreJson
, ruleSubstitution :: Maybe KoreJson
, rulePredicate :: Maybe KoreJson
, ruleId :: Maybe Text
}
deriving stock (Generic, Show, Eq)
deriving
Expand Down
73 changes: 37 additions & 36 deletions kore/src/Kore/Exec.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -339,7 +339,7 @@ exec
infoExecDepth (maximum (ExecDepth 0 : depths))
let finalConfigs' =
MultiOr.make $
mapMaybe extractProgramState finalConfigs
mapMaybe (fst . extractProgramState) finalConfigs
debugFinalPatterns finalConfigs'
exitCode <- getExitCode verifiedModule finalConfigs'
let finalTerm =
Expand All @@ -364,12 +364,20 @@ exec
transit ::
GraphTraversal.TState
Prim
(ExecDepth, ProgramState (Pattern RewritingVariableName)) ->
( ExecDepth
, ProgramState
(RuleInfo RewritingVariableName)
(Pattern RewritingVariableName)
) ->
Simplifier
( GraphTraversal.TransitionResult
( GraphTraversal.TState
Prim
(ExecDepth, ProgramState (Pattern RewritingVariableName))
( ExecDepth
, ProgramState
(RuleInfo RewritingVariableName)
(Pattern RewritingVariableName)
)
)
)
transit =
Expand All @@ -380,21 +388,21 @@ exec
toTransitionResult

toTransitionResult ::
(ExecDepth, ProgramState p) ->
[(ExecDepth, ProgramState p)] ->
(ExecDepth, ProgramState d p) ->
[(ExecDepth, ProgramState d p)] ->
( GraphTraversal.TransitionResult
(ExecDepth, ProgramState p)
(ExecDepth, ProgramState d p)
)
toTransitionResult prior [] =
case snd prior of
Start _ -> GraphTraversal.Stop prior []
Rewritten _ -> GraphTraversal.Stop prior []
Rewritten _ _ -> GraphTraversal.Stop prior []
Remaining _ -> GraphTraversal.Stuck prior
Kore.Rewrite.Bottom -> GraphTraversal.Stuck prior
toTransitionResult _prior [next] =
case snd next of
Start _ -> GraphTraversal.Continuing next
Rewritten _ -> GraphTraversal.Continuing next
Rewritten _ _ -> GraphTraversal.Continuing next
Remaining _ -> GraphTraversal.Stuck next
Kore.Rewrite.Bottom -> GraphTraversal.Stuck next
toTransitionResult prior (s : ss) =
Expand All @@ -415,7 +423,7 @@ data RuleTrace = RuleTrace

-- | Type for json-rpc execution state, for readability
data RpcExecState v = RpcExecState
{ rpcProgState :: ProgramState (Pattern v)
{ rpcProgState :: ProgramState (RuleInfo v) (Pattern v)
-- ^ program state
, rpcRules :: Seq RuleTrace
-- ^ rule label/ids we have applied so far
Expand All @@ -432,12 +440,6 @@ startState t =
, rpcDepth = ExecDepth 0
}

stateGetRewritingPattern ::
RpcExecState RewritingVariableName ->
RpcExecState VariableName
stateGetRewritingPattern state@RpcExecState{rpcProgState} =
state{rpcProgState = fmap getRewritingPattern rpcProgState}

{- | Version of @kore-exec@ suitable for the JSON RPC server. Cannot
execute across branches, supports a depth limit and rule labels to
stop on (distinguished as cut-points for LHS or terminal-rules for
Expand All @@ -460,7 +462,7 @@ rpcExec ::
StopLabels ->
-- | The input pattern
TermLike VariableName ->
SMT (GraphTraversal.TraversalResult (RpcExecState VariableName))
SMT (GraphTraversal.TraversalResult (RpcExecState RewritingVariableName))
rpcExec
depthLimit
stepTimeout
Expand All @@ -478,19 +480,18 @@ rpcExec
StopLabels{cutPointLabels, terminalLabels}
(mkRewritingTerm -> initialTerm) =
simplifierRun $
fmap stateGetRewritingPattern
<$> GraphTraversal.graphTraversal
GraphTraversal.GraphTraversalCancel
stepTimeout
enableMA
Strategy.LeafOrBranching
Strategy.DepthFirst
(Limit 2) -- breadth limit 2 because we never go beyond a branch
transit
(const Nothing)
Limit.Unlimited
execStrategy
(startState initialTerm)
GraphTraversal.graphTraversal
GraphTraversal.GraphTraversalCancel
stepTimeout
enableMA
Strategy.LeafOrBranching
Strategy.DepthFirst
(Limit 2) -- breadth limit 2 because we never go beyond a branch
transit
(const Nothing)
Limit.Unlimited
execStrategy
(startState initialTerm)
where
simplifierRun
| tracingEnabled =
Expand Down Expand Up @@ -525,7 +526,7 @@ rpcExec
-- The rule label is carried around unmodified in the
-- transition, and adjusted in `toTransitionResult`
withRpcExecState ::
TransitionRule m r (ExecDepth, ProgramState (Pattern v)) ->
TransitionRule m r (ExecDepth, ProgramState (RuleInfo v) (Pattern v)) ->
TransitionRule m r (RpcExecState v)
withRpcExecState transition =
\prim RpcExecState{rpcProgState, rpcRules, rpcDepth} ->
Expand All @@ -543,7 +544,7 @@ rpcExec
Kore.Rewrite.Bottom -> GraphTraversal.Vacuous prior
-- returns `Final` to signal that no instructions were left.
Start _ -> GraphTraversal.Final prior
Rewritten _ -> GraphTraversal.Final prior
Rewritten _ _ -> GraphTraversal.Final prior
toTransitionResult prior@RpcExecState{rpcRules = priorRules} [(next, rules)]
| (_ : _) <- mapMaybe (isCutPoint . fst) (toList rules) =
GraphTraversal.Stop
Expand All @@ -557,7 +558,7 @@ rpcExec
let next' = setTraces rules priorRules next
in case nextPState of
Start _ -> GraphTraversal.Continuing next'
Rewritten _ -> GraphTraversal.Continuing next'
Rewritten _ _ -> GraphTraversal.Continuing next'
Remaining _ -> GraphTraversal.Stuck next'
Kore.Rewrite.Bottom -> GraphTraversal.Vacuous prior
toTransitionResult prior rs =
Expand Down Expand Up @@ -603,8 +604,8 @@ rpcExec

-- | Modify a 'TransitionRule' to track the depth of the execution graph.
trackExecDepth ::
TransitionRule monad rule (ProgramState p) ->
TransitionRule monad rule (ExecDepth, ProgramState p)
TransitionRule monad rule (ProgramState d p) ->
TransitionRule monad rule (ExecDepth, ProgramState d p)
trackExecDepth transit prim (execDepth, execState) = do
execState' <- transit prim execState
let execDepth' = (if didRewrite execState' then succ else id) execDepth
Expand All @@ -613,7 +614,7 @@ trackExecDepth transit prim (execDepth, execState) = do
-- The new state can become Bottom by simplification after rewriting,
-- or it remains Rewritten. If it is Remaining, it was not rewritten.
didRewrite Kore.Rewrite.Bottom = prim == Rewrite
didRewrite (Rewritten _) = prim == Rewrite
didRewrite (Rewritten _ _) = prim == Rewrite
didRewrite _ = False

-- | Add profiling markers to a 'TransitionRule'.
Expand Down Expand Up @@ -724,7 +725,7 @@ search
executionGraph <-
runStrategy' (Start initialPattern)
let match target config1 config2 = do
extracted <- hoistMaybe $ extractProgramState config2
extracted <- hoistMaybe $ fst $ extractProgramState config2
Search.matchWith target config1 extracted
solutionsLists <-
searchGraph
Expand Down
100 changes: 77 additions & 23 deletions kore/src/Kore/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,8 @@ import Kore.Internal.Predicate (
getMultiAndPredicate,
pattern PredicateTrue,
)
import Kore.Internal.Predicate qualified as Predicate
import Kore.Internal.Substitution (Assignment, assignedVariable)
import Kore.Internal.Substitution qualified as Substitution
import Kore.Internal.TermLike (TermLike)
import Kore.Internal.TermLike qualified as TermLike
Expand All @@ -73,13 +75,18 @@ import Kore.Parser (parseKoreModule)
import Kore.Reachability.Claim qualified as Claim
import Kore.Rewrite (
ProgramState,
RuleInfo (..),
extractProgramState,
)
import Kore.Rewrite.ClaimPattern qualified as ClaimPattern
import Kore.Rewrite.RewriteStep (EnableAssumeInitialDefined (..))
import Kore.Rewrite.RewritingVariable (
RewritingVariableName,
getRewritingPattern,
getRewritingTerm,
getRewritingVariable,
isSomeConfigVariable,
isSomeEquationVariable,
mkRewritingPattern,
mkRewritingTerm,
)
Expand All @@ -94,11 +101,14 @@ import Kore.Simplify.Pattern qualified as Pattern
import Kore.Simplify.Simplify (Simplifier, SimplifierTrace (..))
import Kore.Syntax (VariableName)
import Kore.Syntax.Definition (Definition (..))
import Kore.Syntax.Json qualified
import Kore.Syntax.Json qualified as PatternJson
import Kore.Syntax.Module (Module (..), ModuleName (..))
import Kore.Syntax.Sentence (
SentenceAxiom,
)
import Kore.Syntax.Variable qualified as SomeVariable
import Kore.TopBottom (TopBottom (isTop))
import Kore.Validate.DefinitionVerifier (verifyAndIndexDefinitionWithBase)
import Kore.Validate.PatternVerifier (Context (..))
import Kore.Validate.PatternVerifier qualified as PatternVerifier
Expand Down Expand Up @@ -223,7 +233,7 @@ respond serverState moduleName runSMT =
buildResult ::
Maybe Double ->
TermLike.Sort ->
GraphTraversal.TraversalResult (Exec.RpcExecState TermLike.VariableName) ->
GraphTraversal.TraversalResult (Exec.RpcExecState RewritingVariableName) ->
Either ErrorObj (API 'Res)
buildResult mbDuration sort = \case
GraphTraversal.Ended
Expand All @@ -233,7 +243,7 @@ respond serverState moduleName runSMT =
Right $
Execute $
ExecuteResult
{ state = patternToExecState sort result
{ state = patternToExecState False sort result
, depth = Depth depth
, reason = if Just (Depth depth) == maxDepth then DepthBound else Stuck
, rule = Nothing
Expand All @@ -249,7 +259,7 @@ respond serverState moduleName runSMT =
Right $
Execute $
ExecuteResult
{ state = patternToExecState sort result
{ state = patternToExecState False sort result
, depth = Depth depth
, reason = Stuck
, rule = Nothing
Expand All @@ -265,7 +275,7 @@ respond serverState moduleName runSMT =
Right $
Execute $
ExecuteResult
{ state = patternToExecState sort result
{ state = patternToExecState False sort result
, depth = Depth depth
, reason = Vacuous
, rule = Nothing
Expand All @@ -280,20 +290,20 @@ respond serverState moduleName runSMT =
Right $
Execute $
ExecuteResult
{ state = patternToExecState sort rpcProgState
{ state = patternToExecState False sort rpcProgState
, depth = Depth depth
, reason = CutPointRule
, rule
, nextStates =
Just $ map (patternToExecState sort . Exec.rpcProgState) nexts
Just $ map (patternToExecState False sort . Exec.rpcProgState) nexts
, logs = mkLogs mbDuration rules
, unknownPredicate = Nothing
}
| Just rule <- containsLabelOrRuleId rules terminalRules ->
Right $
Execute $
ExecuteResult
{ state = patternToExecState sort rpcProgState
{ state = patternToExecState False sort rpcProgState
, depth = Depth depth
, reason = TerminalRule
, rule
Expand All @@ -305,12 +315,12 @@ respond serverState moduleName runSMT =
Right $
Execute $
ExecuteResult
{ state = patternToExecState sort rpcProgState
{ state = patternToExecState False sort rpcProgState
, depth = Depth depth
, reason = Branching
, rule = Nothing
, nextStates =
Just $ map (patternToExecState sort . Exec.rpcProgState) nexts
Just $ map (patternToExecState True sort . Exec.rpcProgState) nexts
, logs = mkLogs mbDuration rules
, unknownPredicate = Nothing
}
Expand All @@ -320,7 +330,7 @@ respond serverState moduleName runSMT =
Right $
Execute $
ExecuteResult
{ state = patternToExecState sort rpcProgState
{ state = patternToExecState False sort rpcProgState
, depth = Depth depth
, reason = Timeout
, rule = Nothing
Expand All @@ -335,22 +345,66 @@ respond serverState moduleName runSMT =
Left $ backendError MultipleStates $ show other

patternToExecState ::
Bool ->
TermLike.Sort ->
ProgramState (Pattern TermLike.VariableName) ->
ProgramState (RuleInfo RewritingVariableName) (Pattern RewritingVariableName) ->
ExecuteState
patternToExecState sort s =
ExecuteState
{ term =
PatternJson.fromTermLike $ Pattern.term p
, substitution =
PatternJson.fromSubstitution sort $ Pattern.substitution p
, predicate =
case Pattern.predicate p of
PredicateTrue -> Nothing
pr -> Just $ PatternJson.fromPredicate sort pr
}
patternToExecState includeRuleInfo sort s
| includeRuleInfo =
ExecuteState
{ term
, predicate
, substitution
, ruleSubstitution
, rulePredicate
, ruleId
}
| otherwise =
ExecuteState
{ term
, predicate
, substitution
, ruleSubstitution = Nothing
, rulePredicate = Nothing
, ruleId = Nothing
}
where
p = fromMaybe (Pattern.bottomOf sort) $ extractProgramState s
term = PatternJson.fromTermLike $ Pattern.term p
predicate =
case Pattern.predicate p of
PredicateTrue -> Nothing
pr -> Just $ PatternJson.fromPredicate sort pr
substitution =
PatternJson.fromSubstitution sort $ Pattern.substitution p
(p, rulePredicate, ruleSubstitution, ruleId) = case extractProgramState s of
(Nothing, _) -> (Pattern.bottomOf sort, Nothing, Nothing, Nothing)
(Just p', Nothing) -> (getRewritingPattern p', Nothing, Nothing, Nothing)
(Just p', Just (RuleInfo{rulePredicate = pr, ruleSubstitution = sub, ruleId = UniqueId rid})) ->
let subUnwrapped = Substitution.unwrap sub
-- any substitutions which are not RuleVariable <var> -> <term> have been added to the substitution list
-- via an equation in the requires clause, e.g. X ==Int 0
-- hence, we want to copy these into the rule-condition
predsFromSub = filter ((isSomeConfigVariable ||| isSomeEquationVariable) . assignedVariable) subUnwrapped
pr' = Predicate.fromPredicate sort $ Predicate.mapVariables getRewritingVariable pr
finalPr =
if isTop pr
then
if null predsFromSub
then Nothing
else Just $ Kore.Syntax.Json.fromTermLike $ foldl1 TermLike.mkAnd $ map toEquals predsFromSub
else Just $ Kore.Syntax.Json.fromTermLike $ foldl TermLike.mkAnd pr' $ map toEquals predsFromSub
in ( getRewritingPattern p'
, finalPr
, PatternJson.fromSubstitution sort $ Substitution.mapVariables getRewritingVariable sub
, rid
)

toEquals :: Assignment RewritingVariableName -> TermLike VariableName
toEquals (Substitution.Assignment v t) =
TermLike.mkEquals sort (TermLike.mkVar $ SomeVariable.mapSomeVariable getRewritingVariable v) $
TermLike.mapVariables getRewritingVariable t

a ||| b = \v -> a v || b v

-- Step StepRequest{} -> pure $ Right $ Step $ StepResult []
Implies ImpliesRequest{antecedent, consequent, _module, logSuccessfulSimplifications, logTiming} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do
Expand Down
Loading

0 comments on commit 7e2b8b3

Please sign in to comment.