Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

kore-rpc - Return branch rule id and condition #3716

Merged
merged 20 commits into from
Feb 7, 2024
Merged

kore-rpc - Return branch rule id and condition #3716

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
dedac19
remove multior form result and push branching into LogicT
goodlyrottenapple Jan 24, 2024
6f49c6c
Merge branch 'master' into sam/result-multior-cleanup
goodlyrottenapple Jan 24, 2024
a438402
Format with fourmolu
invalid-email-address Jan 24, 2024
241cfc8
fix unit tests
goodlyrottenapple Jan 24, 2024
4b87339
start work on returning condition in program state
goodlyrottenapple Jan 25, 2024
28d0de8
merge master
goodlyrottenapple Jan 26, 2024
6ce3025
return rule substitution and condition
goodlyrottenapple Jan 26, 2024
edb04ac
Format with fourmolu
invalid-email-address Jan 30, 2024
ddfcb64
update tests
goodlyrottenapple Jan 31, 2024
3f63fc2
fourmolu
goodlyrottenapple Jan 31, 2024
9dc632a
fix unit tests
goodlyrottenapple Jan 31, 2024
5310cc5
pull out any variables arising from equations back into a predicate
goodlyrottenapple Feb 2, 2024
0f5957e
Format with fourmolu
invalid-email-address Feb 2, 2024
5b9a548
refactor rule data into RuleInfo, fix tests
goodlyrottenapple Feb 2, 2024
bdd80ee
mrge
goodlyrottenapple Feb 2, 2024
673e9bb
switch back to substitution field, only emit ruleInfo on branching + …
goodlyrottenapple Feb 2, 2024
5b80835
revert tests
goodlyrottenapple Feb 2, 2024
dd1a267
revert to rule-substitution
goodlyrottenapple Feb 2, 2024
e3c9e9b
restore substitution field
goodlyrottenapple Feb 2, 2024
171e553
fix integration test
goodlyrottenapple Feb 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion kore-rpc-types/src/Kore/JsonRpc/Types.hs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading