Skip to content

Commit 5c53adb

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 286b525 + aaf0ef5 commit 5c53adb

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+693
-2245
lines changed

‎booster/library/Booster/JsonRpc.hs

+34-38
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ import Booster.Definition.Base qualified as Definition (RewriteRule (..))
4444
import Booster.LLVM as LLVM (API)
4545
import Booster.Log
4646
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
47-
import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
47+
import Booster.Pattern.Base (Pattern (..), Sort (SortApp))
4848
import Booster.Pattern.Base qualified as Pattern
4949
import Booster.Pattern.Implies (runImplies)
5050
import Booster.Pattern.Pretty
@@ -55,12 +55,11 @@ import Booster.Pattern.Rewrite (
5555
RewriteTrace (..),
5656
performRewrite,
5757
)
58+
import Booster.Pattern.Substitution qualified as Substitution
5859
import Booster.Pattern.Util (
5960
freeVariables,
6061
sortOfPattern,
6162
sortOfTerm,
62-
substituteInPredicate,
63-
substituteInTerm,
6463
)
6564
import Booster.Prettyprinter (renderText)
6665
import Booster.SMT.Interface qualified as SMT
@@ -69,6 +68,7 @@ import Booster.Syntax.Json.Externalise
6968
import Booster.Syntax.Json.Internalise (
7069
InternalisedPredicates (..),
7170
TermOrPredicates (..),
71+
extractSubstitution,
7272
internalisePattern,
7373
internaliseTermOrPredicate,
7474
logPatternError,
@@ -131,12 +131,14 @@ respond stateVar request =
131131
[ req.logSuccessfulRewrites
132132
, req.logFailedRewrites
133133
]
134-
-- apply the given substitution before doing anything else
134+
-- apply the given substitution before doing anything else,
135+
-- as internalisePattern does not substitute
135136
let substPat =
136137
Pattern
137-
{ term = substituteInTerm substitution term
138-
, constraints = Set.fromList $ map (substituteInPredicate substitution) preds
138+
{ term = Substitution.substituteInTerm substitution term
139+
, constraints = Set.fromList $ map (Substitution.substituteInPredicate substitution) preds
139140
, ceilConditions = ceils
141+
, substitution
140142
}
141143
-- remember all variables used in the substitutions
142144
substVars =
@@ -166,7 +168,7 @@ respond stateVar request =
166168
result <-
167169
performRewrite rewriteConfig substPat
168170
SMT.finaliseSolver solver
169-
pure $ execResponse req result substitution unsupported
171+
pure $ execResponse req result unsupported
170172
RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do
171173
-- block other request executions while modifying the server state
172174
state <- liftIO $ takeMVar stateVar
@@ -244,20 +246,14 @@ respond stateVar request =
244246
RpcError.CouldNotVerifyPattern $
245247
map patternErrorToRpcError patternErrors
246248
-- term and predicate (pattern)
247-
Right (TermAndPredicates pat substitution unsupported) -> do
249+
-- NOTE: the input substitution will have already been applied by internaliseTermOrPredicate
250+
Right (TermAndPredicates pat unsupported) -> do
248251
unless (null unsupported) $ do
249252
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
250253
logMessage ("ignoring unsupported predicate parts" :: Text)
251-
-- apply the given substitution before doing anything else
252-
let substPat =
253-
Pattern
254-
{ term = substituteInTerm substitution pat.term
255-
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
256-
, ceilConditions = pat.ceilConditions
257-
}
258-
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case
254+
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty pat >>= \case
259255
(Right newPattern, _) -> do
260-
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
256+
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
261257
tSort = externaliseSort (sortOfPattern newPattern)
262258
result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
263259
[] -> term
@@ -281,23 +277,24 @@ respond stateVar request =
281277
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
282278
logMessage ("ignoring unsupported predicate parts" :: Text)
283279
-- apply the given substitution before doing anything else
284-
let predicates = map (substituteInPredicate ps.substitution) ps.boolPredicates
280+
let predicates = map (Substitution.substituteInPredicate ps.substitution) ps.boolPredicates
285281
withContext CtxConstraint $
286282
ApplyEquations.simplifyConstraints
287283
def
288284
mLlvmLibrary
289285
solver
290286
mempty
291-
predicates
287+
(predicates <> Substitution.asEquations ps.substitution)
292288
>>= \case
293-
(Right newPreds, _) -> do
289+
(Right simplified, _) -> do
294290
let predicateSort =
295291
fromMaybe (error "not a predicate") $
296292
sortOfJson req.state.term
293+
(simplifiedSubstitution, simplifiedPredicates) = extractSubstitution simplified
297294
result =
298-
map (externalisePredicate predicateSort) newPreds
295+
map (externalisePredicate predicateSort) (Set.toList simplifiedPredicates)
299296
<> map (externaliseCeil predicateSort) ps.ceilPredicates
300-
<> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
297+
<> map (uncurry $ externaliseSubstitution predicateSort) (Map.assocs simplifiedSubstitution)
301298
<> ps.unsupported
302299

303300
pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
@@ -332,7 +329,7 @@ respond stateVar request =
332329
-- term and predicates were sent. Only work on predicates
333330
(boolPs, suppliedSubst) <-
334331
case things of
335-
TermAndPredicates pat substitution unsupported -> do
332+
TermAndPredicates pat unsupported -> do
336333
withContext CtxGetModel $
337334
logMessage' ("ignoring supplied terms and only checking predicates" :: Text)
338335

@@ -341,7 +338,7 @@ respond stateVar request =
341338
logMessage' ("ignoring unsupported predicates" :: Text)
342339
withContext CtxDetail $
343340
logMessage (Text.unwords $ map prettyPattern unsupported)
344-
pure (Set.toList pat.constraints, substitution)
341+
pure (Set.toList pat.constraints, pat.substitution)
345342
Predicates ps -> do
346343
unless (null ps.ceilPredicates && null ps.unsupported) $ do
347344
withContext CtxGetModel $ do
@@ -472,21 +469,20 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} =
472469
execResponse ::
473470
RpcTypes.ExecuteRequest ->
474471
(Natural, Seq (RewriteTrace ()), RewriteResult Pattern) ->
475-
Map Variable Term ->
476472
[Syntax.KorePattern] ->
477473
Either ErrorObj (RpcTypes.API 'RpcTypes.Res)
478-
execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
474+
execResponse req (d, traces, rr) unsupported = case rr of
479475
RewriteBranch p nexts ->
480476
Right $
481477
RpcTypes.Execute
482478
RpcTypes.ExecuteResult
483479
{ reason = RpcTypes.Branching
484480
, depth
485481
, logs
486-
, state = toExecState p originalSubstitution unsupported Nothing
482+
, state = toExecState p unsupported Nothing
487483
, nextStates =
488484
Just $
489-
map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported (Just muid)) $
485+
map (\(_, muid, p') -> toExecState p' unsupported (Just muid)) $
490486
toList nexts
491487
, rule = Nothing
492488
, unknownPredicate = Nothing
@@ -498,7 +494,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
498494
{ reason = RpcTypes.Stuck
499495
, depth
500496
, logs
501-
, state = toExecState p originalSubstitution unsupported Nothing
497+
, state = toExecState p unsupported Nothing
502498
, nextStates = Nothing
503499
, rule = Nothing
504500
, unknownPredicate = Nothing
@@ -510,7 +506,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
510506
{ reason = RpcTypes.Vacuous
511507
, depth
512508
, logs
513-
, state = toExecState p originalSubstitution unsupported Nothing
509+
, state = toExecState p unsupported Nothing
514510
, nextStates = Nothing
515511
, rule = Nothing
516512
, unknownPredicate = Nothing
@@ -522,8 +518,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
522518
{ reason = RpcTypes.CutPointRule
523519
, depth
524520
, logs
525-
, state = toExecState p originalSubstitution unsupported Nothing
526-
, nextStates = Just [toExecState next originalSubstitution unsupported Nothing]
521+
, state = toExecState p unsupported Nothing
522+
, nextStates = Just [toExecState next unsupported Nothing]
527523
, rule = Just lbl
528524
, unknownPredicate = Nothing
529525
}
@@ -534,7 +530,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
534530
{ reason = RpcTypes.TerminalRule
535531
, depth
536532
, logs
537-
, state = toExecState p originalSubstitution unsupported Nothing
533+
, state = toExecState p unsupported Nothing
538534
, nextStates = Nothing
539535
, rule = Just lbl
540536
, unknownPredicate = Nothing
@@ -546,7 +542,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
546542
{ reason = RpcTypes.DepthBound
547543
, depth
548544
, logs
549-
, state = toExecState p originalSubstitution unsupported Nothing
545+
, state = toExecState p unsupported Nothing
550546
, nextStates = Nothing
551547
, rule = Nothing
552548
, unknownPredicate = Nothing
@@ -563,7 +559,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
563559
(logSuccessfulRewrites, logFailedRewrites)
564560
(RewriteStepFailed failure)
565561
in logs <|> abortRewriteLog
566-
, state = toExecState p originalSubstitution unsupported Nothing
562+
, state = toExecState p unsupported Nothing
567563
, nextStates = Nothing
568564
, rule = Nothing
569565
, unknownPredicate = Nothing
@@ -586,8 +582,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
586582
xs@(_ : _) -> Just xs
587583

588584
toExecState ::
589-
Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
590-
toExecState pat sub unsupported muid =
585+
Pattern -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
586+
toExecState pat unsupported muid =
591587
RpcTypes.ExecuteState
592588
{ term = addHeader t
593589
, predicate = addHeader <$> addUnsupported p
@@ -597,7 +593,7 @@ toExecState pat sub unsupported muid =
597593
, ruleId = getUniqueId <$> muid
598594
}
599595
where
600-
(t, p, s) = externalisePattern pat sub
596+
(t, p, s) = externalisePattern pat
601597
termSort = externaliseSort $ sortOfPattern pat
602598
allUnsupported = Syntax.KJAnd termSort unsupported
603599
addUnsupported

‎booster/library/Booster/JsonRpc/Utils.hs

+1-10
Original file line numberDiff line numberDiff line change
@@ -279,18 +279,9 @@ diffBy def pat1 pat2 =
279279
<> if null ps.unsupported
280280
then ""
281281
else BS.unlines ("Unsupported parts:" : map Json.encode ps.unsupported)
282-
renderBS (TermAndPredicates p m u) =
282+
renderBS (TermAndPredicates p u) =
283283
( BS.pack . renderDefault $
284284
pretty (PrettyWithModifiers @['Decoded, 'Truncated] p)
285-
<+> vsep
286-
( map
287-
( \(k, v) ->
288-
pretty (PrettyWithModifiers @['Decoded, 'Truncated] k)
289-
<+> "="
290-
<+> pretty (PrettyWithModifiers @['Decoded, 'Truncated] v)
291-
)
292-
(Map.toList m)
293-
)
294285
)
295286
<> if null u then "" else BS.unlines ("Unsupported parts: " : map Json.encode u)
296287
internalise =

‎booster/library/Booster/Log.hs

+3-2
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,7 @@ import Booster.Pattern.Base (
6969
pattern AndTerm,
7070
)
7171
import Booster.Pattern.Pretty
72+
import Booster.Pattern.Substitution (asEquations)
7273
import Booster.Prettyprinter (renderOneLineText)
7374
import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern)
7475
import Booster.Syntax.Json.Externalise (externaliseTerm)
@@ -185,8 +186,8 @@ withTermContext t@(Term attrs _) m =
185186
m
186187

187188
withPatternContext :: LoggerMIO m => Pattern -> m a -> m a
188-
withPatternContext Pattern{term, constraints} m =
189-
let t' = foldl' AndTerm term $ Set.toList $ Set.map coerce constraints -- FIXME
189+
withPatternContext Pattern{term, constraints, substitution} m =
190+
let t' = foldl' AndTerm term . map coerce $ Set.toList constraints <> asEquations substitution
190191
in withTermContext t' m
191192

192193
instance ToLogFormat KorePattern where

‎booster/library/Booster/Pattern/ApplyEquations.hs

+25-2
Original file line numberDiff line numberDiff line change
@@ -66,10 +66,12 @@ import Booster.Pattern.Bool
6666
import Booster.Pattern.Index qualified as Idx
6767
import Booster.Pattern.Match
6868
import Booster.Pattern.Pretty
69+
import Booster.Pattern.Substitution
6970
import Booster.Pattern.Util
7071
import Booster.Prettyprinter (renderOneLineText)
7172
import Booster.SMT.Interface qualified as SMT
7273
import Booster.Syntax.Json.Externalise (externaliseTerm)
74+
import Booster.Syntax.Json.Internalise (extractSubstitution)
7375
import Booster.Util (Bound (..))
7476
import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached))
7577
import Kore.Util (showHashHex)
@@ -455,7 +457,15 @@ evaluatePattern ::
455457
Pattern ->
456458
io (Either EquationFailure Pattern, SimplifierCache)
457459
evaluatePattern def mLlvmLibrary smtSolver cache pat =
458-
runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat
460+
runEquationT
461+
def
462+
mLlvmLibrary
463+
smtSolver
464+
cache
465+
-- interpret substitution as additional known constraints
466+
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
467+
. evaluatePattern'
468+
$ pat
459469

460470
-- version for internal nested evaluation
461471
evaluatePattern' ::
@@ -469,7 +479,20 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
469479
traverse_ simplifyAssumedPredicate . predicates =<< getState
470480
-- this may yield additional new constraints, left unevaluated
471481
evaluatedConstraints <- predicates <$> getState
472-
pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions}
482+
-- The interface-level evaluatePattern puts pat.substitution together with pat.constraints
483+
-- into the simplifier state as known truth. Here the substitution will bubble-up as part of
484+
-- evaluatedConstraints. To avoid duplicating constraints (i.e. having equivalent entities
485+
-- in pat.predicate and pat.substitution), we discard the old substitution here
486+
-- and extract a possible simplified one from evaluatedConstraints.
487+
let (simplifiedSubsitution, simplifiedConstraints) = extractSubstitution (Set.toList evaluatedConstraints)
488+
489+
pure
490+
Pattern
491+
{ constraints = simplifiedConstraints
492+
, term = newTerm
493+
, ceilConditions
494+
, substitution = simplifiedSubsitution
495+
}
473496
where
474497
-- when TooManyIterations exception occurred while evaluating the top-level term,
475498
-- i.e. not in a recursive evaluation of a side-condition,

‎booster/library/Booster/Pattern/Base.hs

+6-2
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ import Data.Functor.Foldable
3636
import Data.Hashable (Hashable)
3737
import Data.Hashable qualified as Hashable
3838
import Data.List as List (foldl', foldl1', sort)
39+
import Data.Map.Strict (Map)
3940
import Data.Set (Set)
4041
import Data.Set qualified as Set
4142
import GHC.Generics (Generic)
@@ -761,19 +762,22 @@ pattern KSeq sort a =
761762

762763
--------------------
763764

765+
type Substitution = Map Variable Term
766+
764767
-- | A term (configuration) constrained by a number of predicates.
765768
data Pattern = Pattern
766769
{ term :: Term
767770
, constraints :: !(Set Predicate)
771+
, substitution :: Substitution
768772
, ceilConditions :: ![Ceil]
769773
}
770774
deriving stock (Eq, Ord, Show, Generic, Data)
771775
deriving anyclass (NFData)
772776

773777
pattern Pattern_ :: Term -> Pattern
774-
pattern Pattern_ t <- Pattern t _ _
778+
pattern Pattern_ t <- Pattern t _ _ _
775779
where
776-
Pattern_ t = Pattern t mempty mempty
780+
Pattern_ t = Pattern t mempty mempty mempty
777781

778782
pattern ConsApplication :: Symbol -> [Sort] -> [Term] -> Term
779783
pattern ConsApplication sym sorts args <-

‎booster/library/Booster/Pattern/Binary.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -564,7 +564,7 @@ decodePattern mDef = do
564564
preds <- forM preds' $ \case
565565
BPredicate pIdx -> Predicate <$> getTerm pIdx
566566
_ -> fail "Expecting a predicate"
567-
pure $ Pattern trm (Set.fromList preds) mempty
567+
pure $ Pattern trm (Set.fromList preds) mempty mempty
568568
_ -> fail "Expecting a term on the top of the stack"
569569

570570
encodeMagicHeaderAndVersion :: Version -> Put

‎booster/library/Booster/Pattern/Bool.hs

+1-2
Original file line numberDiff line numberDiff line change
@@ -36,11 +36,10 @@ import Booster.Definition.Attributes.Base (
3636
pattern IsNotMacroOrAlias,
3737
)
3838
import Booster.Pattern.Base (
39-
Pattern,
39+
Pattern (..),
4040
Predicate (..),
4141
Symbol (Symbol),
4242
Term,
43-
constraints,
4443
pattern DomainValue,
4544
pattern SortBool,
4645
pattern SortInt,

0 commit comments

Comments
 (0)