Skip to content

Commit

Permalink
Remove ML connectives from the predicate type (#155)
Browse files Browse the repository at this point in the history
Turn `Predicate` into a newtype for `Terms` of sort `Bool`. This also
removes all the predicate simplifications, since those rules introduce
ML connectives. This should be a sound thing to do since the frontend
turns all `requires REQ` clauses into `REQ #Equals true`. All we should
do when internalising is to unwrap `REQ #Equals true` into `X`.

If we add a restriction to requires/ensures that they can only be
expressions of sort Bool
(runtimeverification/k#3284), this should be
sound. Equally, we dont want to use any rules such as

```
rule {K1 =/=Int K2 #Equals true} => #Not({K1 #Equals K2})
```
from `domains.md`:
https://github.com/runtimeverification/k/blob/71a183b85a48da94e34541ca138757fbeb37ce8a/k-distribution/include/kframework/builtin/domains.md?plain=1#L966-L974

since they would now introduce ML connectives which are unnecessary in
this instance. We want this rule to be applied instead

```
rule I1:Int =/=Int I2:Int => notBool (I1 ==Int I2)
```

other rules, such as

```
rule {true #Equals @b1 andBool @b2} => {true #Equals @b1} #And {true #Equals @b2}
```
are kind of meta-rules which we implicitly apply already:


https://github.com/runtimeverification/hs-backend-booster/blob/37717b4e33455e8e16e7ca51e946b9a7b4f3c1be/library/Booster/Pattern/Simplify.hs#L20-L25

There is still the question of ceil simplification rules but given that
they are most likely unsound in their current state and the booster is
very conservative around definedness, I don't think we need to worry
about them right now... the question is whether/how we will have to deal
with them in the future.

---------

Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Jost Berthold <jost.berthold@runtimeverification.com>
  • Loading branch information
4 people authored Nov 20, 2023
1 parent 7dc1965 commit 27ac540
Show file tree
Hide file tree
Showing 30 changed files with 467 additions and 762 deletions.
14 changes: 1 addition & 13 deletions library/Booster/Definition/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,6 @@ data KoreDefinition = KoreDefinition
, rewriteTheory :: Theory (RewriteRule "Rewrite")
, functionEquations :: Theory (RewriteRule "Function")
, simplifications :: Theory (RewriteRule "Simplification")
, predicateSimplifications :: Theory PredicateEquation
}
deriving stock (Eq, Show, GHC.Generic)
deriving anyclass (NFData)
Expand All @@ -65,7 +64,6 @@ emptyKoreDefinition attributes =
, rewriteTheory = Map.empty
, functionEquations = Map.empty
, simplifications = Map.empty
, predicateSimplifications = Map.empty
}

data RewriteRule (tag :: k) = RewriteRule
Expand All @@ -84,17 +82,7 @@ data Alias = Alias
{ name :: AliasName
, params :: [Sort]
, args :: [Variable]
, rhs :: TermOrPredicate
}
deriving stock (Eq, Ord, Show, GHC.Generic)
deriving anyclass (NFData)

data PredicateEquation = PredicateEquation
{ target :: Predicate
, conditions :: [Predicate]
, rhs :: [Predicate]
, attributes :: AxiomAttributes
, computedAttributes :: ComputedAxiomAttributes
, rhs :: Pattern
}
deriving stock (Eq, Ord, Show, GHC.Generic)
deriving anyclass (NFData)
8 changes: 0 additions & 8 deletions library/Booster/Definition/Util.hs
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,6 @@ data Summary = Summary
, rewriteRules :: Map.Map TermIndex [SourceRef]
, functionRules :: Map.Map TermIndex [SourceRef]
, simplifications :: Map.Map TermIndex [SourceRef]
, predicateSimplifications :: Map.Map TermIndex [SourceRef]
}
deriving stock (Eq, Show, Generic)
deriving anyclass (NFData)
Expand Down Expand Up @@ -80,7 +79,6 @@ mkSummary file def =
, rewriteRules = Map.map sourceRefs def.rewriteTheory
, functionRules = Map.map sourceRefs def.functionEquations
, simplifications = Map.map sourceRefs def.simplifications
, predicateSimplifications = Map.map sourceRefs def.predicateSimplifications
}
where
sourceRefs :: HasSourceRef x => Map.Map k [x] -> [SourceRef]
Expand Down Expand Up @@ -111,9 +109,6 @@ instance Pretty Summary where
<> ( "Simplifications by term index:"
: tableView prettyTermIndex pretty summary.simplifications
)
<> ( "Predicate simplifications by term index:"
: tableView prettyTermIndex pretty summary.predicateSimplifications
)
<> [mempty]
where
tableView :: (k -> Doc a) -> (elem -> Doc a) -> Map.Map k [elem] -> [Doc a]
Expand Down Expand Up @@ -164,6 +159,3 @@ instance HasSourceRef AxiomAttributes where

instance HasSourceRef (RewriteRule a) where
sourceRef r = sourceRef r.attributes

instance HasSourceRef PredicateEquation where
sourceRef r = sourceRef r.attributes
57 changes: 34 additions & 23 deletions library/Booster/JsonRpc.hs
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,14 @@ import Booster.Definition.Base (KoreDefinition (..))
import Booster.Definition.Base qualified as Definition (RewriteRule (..))
import Booster.LLVM.Internal qualified as LLVM
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
import Booster.Pattern.Base (Pattern (..), TermOrPredicate (..))
import Booster.Pattern.Base (
InternalisedPredicate (..),
Pattern (..),
Term,
TermOrPredicate (..),
Variable,
)
import Booster.Pattern.Base qualified as Pattern
import Booster.Pattern.Rewrite (
RewriteFailed (..),
RewriteResult (..),
Expand Down Expand Up @@ -88,7 +95,7 @@ respond stateVar =
Left patternError -> do
Log.logDebug $ "Error internalising cterm" <> Text.pack (show patternError)
pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternError
Right pat -> do
Right (pat, substitution) -> do
let cutPoints = fromMaybe [] req.cutPointRules
terminals = fromMaybe [] req.terminalRules
mbDepth = fmap RpcTypes.getNat req.maxDepth
Expand All @@ -109,7 +116,7 @@ respond stateVar =
Just $
fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
else Nothing
pure $ execResponse duration req result
pure $ execResponse duration req result substitution
RpcTypes.AddModule req -> do
-- block other request executions while modifying the server state
state <- liftIO $ takeMVar stateVar
Expand Down Expand Up @@ -172,11 +179,11 @@ respond stateVar =
Log.logError $ "Error internalising cterm: " <> Text.pack (show patternErrors)
pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrors
-- term and predicate (pattern)
Right (TermAndPredicate pat) -> do
Right (TermAndPredicateAndSubstitution pat substitution) -> do
Log.logInfoNS "booster" "Simplifying a pattern"
ApplyEquations.evaluatePattern doTracing def mLlvmLibrary mempty pat >>= \case
(Right newPattern, patternTraces, _) -> do
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
tSort = externaliseSort (sortOfPattern newPattern)
result = case catMaybes [mbPredicate, mbSubstitution] of
[] -> term
Expand All @@ -190,7 +197,7 @@ respond stateVar =
(Left other, _traces, _) ->
pure . Left . RpcError.backendError RpcError.Aborted $ show other -- FIXME
-- predicate only
Right (APredicate predicate) -> do
Right (BoolOrCeilOrSubstitutionPredicate (IsPredicate predicate)) -> do
Log.logInfoNS "booster" "Simplifying a predicate"
ApplyEquations.simplifyConstraint doTracing def mLlvmLibrary mempty predicate >>= \case
(Right newPred, traces, _) -> do
Expand All @@ -201,6 +208,9 @@ respond stateVar =
pure $ Right (addHeader result, traces)
(Left something, _traces, _) ->
pure . Left . RpcError.backendError RpcError.Aborted $ show something -- FIXME
Right (BoolOrCeilOrSubstitutionPredicate _) ->
pure . Left . RpcError.backendError RpcError.Aborted $
("cannot simplify ceil/substitution at the moment" :: String) -- FIXME
stop <- liftIO $ getTime Monotonic

let duration =
Expand Down Expand Up @@ -275,17 +285,18 @@ execResponse ::
Maybe Double ->
RpcTypes.ExecuteRequest ->
(Natural, Seq (RewriteTrace Pattern), RewriteResult Pattern) ->
Map Variable Term ->
Either ErrorObj (RpcTypes.API 'RpcTypes.Res)
execResponse mbDuration req (d, traces, rr) = case rr of
execResponse mbDuration req (d, traces, rr) originalSubstitution = case rr of
RewriteBranch p nexts ->
Right $
RpcTypes.Execute
RpcTypes.ExecuteResult
{ reason = RpcTypes.Branching
, depth
, logs
, state = toExecState p
, nextStates = Just $ map (\(_, _, p') -> toExecState p') $ toList nexts
, state = toExecState p originalSubstitution
, nextStates = Just $ map (\(_, _, p') -> toExecState p' originalSubstitution) $ toList nexts
, rule = Nothing
}
RewriteStuck p ->
Expand All @@ -295,7 +306,7 @@ execResponse mbDuration req (d, traces, rr) = case rr of
{ reason = RpcTypes.Stuck
, depth
, logs
, state = toExecState p
, state = toExecState p originalSubstitution
, nextStates = Nothing
, rule = Nothing
}
Expand All @@ -306,7 +317,7 @@ execResponse mbDuration req (d, traces, rr) = case rr of
{ reason = RpcTypes.Vacuous
, depth
, logs
, state = toExecState p
, state = toExecState p originalSubstitution
, nextStates = Nothing
, rule = Nothing
}
Expand All @@ -317,8 +328,8 @@ execResponse mbDuration req (d, traces, rr) = case rr of
{ reason = RpcTypes.CutPointRule
, depth
, logs
, state = toExecState p
, nextStates = Just [toExecState next]
, state = toExecState p originalSubstitution
, nextStates = Just [toExecState next originalSubstitution]
, rule = Just lbl
}
RewriteTerminal lbl _ p ->
Expand All @@ -328,7 +339,7 @@ execResponse mbDuration req (d, traces, rr) = case rr of
{ reason = RpcTypes.TerminalRule
, depth
, logs
, state = toExecState p
, state = toExecState p originalSubstitution
, nextStates = Nothing
, rule = Just lbl
}
Expand All @@ -339,7 +350,7 @@ execResponse mbDuration req (d, traces, rr) = case rr of
{ reason = RpcTypes.DepthBound
, depth
, logs
, state = toExecState p
, state = toExecState p originalSubstitution
, nextStates = Nothing
, rule = Nothing
}
Expand All @@ -356,7 +367,7 @@ execResponse mbDuration req (d, traces, rr) = case rr of
(logSuccessfulSimplifications, logFailedSimplifications)
(RewriteStepFailed failure)
in logs <|> abortRewriteLog
, state = toExecState p
, state = toExecState p originalSubstitution
, nextStates = Nothing
, rule = Nothing
}
Expand Down Expand Up @@ -385,15 +396,15 @@ execResponse mbDuration req (d, traces, rr) = case rr of
(Just t, Nothing) -> Just [t]
(Just t, Just xs) -> Just (t : xs)

toExecState :: Pattern -> RpcTypes.ExecuteState
toExecState pat =
toExecState :: Pattern -> Map Variable Term -> RpcTypes.ExecuteState
toExecState pat sub =
RpcTypes.ExecuteState
{ term = addHeader t
, predicate = fmap addHeader p
, substitution = fmap addHeader s
}
where
(t, p, s) = externalisePattern pat
(t, p, s) = externalisePattern pat sub

mkLogEquationTrace :: (Bool, Bool) -> ApplyEquations.EquationTrace -> Maybe LogEntry
mkLogEquationTrace
Expand All @@ -409,7 +420,7 @@ mkLogEquationTrace
, origin
, result =
Success
{ rewrittenTerm = Just $ execStateToKoreJson $ toExecState $ Pattern rewrittenTrm mempty
{ rewrittenTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ rewrittenTrm) mempty
, substitution = Nothing
, ruleId = fromMaybe "UNKNOWN" _ruleId
}
Expand Down Expand Up @@ -474,7 +485,7 @@ mkLogEquationTrace
}
_ -> Nothing
where
originalTerm = Just $ execStateToKoreJson $ toExecState $ Pattern subjectTerm mempty
originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ subjectTerm) mempty
originalTermIndex = Nothing
origin = Booster
_ruleId = fmap getUniqueId uid
Expand All @@ -495,7 +506,7 @@ mkLogRewriteTrace
Rewrite
{ result =
Success
{ rewrittenTerm = Just $ execStateToKoreJson $ toExecState res
{ rewrittenTerm = Just $ execStateToKoreJson $ toExecState res mempty
, substitution = Nothing
, ruleId = maybe "UNKNOWN" getUniqueId uid
}
Expand Down Expand Up @@ -547,7 +558,7 @@ mkLogRewriteTrace
let final = singleton $ case failure of
ApplyEquations.IndexIsNone trm ->
Simplification
{ originalTerm = Just $ execStateToKoreJson $ toExecState $ Pattern trm mempty
{ originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ trm) mempty
, originalTermIndex = Nothing
, origin = Booster
, result = Failure{reason = "No index found for term", _ruleId = Nothing}
Expand Down
25 changes: 8 additions & 17 deletions library/Booster/JsonRpc/Utils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,7 @@ import Data.Aeson as Json
import Data.Aeson.Encode.Pretty (encodePretty')
import Data.Aeson.Types (parseMaybe)
import Data.ByteString.Lazy.Char8 qualified as BS
import Data.Functor.Foldable (Corecursive (embed), cata)
import Data.Maybe (fromMaybe)
import Data.Set qualified as Set
import Network.JSONRPC
import Prettyprinter
import System.Exit (ExitCode (..))
Expand All @@ -36,6 +34,7 @@ import Booster.Definition.Base qualified as Internal
import Booster.Pattern.Base qualified as Internal
import Booster.Prettyprinter
import Booster.Syntax.Json.Internalise
import Data.Map qualified as Map
import Kore.JsonRpc.Types
import Kore.Syntax.Json.Types hiding (Left, Right)

Expand Down Expand Up @@ -235,23 +234,15 @@ diffBy def pat1 pat2 =
renderDiff (internalise pat1) (internalise pat2)
where
renderBS :: Internal.TermOrPredicate -> BS.ByteString
renderBS (Internal.APredicate p) = BS.pack . renderDefault $ pretty p
renderBS (Internal.TermAndPredicate p) = BS.pack . renderDefault $ pretty p
renderBS (Internal.BoolOrCeilOrSubstitutionPredicate (Internal.IsPredicate p)) = BS.pack . renderDefault $ pretty p
renderBS (Internal.BoolOrCeilOrSubstitutionPredicate (Internal.IsCeil c)) = BS.pack . renderDefault $ pretty c
renderBS (Internal.BoolOrCeilOrSubstitutionPredicate (Internal.IsSubstitution k v)) = BS.pack . renderDefault $ pretty k <+> "=" <+> pretty v
renderBS (Internal.TermAndPredicateAndSubstitution p m) =
BS.pack . renderDefault $
pretty p <+> vsep (map (\(k, v) -> pretty k <+> "=" <+> pretty v) (Map.toList m))
internalise =
either
(("Pattern could not be internalised: " <>) . Json.encode)
(renderBS . orientEquals)
renderBS
. runExcept
. internaliseTermOrPredicate DisallowAlias IgnoreSubsorts Nothing def

orientEquals = \case
Internal.APredicate p ->
Internal.APredicate $ orient p
Internal.TermAndPredicate p ->
Internal.TermAndPredicate p{Internal.constraints = Set.map orient p.constraints}
where
orient :: Internal.Predicate -> Internal.Predicate
orient = cata $ \case
Internal.EqualsTermF t1 t2
| t1 > t2 -> Internal.EqualsTerm t2 t1
other -> embed other
Loading

0 comments on commit 27ac540

Please sign in to comment.