Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into release
Browse files Browse the repository at this point in the history
  • Loading branch information
devops committed Jul 30, 2024
2 parents 0f13799 + be64ead commit aa5984e
Show file tree
Hide file tree
Showing 7 changed files with 701 additions and 11 deletions.
9 changes: 8 additions & 1 deletion booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ import Booster.Pattern.Rewrite (
performRewrite,
)
import Booster.Pattern.Util (
freeVariables,
sortOfPattern,
substituteInPredicate,
substituteInTerm,
Expand Down Expand Up @@ -143,10 +144,16 @@ respond stateVar request =
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
, ceilConditions = pat.ceilConditions
}
-- remember all variables used in the substitutions
substVars =
Set.unions
[ Set.singleton v <> freeVariables e
| (v, e) <- Map.assocs substitution
]

solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
result <-
performRewrite doTracing def mLlvmLibrary solver mbDepth cutPoints terminals substPat
performRewrite doTracing def mLlvmLibrary solver substVars mbDepth cutPoints terminals substPat
SMT.finaliseSolver solver
stop <- liftIO $ getTime Monotonic
let duration =
Expand Down
18 changes: 13 additions & 5 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,7 @@ data RewriteConfig = RewriteConfig
{ definition :: KoreDefinition
, llvmApi :: Maybe LLVM.API
, smtSolver :: SMT.SMTContext
, varsToAvoid :: Set.Set Variable
, doTracing :: Flag "CollectRewriteTraces"
, logger :: Logger LogMessage
, prettyModifiers :: ModifiersRep
Expand All @@ -103,15 +104,18 @@ runRewriteT ::
KoreDefinition ->
Maybe LLVM.API ->
SMT.SMTContext ->
Set.Set Variable ->
SimplifierCache ->
RewriteT io a ->
io (Either (RewriteFailed "Rewrite") (a, SimplifierCache))
runRewriteT doTracing definition llvmApi smtSolver cache m = do
runRewriteT doTracing definition llvmApi smtSolver varsToAvoid cache m = do
logger <- getLogger
prettyModifiers <- getPrettyModifiers
runExceptT
. flip runStateT cache
. flip runReaderT RewriteConfig{definition, llvmApi, smtSolver, doTracing, logger, prettyModifiers}
. flip
runReaderT
RewriteConfig{definition, llvmApi, smtSolver, varsToAvoid, doTracing, logger, prettyModifiers}
. unRewriteT
$ m

Expand Down Expand Up @@ -408,9 +412,10 @@ applyRule pat@Pattern{ceilConditions} rule =
-- existential variables may be present in rule.rhs and rule.ensures,
-- need to strip prefixes and freshen their names with respect to variables already
-- present in the input pattern and in the unification substitution
let varsFromInput = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
varsFromSubst = Set.unions . map freeVariables . Map.elems $ subst
forbiddenVars = varsFromInput <> varsFromSubst
forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst
existentialSubst =
Map.fromSet
(\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
Expand Down Expand Up @@ -703,6 +708,8 @@ performRewrite ::
KoreDefinition ->
Maybe LLVM.API ->
SMT.SMTContext ->
-- | Variable names to avoid (for new existentials)
Set.Set Variable ->
-- | maximum depth
Maybe Natural ->
-- | cut point rule labels
Expand All @@ -711,7 +718,7 @@ performRewrite ::
[Text] ->
Pattern ->
io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern)
performRewrite doTracing def mLlvmLibrary smtSolver mbMaxDepth cutLabels terminalLabels pat = do
performRewrite doTracing def mLlvmLibrary smtSolver varsToAvoid mbMaxDepth cutLabels terminalLabels pat = do
(rr, RewriteStepsState{counter, traces}) <-
flip runStateT rewriteStart $ doSteps False pat
pure (counter, traces, rr)
Expand Down Expand Up @@ -804,6 +811,7 @@ performRewrite doTracing def mLlvmLibrary smtSolver mbMaxDepth cutLabels termina
def
mLlvmLibrary
smtSolver
varsToAvoid
simplifierCache
(withPatternContext pat' $ rewriteStep cutLabels terminalLabels pat')
>>= \case
Expand Down
28 changes: 28 additions & 0 deletions booster/test/rpc-integration/test-questionmark-vars/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,3 +92,31 @@ transition rules that unconditionally introduce a fresh variable in the configur
<a-state> ?X2 </a-state>
<b-state> ?X1 </b-state>
```

5) _ques-and-substitution_

If a substitution `X ==K b` is supplied, it will be applied before rewriting.
However, the variable `X` can still not be used because the substitution will also be returned in the result (for information).
Therefore, the newly created variable cannot be `X0`.

_Input:_

```
<k> #setAStateSymbolic </k>
<a-state> ?X0 </a-state>
<b-state> ?X </b-state>
#And
?X #Equals b #And ?X0 #Equals ?X1 #And ?X2 #Equals ?X3 // substitutions
```

_Expected:_

```
<k> .K </k>
<a-state> ?X0 </a-state>
<b-state> b </b-state>
#And
?X #Equals b #And ?X0 #Equals ?X1 #And ?X2 #Equals ?X3 // substitutions
#And
condition(?X4)
```
225 changes: 225 additions & 0 deletions ...er/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,225 @@
{
"jsonrpc": "2.0",
"id": 1,
"result": {
"reason": "stuck",
"depth": 1,
"state": {
"term": {
"format": "KORE",
"version": 1,
"term": {
"tag": "App",
"name": "Lbl'-LT-'generatedTop'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'-LT-'k'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'a-state'-GT-'",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "Var'Ques'X4",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
}
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'b-state'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State",
"sorts": [],
"args": []
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'generatedCounter'-GT-'",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
]
}
},
"substitution": {
"format": "KORE",
"version": 1,
"term": {
"tag": "And",
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"patterns": [
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortState",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "EVar",
"name": "Var'Ques'X",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
}
},
"second": {
"tag": "App",
"name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State",
"sorts": [],
"args": []
}
},
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortState",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "EVar",
"name": "Var'Ques'X0",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
}
},
"second": {
"tag": "EVar",
"name": "Var'Ques'X1",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
}
}
},
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortState",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "EVar",
"name": "Var'Ques'X2",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
}
},
"second": {
"tag": "EVar",
"name": "Var'Ques'X3",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
}
}
}
]
}
},
"predicate": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "true"
},
"second": {
"tag": "App",
"name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "Var'Ques'X4",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
}
}
]
}
}
}
}
}
}
Loading

0 comments on commit aa5984e

Please sign in to comment.