Skip to content

Commit

Permalink
Remove states from RPC logs, include only rule unique IDs (#484)
Browse files Browse the repository at this point in the history 
This PR removes the states from Booster's rewrite and equation traces.
Only rule unique IDs are included in the RPC logs now.

Here's a quick performance comparison on the execute request
`test-fountry-bug-report/state-007.send` with `log-successful-rewrites`
and `log-successful-simplifications` set to `true`:

| Git revision | Time | Comment |

|:--------------------------------------|:-----------|----------------------------------------------------|
| georgy/rpc-logs-only-labels | 3.286555 s | this PR |
| main (0ef6ecd) | 3.259145294| Georgy's log fix reverted |
| 0096f93 | 35s | logs with states, `-N` still there |

The performance with unique IDs only seems to be on par with not
collecting traces at all.

I have also checked that:

- [x] we still emit rewrite logs with states to `stderr` when `-l
Rewrite/RewriteSuccess` is passed and `log-successful/failed-rewrites:
false`
- [x] we still emit simplification logs with states to `stderr` when `-l
Simplify/SimplifySuccess` is passed and
`log-successful/failed-simplifications: false `


# Summary of changes

The idea is to stop accumulating states in `RewriteTrace`s and
`EquationTrace`s while still keeping the possibility to emit them in
`stderr` logs and possibly stream them to the client in future.

## Refactoring of `EquationTrace`

* the `EquationMetadata` type is introduced to hold an equation's
location, rule label and unique id information
* `EquationTrace` is split into two constructors, `EquationApplied` and
`EquationNotApplied`, where the former can hold the post-term, and the
latter an `ApplyEquationResult`
* `EquationTrace` is made parametric in the term type, similar to
`RewriteTrace`. The old `EquationTrace` now becomes `EquationTrace Term`
* a function `eraseStates :: EquationTrace Term -> EquationTrace ()` is
added to remove the terms from a trace, leaving only metadata. This
function will be called in the rewriting code to erase the states from
the equation traces.

## Refactoring of `RewriteTrace`

* The `RewriteSimplified` data constructor is changed to accommodate the
parametricity of `EquationTrace`. Since `EquationTrace` usually holds a
`Term`, rather than a `Pattern`, we need the `TracePayload` type family
to connect the two. The intention is to use `RewriteTrace ()`
everywhere, and all the parametricity is only needed to make the code
changes minimal. Once we are happy with the API, we could remove
parameters from both `RewriteTrace` and `EquationTrace`.
* As with `EquationTrace`, a we now have the `eraseStates ::
RewriteTrace Pattern -> RewriteTrace ()` function that drops the patters
from the traces. It also erases the states in euqational traces stored
in `RewriteSimplified` constructors.


# Future work

The `ApplyEquationResult` holds one success and several error cases: 

```haskell
data ApplyEquationResult
    = Success Term
    | FailedMatch MatchFailReason
    | IndeterminateMatch
    | IndeterminateCondition [Predicate]
    | ConditionFalse Predicate
    | EnsuresFalse Predicate
    | RuleNotPreservingDefinedness
    | MatchConstraintViolated Constrained VarName
```

I think it would be cleaner to factor out the error cases into a
separate type:

```haskell
data ApplyEquationFailureReason
    = FailedMatch MatchFailReason
    | IndeterminateMatch
    | IndeterminateCondition [Predicate]
    | ConditionFalse Predicate
    | EnsuresFalse Predicate
    | RuleNotPreservingDefinedness
    | MatchConstraintViolated Constrained VarName

data ApplyEquationResult
    = ApplyEquationSuccess Term
    | ApplyEquationFailure ApplyEquationFailureReason
```

This would make `EquationTrace` cleaner, as currently it can have
represent absurd case of `EquationNotApplied ... Success`.

---------

Co-authored-by: Samuel Balco <goodlyrottenapple@gmail.com>
  • Loading branch information
@geo2a @goodlyrottenapple
geo2a and goodlyrottenapple authored Feb 1, 2024
1 parent 3ee0794 commit a15ebef
Show file tree
Hide file tree
Showing 10 changed files with 198 additions and 1,825 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/test.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ concurrency:

env:
ghc_version: '9.2.8'
hlint_version: '3.4.1'
hlint_version: '3.5'
fourmolu_version: '0.12.0.0'
hpack_version: '0.34.2'

Expand Down
189 changes: 104 additions & 85 deletions library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -330,7 +330,7 @@ respond stateVar =
mkSimplifyResponse state traceData =
RpcTypes.Simplify
RpcTypes.SimplifyResult{state, logs = mkTraces duration traceData}
pure $ second (uncurry mkSimplifyResponse) result
pure $ second (uncurry mkSimplifyResponse) (fmap (second (map ApplyEquations.eraseStates)) result)
RpcTypes.GetModel req -> withContext req._module $ \case
(_, _, Nothing) -> do
Log.logErrorNS "booster" "get-model request, not supported without SMT solver"
Expand Down Expand Up @@ -514,7 +514,7 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} =
execResponse ::
Maybe Double ->
RpcTypes.ExecuteRequest ->
(Natural, Seq (RewriteTrace Pattern), RewriteResult Pattern) ->
(Natural, Seq (RewriteTrace ()), RewriteResult Pattern) ->
Map Variable Term ->
[Syntax.KorePattern] ->
Either ErrorObj (RpcTypes.API 'RpcTypes.Res)
Expand Down Expand Up @@ -619,21 +619,19 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c

logs =
let traceLogs =
fmap concat
. mapM
concat . catMaybes . toList $
fmap
( mkLogRewriteTrace
(logSuccessfulRewrites, logFailedRewrites)
(logSuccessfulSimplifications, logFailedSimplifications)
)
$ toList traces
traces
timingLog =
fmap (ProcessingTime $ Just Booster) mbDuration
in case (timingLog, traceLogs) of
(Nothing, Nothing) -> Nothing
(Nothing, Just []) -> Nothing
(Nothing, Just xs@(_ : _)) -> Just xs
(Just t, Nothing) -> Just [t]
(Just t, Just xs) -> Just (t : xs)
(Nothing, []) -> Nothing
(Nothing, xs@(_ : _)) -> Just xs
(Just t, xs) -> Just (t : xs)

toExecState :: Pattern -> Map Variable Term -> [Syntax.KorePattern] -> RpcTypes.ExecuteState
toExecState pat sub unsupported =
Expand All @@ -650,108 +648,129 @@ toExecState pat sub unsupported =
| null unsupported = id
| otherwise = maybe (Just allUnsupported) (Just . Syntax.KJAnd termSort . (: unsupported))

mkLogEquationTrace :: (Bool, Bool) -> ApplyEquations.EquationTrace -> Maybe LogEntry
mkLogEquationTrace :: (Bool, Bool) -> ApplyEquations.EquationTrace () -> Maybe LogEntry
mkLogEquationTrace
(logSuccessfulSimplifications, logFailedSimplifications)
ApplyEquations.EquationTrace{subjectTerm, ruleId = uid, result} =
case result of
ApplyEquations.Success rewrittenTrm
| logSuccessfulSimplifications ->
(logSuccessfulSimplifications, logFailedSimplifications) = \case
ApplyEquations.EquationApplied _subjectTerm metadata _rewritten ->
if logSuccessfulSimplifications
then
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result =
Success
{ rewrittenTerm =
Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ rewrittenTrm) mempty mempty
{ rewrittenTerm = Nothing
, substitution = Nothing
, ruleId = fromMaybe "UNKNOWN" _ruleId
}
}
ApplyEquations.FailedMatch _failReason
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result = Failure{reason = "Failed match", _ruleId}
}
ApplyEquations.IndeterminateMatch
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result = Failure{reason = "Indeterminate match", _ruleId}
}
ApplyEquations.IndeterminateCondition _failedConditions
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result = Failure{reason = "Indeterminate side-condition", _ruleId}
}
ApplyEquations.ConditionFalse{}
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result = Failure{reason = "Side-condition is false", _ruleId}
}
ApplyEquations.RuleNotPreservingDefinedness
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result = Failure{reason = "The equation does not preserve definedness", _ruleId}
}
ApplyEquations.MatchConstraintViolated _ varName
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result =
Failure
{ reason = "Symbolic/concrete constraint violated for variable: " <> Text.decodeUtf8 varName
, _ruleId
}
}
_ -> Nothing
where
originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ subjectTerm) mempty mempty
originalTermIndex = Nothing
origin = Booster
_ruleId = fmap getUniqueId uid
else Nothing
where
originalTerm = Nothing
originalTermIndex = Nothing
origin = Booster
_ruleId = fmap getUniqueId metadata.ruleId
ApplyEquations.EquationNotApplied _subjectTerm metadata result ->
case result of
ApplyEquations.Success rewrittenTrm
| logSuccessfulSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result =
Success
{ rewrittenTerm =
Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ rewrittenTrm) mempty mempty
, substitution = Nothing
, ruleId = fromMaybe "UNKNOWN" _ruleId
}
}
ApplyEquations.FailedMatch _failReason
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result = Failure{reason = "Failed match", _ruleId}
}
ApplyEquations.IndeterminateMatch
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result = Failure{reason = "Indeterminate match", _ruleId}
}
ApplyEquations.IndeterminateCondition _failedConditions
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result = Failure{reason = "Indeterminate side-condition", _ruleId}
}
ApplyEquations.ConditionFalse{}
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result = Failure{reason = "Side-condition is false", _ruleId}
}
ApplyEquations.RuleNotPreservingDefinedness
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result = Failure{reason = "The equation does not preserve definedness", _ruleId}
}
ApplyEquations.MatchConstraintViolated _ varName
| logFailedSimplifications ->
Just $
Simplification
{ originalTerm
, originalTermIndex
, origin
, result =
Failure
{ reason = "Symbolic/concrete constraint violated for variable: " <> Text.decodeUtf8 varName
, _ruleId
}
}
_ -> Nothing
where
originalTerm = Nothing
originalTermIndex = Nothing
origin = Booster
_ruleId = fmap getUniqueId metadata.ruleId

mkLogRewriteTrace ::
(Bool, Bool) ->
(Bool, Bool) ->
RewriteTrace Pattern ->
RewriteTrace () ->
Maybe [LogEntry]
mkLogRewriteTrace
(logSuccessfulRewrites, logFailedRewrites)
equationLogOpts@(logSuccessfulSimplifications, logFailedSimplifications) =
\case
RewriteSingleStep _ uid _ res
RewriteSingleStep _ uid _ _res
| logSuccessfulRewrites ->
Just $
singleton $
Rewrite
{ result =
Success
{ rewrittenTerm = Just $ execStateToKoreJson $ toExecState res mempty mempty
{ rewrittenTerm = Nothing
, substitution = Nothing
, ruleId = maybe "UNKNOWN" getUniqueId uid
}
Expand Down
Loading

0 comments on commit a15ebef

Please sign in to comment.