Skip to content

Commit c4a7dec

Browse files
geo2ageo2a
committed
Refactor requires check, use syntactic clauses
1 parent cb02384 commit c4a7dec

File tree

1 file changed

+252
-102
lines changed

1 file changed

+252
-102
lines changed

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

+252-102
Original file line numberDiff line numberDiff line change
@@ -842,10 +842,25 @@ applyEquation term rule =
842842
-- check required constraints from lhs.
843843
-- Reaction on false/indeterminate varies depending on the equation's type (function/simplification),
844844
-- see @handleSimplificationEquation@ and @handleFunctionEquation@
845-
checkRequires subst
846845

847-
-- check ensured conditions, filter any true ones, prune if any is false
848-
ensuredConditions <- checkEnsures subst
846+
-- instantiate the requires clause with the obtained substitution
847+
let rawRequired =
848+
concatMap
849+
splitBoolPredicates
850+
rule.requires
851+
-- required = map (coerce . substituteInTerm subst . coerce) rawRequired
852+
knownPredicates <- (.predicates) <$> lift getState
853+
854+
let (syntacticRequires, restRequires) = case rule.attributes.syntacticClauses of
855+
SyntacticClauses [] -> ([], rawRequired)
856+
SyntacticClauses _syntactic -> ([head rawRequired], tail rawRequired) -- TODO should use _syntactic to select
857+
858+
-- check required conditions
859+
withContext CtxConstraint $
860+
checkRequires subst (Set.toList knownPredicates) syntacticRequires restRequires
861+
862+
-- check all ensured conditions together with the path condition
863+
ensuredConditions <- checkEnsures rule subst
849864
lift $ pushConstraints $ Set.fromList ensuredConditions
850865

851866
-- when a new path condition is added, invalidate the equation cache
@@ -856,46 +871,9 @@ applyEquation term rule =
856871
\s -> s{cache = s.cache{equations = mempty}}
857872
pure $ substituteInTerm subst rule.rhs
858873
where
859-
filterOutKnownConstraints :: Set Predicate -> [Predicate] -> EquationT io [Predicate]
860-
filterOutKnownConstraints priorKnowledge constraitns = do
861-
let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns
862-
unless (null knownTrue) $
863-
getPrettyModifiers >>= \case
864-
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
865-
logMessage $
866-
renderOneLineText $
867-
"Known true side conditions (won't check):"
868-
<+> hsep (intersperse "," $ map (pretty' @mods) knownTrue)
869-
pure toCheck
870-
871-
-- Simplify given predicate in a nested EquationT execution.
872-
-- Call 'whenBottom' if it is Bottom, return Nothing if it is Top,
873-
-- otherwise return the simplified remaining predicate.
874-
checkConstraint whenBottom (Predicate p) = withContext CtxConstraint $ do
875-
let fallBackToUnsimplifiedOrBottom :: EquationFailure -> EquationT io Term
876-
fallBackToUnsimplifiedOrBottom = \case
877-
UndefinedTerm{} -> pure FalseBool
878-
_ -> pure p
879-
-- exceptions need to be handled differently in the recursion,
880-
-- falling back to the unsimplified constraint instead of aborting.
881-
simplified <-
882-
lift $ simplifyConstraint' True p `catch_` fallBackToUnsimplifiedOrBottom
883-
case simplified of
884-
FalseBool -> do
885-
throwE . whenBottom $ coerce p
886-
TrueBool -> pure Nothing
887-
other -> pure . Just $ coerce other
888-
889874
allMustBeConcrete (AllConstrained Concrete) = True
890875
allMustBeConcrete _ = False
891876

892-
checkConcreteness ::
893-
Concreteness ->
894-
Map Variable Term ->
895-
ExceptT
896-
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
897-
(EquationT io)
898-
()
899877
checkConcreteness Unconstrained _ = pure ()
900878
checkConcreteness (AllConstrained constrained) subst =
901879
mapM_ (\(var, t) -> mkCheck (toPair var) constrained t) $ Map.assocs subst
@@ -942,74 +920,246 @@ applyEquation term rule =
942920
check
943921
$ Map.lookup Variable{variableSort = SortApp sortName [], variableName} subst
944922

945-
checkRequires ::
946-
Substitution ->
947-
ExceptT
948-
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
949-
(EquationT io)
950-
()
951-
checkRequires matchingSubst = do
952-
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
953-
-- instantiate the requires clause with the obtained substitution
954-
let required =
955-
concatMap
956-
(splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce)
957-
rule.requires
958-
-- If the required condition is _syntactically_ present in
959-
-- the prior (known constraints), we don't check it.
960-
knownPredicates <- (.predicates) <$> lift getState
961-
toCheck <- lift $ filterOutKnownConstraints knownPredicates required
923+
filterOutKnownConstraints ::
924+
forall io.
925+
LoggerMIO io =>
926+
Set Predicate ->
927+
[Predicate] ->
928+
EquationT io [Predicate]
929+
filterOutKnownConstraints priorKnowledge constraitns = do
930+
let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns
931+
unless (null knownTrue) $
932+
getPrettyModifiers >>= \case
933+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
934+
logMessage $
935+
renderOneLineText $
936+
"Known true side conditions (won't check):"
937+
<+> hsep (intersperse "," $ map (pretty' @mods) knownTrue)
938+
pure toCheck
962939

963-
-- check the filtered requires clause conditions
964-
unclearConditions <-
965-
catMaybes
966-
<$> mapM
967-
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p)
940+
checkRequires ::
941+
forall io.
942+
LoggerMIO io =>
943+
Substitution ->
944+
[Predicate] ->
945+
[Predicate] ->
946+
[Predicate] ->
947+
ExceptT
948+
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
949+
(EquationT io)
950+
()
951+
checkRequires currentSubst knownPredicates syntacticRequires restRequires' = do
952+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
953+
case syntacticRequires of
954+
[] -> checkRequiresSemantically currentSubst (Set.fromList knownPredicates) restRequires'
955+
_ ->
956+
withContext CtxSyntactic $
957+
checkRequiresSyntactically
958+
syntacticRequires
959+
currentSubst
960+
knownPredicates
961+
restRequires'
962+
963+
checkRequiresSyntactically ::
964+
forall io.
965+
LoggerMIO io =>
966+
[Predicate] ->
967+
Substitution ->
968+
[Predicate] ->
969+
[Predicate] ->
970+
ExceptT
971+
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
972+
(EquationT io)
973+
()
974+
checkRequiresSyntactically syntacticRequires currentSubst knownPredicates restRequires' = do
975+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
976+
case syntacticRequires of
977+
[] ->
978+
unless (null restRequires') $
979+
-- no more @syntacticRequires@, but unresolved conditions remain: abort
980+
throwRemainingRequires currentSubst restRequires'
981+
(headSyntacticRequires : restSyntacticRequires) -> do
982+
koreDef <- (.definition) <$> lift getConfig
983+
case knownPredicates of
984+
[] ->
985+
unless (null restRequires') $
986+
-- no more @knownPredicates@, but unresolved conditions remain: abort
987+
throwRemainingRequires currentSubst restRequires'
988+
(c : cs) -> case matchTermsWithSubst Eval koreDef currentSubst (coerce headSyntacticRequires) (coerce c) of
989+
MatchFailed{} -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires'
990+
MatchIndeterminate{} -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires'
991+
MatchSuccess newSubst ->
992+
-- we got a substitution from matching @headSyntacticRequires@ against the clause @c@ of the path condition,
993+
-- try applying it to @syntacticRequires <> restRequires'@, simplifying that with LLVM,
994+
-- and filtering from the path condition
995+
( do
996+
withContext CtxSubstitution
997+
$ logMessage
998+
$ WithJsonMessage
999+
(object ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList newSubst)])
1000+
$ renderOneLineText
1001+
$ "Substitution:"
1002+
<+> ( hsep $
1003+
intersperse "," $
1004+
map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $
1005+
Map.toList newSubst
1006+
)
1007+
1008+
let substitited = map (coerce . substituteInTerm newSubst . coerce) (syntacticRequires <> restRequires')
1009+
simplified <- coerce <$> mapM simplifyWithLLVM substitited
1010+
stillUnclear <- lift $ filterOutKnownConstraints (Set.fromList knownPredicates) simplified
1011+
case stillUnclear of
1012+
[] -> pure () -- done
1013+
_ -> do
1014+
logMessage $
1015+
renderOneLineText
1016+
( "Uncertain about conditions in syntactic simplification rule: "
1017+
<+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
1018+
)
1019+
-- @newSubst@ does not solve the conditions completely, repeat the process for @restSyntacticRequires@
1020+
-- using the learned @newSubst@
1021+
checkRequiresSyntactically restSyntacticRequires newSubst knownPredicates restRequires'
1022+
)
1023+
`catchE` ( \case
1024+
(_, IndeterminateCondition{}) -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires'
1025+
(_, ConditionFalse{}) -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires'
1026+
err -> throwE err
1027+
)
1028+
where
1029+
simplifyWithLLVM term = do
1030+
simplified <-
1031+
lift $
1032+
simplifyConstraint' False term
1033+
`catch_` ( \case
1034+
UndefinedTerm{} -> pure FalseBool
1035+
_ -> pure term
1036+
)
1037+
case simplified of
1038+
FalseBool -> do
1039+
throwE
1040+
( \ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text)
1041+
, ConditionFalse . coerce $ term
9681042
)
969-
toCheck
1043+
other -> pure other
9701044

971-
-- unclear conditions may have been simplified and
972-
-- could now be syntactically present in the path constraints, filter again
973-
stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions
1045+
throwRemainingRequires subst preds = do
1046+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
1047+
let substintuted = map (substituteInPredicate subst) preds
1048+
throwE
1049+
( \ctx ->
1050+
ctx . logMessage $
1051+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) preds]) $
1052+
renderOneLineText
1053+
( "Uncertain about conditions in syntactic simplification rule: "
1054+
<+> hsep (intersperse "," $ map (pretty' @mods) substintuted)
1055+
)
1056+
, IndeterminateCondition restRequires'
1057+
)
9741058

975-
solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig
1059+
checkRequiresSemantically ::
1060+
forall io.
1061+
LoggerMIO io =>
1062+
Substitution ->
1063+
Set Predicate ->
1064+
[Predicate] ->
1065+
ExceptT
1066+
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
1067+
(EquationT io)
1068+
()
1069+
checkRequiresSemantically currentSubst knownPredicates restRequires' = do
1070+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
1071+
1072+
-- apply current substitution to restRequires
1073+
let restRequires = map (coerce . substituteInTerm currentSubst . coerce) restRequires'
1074+
toCheck <- lift $ filterOutKnownConstraints knownPredicates restRequires
1075+
unclearRequires <-
1076+
catMaybes
1077+
<$> mapM
1078+
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p)
1079+
)
1080+
toCheck
9761081

977-
-- check any conditions that are still unclear with the SMT solver
978-
-- (or abort if no solver is being used), abort if still unclear after
979-
unless (null stillUnclear) $
980-
lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case
981-
SMT.IsUnknown{} -> do
982-
-- no solver or still unclear: abort
983-
throwE
984-
( \ctx ->
985-
ctx . logMessage $
986-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
987-
renderOneLineText
988-
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
989-
)
990-
, IndeterminateCondition stillUnclear
991-
)
992-
SMT.IsInvalid -> do
993-
-- actually false given path condition: fail
994-
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
995-
throwE
996-
( \ctx ->
997-
ctx . logMessage $
998-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
999-
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
1000-
, ConditionFalse failedP
1001-
)
1002-
SMT.IsValid{} -> do
1003-
-- can proceed
1004-
pure ()
1082+
-- unclear conditions may have been simplified and
1083+
-- could now be syntactically present in the path constraints, filter again
1084+
stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearRequires
10051085

1006-
checkEnsures ::
1007-
Substitution ->
1008-
ExceptT
1009-
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
1010-
(EquationT io)
1011-
[Predicate]
1012-
checkEnsures matchingSubst = do
1086+
-- check unclear requires-clauses in the context of known constraints (prior)
1087+
solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig
1088+
1089+
-- check any conditions that are still unclear with the SMT solver
1090+
-- (or abort if no solver is being used), abort if still unclear after
1091+
unless (null stillUnclear) $
1092+
lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case
1093+
SMT.IsUnknown{} -> do
1094+
-- no solver or still unclear: abort
1095+
throwE
1096+
( \ctx ->
1097+
ctx . logMessage $
1098+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
1099+
renderOneLineText
1100+
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
1101+
)
1102+
, IndeterminateCondition stillUnclear
1103+
)
1104+
SMT.IsInvalid -> do
1105+
-- actually false given path condition: fail
1106+
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
1107+
throwE
1108+
( \ctx ->
1109+
ctx . logMessage $
1110+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
1111+
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
1112+
, ConditionFalse failedP
1113+
)
1114+
SMT.IsValid{} -> do
1115+
-- can proceed
1116+
pure ()
1117+
1118+
-- Simplify given predicate in a nested EquationT execution.
1119+
-- Call 'whenBottom' if it is Bottom, return Nothing if it is Top,
1120+
-- otherwise return the simplified remaining predicate.
1121+
checkConstraint ::
1122+
forall io.
1123+
LoggerMIO io =>
1124+
( Predicate ->
1125+
( (EquationT io () -> EquationT io ()) -> EquationT io ()
1126+
, ApplyEquationFailure
1127+
)
1128+
) ->
1129+
Predicate ->
1130+
ExceptT
1131+
( (EquationT io () -> EquationT io ()) -> EquationT io ()
1132+
, ApplyEquationFailure
1133+
)
1134+
(EquationT io)
1135+
(Maybe Predicate)
1136+
checkConstraint whenBottom (Predicate p) = withContext CtxConstraint $ do
1137+
let fallBackToUnsimplifiedOrBottom :: EquationFailure -> EquationT io Term
1138+
fallBackToUnsimplifiedOrBottom = \case
1139+
UndefinedTerm{} -> pure FalseBool
1140+
_ -> pure p
1141+
-- exceptions need to be handled differently in the recursion,
1142+
-- falling back to the unsimplified constraint instead of aborting.
1143+
simplified <-
1144+
lift $ simplifyConstraint' True p `catch_` fallBackToUnsimplifiedOrBottom
1145+
case simplified of
1146+
FalseBool -> do
1147+
throwE . whenBottom $ coerce p
1148+
TrueBool -> pure Nothing
1149+
other -> pure . Just $ coerce other
1150+
1151+
checkEnsures ::
1152+
forall io tag.
1153+
LoggerMIO io =>
1154+
RewriteRule tag ->
1155+
Substitution ->
1156+
ExceptT
1157+
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
1158+
(EquationT io)
1159+
[Predicate]
1160+
checkEnsures
1161+
rule
1162+
matchingSubst = do
10131163
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
10141164
let ensured =
10151165
concatMap

0 commit comments

Comments
 (0)