From bebd5c00c6e6bf5e8659d2fb000fc4c95bb4ae81 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 13 Aug 2024 12:28:03 +0200 Subject: [PATCH] Refactor requires check, use syntactic clauses --- .../library/Booster/Pattern/ApplyEquations.hs | 282 ++++++++++++++---- 1 file changed, 224 insertions(+), 58 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 0d5a28d16b6..9a4b555b729 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -840,57 +840,20 @@ applyEquation term rule = ) -- instantiate the requires clause with the obtained substitution - let required = + let rawRequired = concatMap - (splitBoolPredicates . coerce . substituteInTerm subst . coerce) + splitBoolPredicates rule.requires - -- If the required condition is _syntactically_ present in - -- the prior (known constraints), we don't check it. + -- required = map (coerce . substituteInTerm subst . coerce) rawRequired knownPredicates <- (.predicates) <$> lift getState - toCheck <- lift $ filterOutKnownConstraints knownPredicates required - -- check the filtered requires clause conditions - unclearConditions <- - catMaybes - <$> mapM - ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p) - ) - toCheck - - -- unclear conditions may have been simplified and - -- could now be syntactically present in the path constraints, filter again - stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions - - solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig + let (syntacticRequires, restRequires) = case rule.attributes.syntacticClauses of + SyntacticClauses [] -> ([], rawRequired) + SyntacticClauses _syntactic -> ([head rawRequired], tail rawRequired) -- TODO should use _syntactic to select - -- check any conditions that are still unclear with the SMT solver - -- (or abort if no solver is being used), abort if still unclear after - unless (null stillUnclear) $ - lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case - SMT.IsUnknown{} -> do - -- no solver or still unclear: abort - throwE - ( \ctx -> - ctx . logMessage $ - WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ - renderOneLineText - ( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear) - ) - , IndeterminateCondition stillUnclear - ) - SMT.IsInvalid -> do - -- actually false given path condition: fail - let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear - throwE - ( \ctx -> - ctx . logMessage $ - WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ - renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP) - , ConditionFalse failedP - ) - SMT.IsValid{} -> do - -- can proceed - pure () + -- check required conditions + withContext CtxConstraint $ + checkRequires subst (Set.toList knownPredicates) syntacticRequires restRequires -- check ensured conditions, filter any -- true ones, prune if any is false @@ -905,7 +868,9 @@ applyEquation term rule = ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p) ) ensured + -- check all ensured conditions together with the path condition + solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case SMT.IsInvalid -> do let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions @@ -927,18 +892,6 @@ applyEquation term rule = \s -> s{cache = s.cache{equations = mempty}} pure $ substituteInTerm subst rule.rhs where - filterOutKnownConstraints :: Set Predicate -> [Predicate] -> EquationT io [Predicate] - filterOutKnownConstraints priorKnowledge constraitns = do - let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns - unless (null knownTrue) $ - getPrettyModifiers >>= \case - ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> - logMessage $ - renderOneLineText $ - "Known true side conditions (won't check):" - <+> hsep (intersperse "," $ map (pretty' @mods) knownTrue) - pure toCheck - -- Simplify given predicate in a nested EquationT execution. -- Call 'whenBottom' if it is Bottom, return Nothing if it is Top, -- otherwise return the simplified remaining predicate. @@ -1013,6 +966,219 @@ applyEquation term rule = check $ Map.lookup Variable{variableSort = SortApp sortName [], variableName} subst +filterOutKnownConstraints :: + forall io. + LoggerMIO io => + Set Predicate -> + [Predicate] -> + EquationT io [Predicate] +filterOutKnownConstraints priorKnowledge constraitns = do + let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns + unless (null knownTrue) $ + getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> + logMessage $ + renderOneLineText $ + "Known true side conditions (won't check):" + <+> hsep (intersperse "," $ map (pretty' @mods) knownTrue) + pure toCheck + +checkRequires :: + forall io. + LoggerMIO io => + Substitution -> + [Predicate] -> + [Predicate] -> + [Predicate] -> + ExceptT + ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) + (EquationT io) + () +checkRequires currentSubst knownPredicates syntacticRequires restRequires' = do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + case syntacticRequires of + [] -> checkRequiresSemantically currentSubst (Set.fromList knownPredicates) restRequires' + _ -> + withContext CtxSyntactic $ + checkRequiresSyntactically + syntacticRequires + currentSubst + knownPredicates + restRequires' + +checkRequiresSyntactically :: + forall io. + LoggerMIO io => + [Predicate] -> + Substitution -> + [Predicate] -> + [Predicate] -> + ExceptT + ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) + (EquationT io) + () +checkRequiresSyntactically syntacticRequires currentSubst knownPredicates restRequires' = do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + case syntacticRequires of + [] -> + unless (null restRequires') $ + -- no more @syntacticRequires@, but unresolved conditions remain: abort + throwRemainingRequires currentSubst restRequires' + (headSyntacticRequires : restSyntacticRequires) -> do + koreDef <- (.definition) <$> lift getConfig + case knownPredicates of + [] -> + unless (null restRequires') $ + -- no more @knownPredicates@, but unresolved conditions remain: abort + throwRemainingRequires currentSubst restRequires' + (c : cs) -> case matchTermsWithSubst Eval koreDef currentSubst (coerce headSyntacticRequires) (coerce c) of + MatchFailed{} -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires' + MatchIndeterminate{} -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires' + MatchSuccess newSubst -> + -- we got a substitution from matching @headSyntacticRequires@ against the clause @c@ of the path condition, + -- try applying it to @syntacticRequires <> restRequires'@, simplifying that with LLVM, + -- and filtering from the path condition + ( do + withContext CtxSubstitution + $ logMessage + $ WithJsonMessage + (object ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList newSubst)]) + $ renderOneLineText + $ "Substitution:" + <+> ( hsep $ + intersperse "," $ + map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $ + Map.toList newSubst + ) + + let substitited = map (coerce . substituteInTerm newSubst . coerce) (syntacticRequires <> restRequires') + simplified <- coerce <$> mapM simplifyWithLLVM substitited + stillUnclear <- lift $ filterOutKnownConstraints (Set.fromList knownPredicates) simplified + case stillUnclear of + [] -> pure () -- done + _ -> do + logMessage $ + renderOneLineText + ( "Uncertain about conditions in syntactic simplification rule: " + <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear) + ) + -- @newSubst@ does not solve the conditions completely, repeat the process for @restSyntacticRequires@ + -- using the learned @newSubst@ + checkRequiresSyntactically restSyntacticRequires newSubst knownPredicates restRequires' + ) + `catchE` ( \case + (_, IndeterminateCondition{}) -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires' + (_, ConditionFalse{}) -> checkRequiresSyntactically syntacticRequires currentSubst cs restRequires' + err -> throwE err + ) + where + simplifyWithLLVM term = do + simplified <- + lift $ + simplifyConstraint' False term + `catch_` ( \case + UndefinedTerm{} -> pure FalseBool + _ -> pure term + ) + case simplified of + FalseBool -> do + throwE + ( \ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text) + , ConditionFalse . coerce $ term + ) + other -> pure other + + throwRemainingRequires subst preds = do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + let substintuted = map (substituteInPredicate subst) preds + throwE + ( \ctx -> + ctx . logMessage $ + WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) preds]) $ + renderOneLineText + ( "Uncertain about conditions in syntactic simplification rule: " + <+> hsep (intersperse "," $ map (pretty' @mods) substintuted) + ) + , IndeterminateCondition restRequires' + ) + +checkRequiresSemantically :: + forall io. + LoggerMIO io => + Substitution -> + Set Predicate -> + [Predicate] -> + ExceptT + ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) + (EquationT io) + () +checkRequiresSemantically currentSubst knownPredicates restRequires' = do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + + -- apply current substitution to restRequires + let restRequires = map (coerce . substituteInTerm currentSubst . coerce) restRequires' + toCheck <- lift $ filterOutKnownConstraints knownPredicates restRequires + unclearRequires <- + catMaybes + <$> mapM + ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p) + ) + toCheck + + -- unclear conditions may have been simplified and + -- could now be syntactically present in the path constraints, filter again + stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearRequires + + -- check unclear requires-clauses in the context of known constraints (prior) + solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig + + -- check any conditions that are still unclear with the SMT solver + -- (or abort if no solver is being used), abort if still unclear after + unless (null stillUnclear) $ + lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case + SMT.IsUnknown{} -> do + -- no solver or still unclear: abort + throwE + ( \ctx -> + ctx . logMessage $ + WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ + renderOneLineText + ( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear) + ) + , IndeterminateCondition stillUnclear + ) + SMT.IsInvalid -> do + -- actually false given path condition: fail + let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear + throwE + ( \ctx -> + ctx . logMessage $ + WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ + renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP) + , ConditionFalse failedP + ) + SMT.IsValid{} -> do + -- can proceed + pure () + where + -- Simplify given predicate in a nested EquationT execution. + -- Call 'whenBottom' if it is Bottom, return Nothing if it is Top, + -- otherwise return the simplified remaining predicate. + checkConstraint whenBottom (Predicate p) = withContext CtxConstraint $ do + let fallBackToUnsimplifiedOrBottom :: EquationFailure -> EquationT io Term + fallBackToUnsimplifiedOrBottom = \case + UndefinedTerm{} -> pure FalseBool + _ -> pure p + -- exceptions need to be handled differently in the recursion, + -- falling back to the unsimplified constraint instead of aborting. + simplified <- + lift $ simplifyConstraint' True p `catch_` fallBackToUnsimplifiedOrBottom + case simplified of + FalseBool -> do + throwE . whenBottom $ coerce p + TrueBool -> pure Nothing + other -> pure . Just $ coerce other + -------------------------------------------------------------------- {- Simplification for boolean predicates