Skip to content

Commit bebd5c0

Browse files
geo2ageo2a
committed
Refactor requires check, use syntactic clauses
1 parent 6b7c601 commit bebd5c0

File tree

1 file changed

+224
-58
lines changed

1 file changed

+224
-58
lines changed

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

Lines changed: 224 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -840,57 +840,20 @@ applyEquation term rule =
840840
)
841841

842842
-- instantiate the requires clause with the obtained substitution
843-
let required =
843+
let rawRequired =
844844
concatMap
845-
(splitBoolPredicates . coerce . substituteInTerm subst . coerce)
845+
splitBoolPredicates
846846
rule.requires
847-
-- If the required condition is _syntactically_ present in
848-
-- the prior (known constraints), we don't check it.
847+
-- required = map (coerce . substituteInTerm subst . coerce) rawRequired
849848
knownPredicates <- (.predicates) <$> lift getState
850-
toCheck <- lift $ filterOutKnownConstraints knownPredicates required
851849

852-
-- check the filtered requires clause conditions
853-
unclearConditions <-
854-
catMaybes
855-
<$> mapM
856-
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p)
857-
)
858-
toCheck
859-
860-
-- unclear conditions may have been simplified and
861-
-- could now be syntactically present in the path constraints, filter again
862-
stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions
863-
864-
solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig
850+
let (syntacticRequires, restRequires) = case rule.attributes.syntacticClauses of
851+
SyntacticClauses [] -> ([], rawRequired)
852+
SyntacticClauses _syntactic -> ([head rawRequired], tail rawRequired) -- TODO should use _syntactic to select
865853

866-
-- check any conditions that are still unclear with the SMT solver
867-
-- (or abort if no solver is being used), abort if still unclear after
868-
unless (null stillUnclear) $
869-
lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case
870-
SMT.IsUnknown{} -> do
871-
-- no solver or still unclear: abort
872-
throwE
873-
( \ctx ->
874-
ctx . logMessage $
875-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
876-
renderOneLineText
877-
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
878-
)
879-
, IndeterminateCondition stillUnclear
880-
)
881-
SMT.IsInvalid -> do
882-
-- actually false given path condition: fail
883-
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
884-
throwE
885-
( \ctx ->
886-
ctx . logMessage $
887-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
888-
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
889-
, ConditionFalse failedP
890-
)
891-
SMT.IsValid{} -> do
892-
-- can proceed
893-
pure ()
854+
-- check required conditions
855+
withContext CtxConstraint $
856+
checkRequires subst (Set.toList knownPredicates) syntacticRequires restRequires
894857

895858
-- check ensured conditions, filter any
896859
-- true ones, prune if any is false
@@ -905,7 +868,9 @@ applyEquation term rule =
905868
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p)
906869
)
907870
ensured
871+
908872
-- check all ensured conditions together with the path condition
873+
solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig
909874
lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
910875
SMT.IsInvalid -> do
911876
let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
@@ -927,18 +892,6 @@ applyEquation term rule =
927892
\s -> s{cache = s.cache{equations = mempty}}
928893
pure $ substituteInTerm subst rule.rhs
929894
where
930-
filterOutKnownConstraints :: Set Predicate -> [Predicate] -> EquationT io [Predicate]
931-
filterOutKnownConstraints priorKnowledge constraitns = do
932-
let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns
933-
unless (null knownTrue) $
934-
getPrettyModifiers >>= \case
935-
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
936-
logMessage $
937-
renderOneLineText $
938-
"Known true side conditions (won't check):"
939-
<+> hsep (intersperse "," $ map (pretty' @mods) knownTrue)
940-
pure toCheck
941-
942895
-- Simplify given predicate in a nested EquationT execution.
943896
-- Call 'whenBottom' if it is Bottom, return Nothing if it is Top,
944897
-- otherwise return the simplified remaining predicate.
@@ -1013,6 +966,219 @@ applyEquation term rule =
1013966
check
1014967
$ Map.lookup Variable{variableSort = SortApp sortName [], variableName} subst
1015968

969+
filterOutKnownConstraints ::
970+
forall io.
971+
LoggerMIO io =>
972+
Set Predicate ->
973+
[Predicate] ->
974+
EquationT io [Predicate]
975+
filterOutKnownConstraints priorKnowledge constraitns = do
976+
let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns
977+
unless (null knownTrue) $
978+
getPrettyModifiers >>= \case
979+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
980+
logMessage $
981+
renderOneLineText $
982+
"Known true side conditions (won't check):"
983+
<+> hsep (intersperse "," $ map (pretty' @mods) knownTrue)
984+
pure toCheck
985+
986+
checkRequires ::
987+
forall io.
988+
LoggerMIO io =>
989+
Substitution ->
990+
[Predicate] ->
991+
[Predicate] ->
992+
[Predicate] ->
993+
ExceptT
994+
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
995+
(EquationT io)
996+
()
997+
checkRequires currentSubst knownPredicates syntacticRequires restRequires' = do
998+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
999+
case syntacticRequires of
1000+
[] -> checkRequiresSemantically currentSubst (Set.fromList knownPredicates) restRequires'
1001+
_ ->
1002+
withContext CtxSyntactic $
1003+
checkRequiresSyntactically
1004+
syntacticRequires
1005+
currentSubst
1006+
knownPredicates
1007+
restRequires'
1008+
1009+
checkRequiresSyntactically ::
1010+
forall io.
1011+
LoggerMIO io =>
1012+
[Predicate] ->
1013+
Substitution ->
1014+
[Predicate] ->
1015+
[Predicate] ->
1016+
ExceptT
1017+
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
1018+
(EquationT io)
1019+
()
1020+
checkRequiresSyntactically syntacticRequires currentSubst knownPredicates restRequires' = do
1021+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
1022+
case syntacticRequires of
1023+
[] ->
1024+
unless (null restRequires') $
1025+
-- no more @syntacticRequires@, but unresolved conditions remain: abort
1026+
throwRemainingRequires currentSubst restRequires'
1027+
(headSyntacticRequires : restSyntacticRequires) -> do
1028+
koreDef <- (.definition) <$> lift getConfig
1029+
case knownPredicates of
1030+
[] ->
1031+
unless (null restRequires') $
1032+
-- no more @knownPredicates@, but unresolved conditions remain: abort
1033+
throwRemainingRequires currentSubst restRequires'
1034+
(c : cs) -> case matchTermsWithSubst Eval koreDef currentSubst (coerce headSyntacticRequires) (coerce c) of
1035+
MatchFailed{} -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires'
1036+
MatchIndeterminate{} -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires'
1037+
MatchSuccess newSubst ->
1038+
-- we got a substitution from matching @headSyntacticRequires@ against the clause @c@ of the path condition,
1039+
-- try applying it to @syntacticRequires <> restRequires'@, simplifying that with LLVM,
1040+
-- and filtering from the path condition
1041+
( do
1042+
withContext CtxSubstitution
1043+
$ logMessage
1044+
$ WithJsonMessage
1045+
(object ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList newSubst)])
1046+
$ renderOneLineText
1047+
$ "Substitution:"
1048+
<+> ( hsep $
1049+
intersperse "," $
1050+
map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $
1051+
Map.toList newSubst
1052+
)
1053+
1054+
let substitited = map (coerce . substituteInTerm newSubst . coerce) (syntacticRequires <> restRequires')
1055+
simplified <- coerce <$> mapM simplifyWithLLVM substitited
1056+
stillUnclear <- lift $ filterOutKnownConstraints (Set.fromList knownPredicates) simplified
1057+
case stillUnclear of
1058+
[] -> pure () -- done
1059+
_ -> do
1060+
logMessage $
1061+
renderOneLineText
1062+
( "Uncertain about conditions in syntactic simplification rule: "
1063+
<+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
1064+
)
1065+
-- @newSubst@ does not solve the conditions completely, repeat the process for @restSyntacticRequires@
1066+
-- using the learned @newSubst@
1067+
checkRequiresSyntactically restSyntacticRequires newSubst knownPredicates restRequires'
1068+
)
1069+
`catchE` ( \case
1070+
(_, IndeterminateCondition{}) -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires'
1071+
(_, ConditionFalse{}) -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires'
1072+
err -> throwE err
1073+
)
1074+
where
1075+
simplifyWithLLVM term = do
1076+
simplified <-
1077+
lift $
1078+
simplifyConstraint' False term
1079+
`catch_` ( \case
1080+
UndefinedTerm{} -> pure FalseBool
1081+
_ -> pure term
1082+
)
1083+
case simplified of
1084+
FalseBool -> do
1085+
throwE
1086+
( \ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text)
1087+
, ConditionFalse . coerce $ term
1088+
)
1089+
other -> pure other
1090+
1091+
throwRemainingRequires subst preds = do
1092+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
1093+
let substintuted = map (substituteInPredicate subst) preds
1094+
throwE
1095+
( \ctx ->
1096+
ctx . logMessage $
1097+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) preds]) $
1098+
renderOneLineText
1099+
( "Uncertain about conditions in syntactic simplification rule: "
1100+
<+> hsep (intersperse "," $ map (pretty' @mods) substintuted)
1101+
)
1102+
, IndeterminateCondition restRequires'
1103+
)
1104+
1105+
checkRequiresSemantically ::
1106+
forall io.
1107+
LoggerMIO io =>
1108+
Substitution ->
1109+
Set Predicate ->
1110+
[Predicate] ->
1111+
ExceptT
1112+
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
1113+
(EquationT io)
1114+
()
1115+
checkRequiresSemantically currentSubst knownPredicates restRequires' = do
1116+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
1117+
1118+
-- apply current substitution to restRequires
1119+
let restRequires = map (coerce . substituteInTerm currentSubst . coerce) restRequires'
1120+
toCheck <- lift $ filterOutKnownConstraints knownPredicates restRequires
1121+
unclearRequires <-
1122+
catMaybes
1123+
<$> mapM
1124+
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p)
1125+
)
1126+
toCheck
1127+
1128+
-- unclear conditions may have been simplified and
1129+
-- could now be syntactically present in the path constraints, filter again
1130+
stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearRequires
1131+
1132+
-- check unclear requires-clauses in the context of known constraints (prior)
1133+
solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig
1134+
1135+
-- check any conditions that are still unclear with the SMT solver
1136+
-- (or abort if no solver is being used), abort if still unclear after
1137+
unless (null stillUnclear) $
1138+
lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case
1139+
SMT.IsUnknown{} -> do
1140+
-- no solver or still unclear: abort
1141+
throwE
1142+
( \ctx ->
1143+
ctx . logMessage $
1144+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
1145+
renderOneLineText
1146+
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
1147+
)
1148+
, IndeterminateCondition stillUnclear
1149+
)
1150+
SMT.IsInvalid -> do
1151+
-- actually false given path condition: fail
1152+
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
1153+
throwE
1154+
( \ctx ->
1155+
ctx . logMessage $
1156+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
1157+
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
1158+
, ConditionFalse failedP
1159+
)
1160+
SMT.IsValid{} -> do
1161+
-- can proceed
1162+
pure ()
1163+
where
1164+
-- Simplify given predicate in a nested EquationT execution.
1165+
-- Call 'whenBottom' if it is Bottom, return Nothing if it is Top,
1166+
-- otherwise return the simplified remaining predicate.
1167+
checkConstraint whenBottom (Predicate p) = withContext CtxConstraint $ do
1168+
let fallBackToUnsimplifiedOrBottom :: EquationFailure -> EquationT io Term
1169+
fallBackToUnsimplifiedOrBottom = \case
1170+
UndefinedTerm{} -> pure FalseBool
1171+
_ -> pure p
1172+
-- exceptions need to be handled differently in the recursion,
1173+
-- falling back to the unsimplified constraint instead of aborting.
1174+
simplified <-
1175+
lift $ simplifyConstraint' True p `catch_` fallBackToUnsimplifiedOrBottom
1176+
case simplified of
1177+
FalseBool -> do
1178+
throwE . whenBottom $ coerce p
1179+
TrueBool -> pure Nothing
1180+
other -> pure . Just $ coerce other
1181+
10161182
--------------------------------------------------------------------
10171183

10181184
{- Simplification for boolean predicates

0 commit comments

Comments
 (0)