Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Recording missing constraint about MCE wildcards in FunctionRecorder #825

Merged
merged 1 commit into from
Mar 26, 2024
Merged

Recording missing constraint about MCE wildcards in FunctionRecorder #825

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions src/main/scala/rules/MoreCompleteExhaleSupporter.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -369,12 +369,15 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
ch.withPerm(PermMinus(ch.perm, permTaken))
})

v.decider.assume(
val totalTakenBounds =
Implies(
totalPermSum !== NoPerm,
And(
PermLess(NoPerm, totalPermTaken),
PermLess(totalPermTaken, totalPermSum))))
PermLess(totalPermTaken, totalPermSum)))
v.decider.assume(totalTakenBounds)

newFr = newFr.recordConstraint(totalTakenBounds)

val s1 = s.copy(functionRecorder = newFr)

Expand Down
5 changes: 4 additions & 1 deletion src/main/scala/supporters/functions/FunctionData.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,7 @@ class FunctionData(val programFunction: ast.Function,
private[this] var freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
private[this] var freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
private[this] var freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
private[this] var freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
private[this] var freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
private[this] var freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
private[this] var freshMacros: InsertionOrderedSet[MacroDecl] = InsertionOrderedSet.empty
Expand All @@ -117,6 +118,7 @@ class FunctionData(val programFunction: ast.Function,
freshFvfsAndDomains = mergedFunctionRecorder.freshFvfsAndDomains
freshFieldInvs = mergedFunctionRecorder.freshFieldInvs
freshArps = mergedFunctionRecorder.freshArps
freshConstraints = mergedFunctionRecorder.freshConstraints
freshSnapshots = mergedFunctionRecorder.freshSnapshots
freshPathSymbols = mergedFunctionRecorder.freshPathSymbols
freshMacros = mergedFunctionRecorder.freshMacros
Expand All @@ -143,7 +145,8 @@ class FunctionData(val programFunction: ast.Function,
val nested = (
freshFieldInvs.flatMap(_.definitionalAxioms)
++ freshFvfsAndDomains.flatMap (fvfDef => fvfDef.domainDefinitions ++ fvfDef.valueDefinitions)
++ freshArps.map(_._2))
++ freshArps.map(_._2)
++ freshConstraints)

// Filter out nested definitions that contain free variables.
// This should not happen, but currently can, due to bugs in the function axiomatisation code.
Expand Down
11 changes: 11 additions & 0 deletions src/main/scala/supporters/functions/FunctionRecorder.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
def freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition]
def freshFieldInvs: InsertionOrderedSet[InverseFunctions]
def freshArps: InsertionOrderedSet[(Var, Term)]
def freshConstraints: InsertionOrderedSet[Term]
def freshSnapshots: InsertionOrderedSet[Function]
def freshPathSymbols: InsertionOrderedSet[Function]
def freshMacros: InsertionOrderedSet[MacroDecl]
Expand All @@ -34,6 +35,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
def recordFvfAndDomain(fvfDef: SnapshotMapDefinition): FunctionRecorder
def recordFieldInv(inv: InverseFunctions): FunctionRecorder
def recordArp(arp: Var, constraint: Term): FunctionRecorder
def recordConstraint(constraint: Term): FunctionRecorder
def recordFreshSnapshot(snap: Function): FunctionRecorder
def recordPathSymbol(symbol: Function): FunctionRecorder
def recordFreshMacro(decl: MacroDecl): FunctionRecorder
Expand All @@ -47,6 +49,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet(),
freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet(),
freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(),
freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet(),
freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet(),
freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet(),
freshMacros: InsertionOrderedSet[MacroDecl] = InsertionOrderedSet(),
Expand Down Expand Up @@ -190,6 +193,10 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
if (depth <= 2) copy(freshArps = freshArps + ((arp, constraint)))
else this

def recordConstraint(constraint: Term): ActualFunctionRecorder =
if (depth <= 2) copy(freshConstraints = freshConstraints + constraint)
else this

def recordFreshSnapshot(snap: Function): ActualFunctionRecorder =
if (depth <= 1) copy(freshSnapshots = freshSnapshots + snap)
else this
Expand Down Expand Up @@ -231,6 +238,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
val fvfs = freshFvfsAndDomains ++ other.freshFvfsAndDomains
val fieldInvs = freshFieldInvs ++ other.freshFieldInvs
val arps = freshArps ++ other.freshArps
val constraints = freshConstraints ++ other.freshConstraints
val snaps = freshSnapshots ++ other.freshSnapshots
val symbols = freshPathSymbols ++ other.freshPathSymbols
val macros = freshMacros ++ other.freshMacros
Expand All @@ -240,6 +248,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
freshFvfsAndDomains = fvfs,
freshFieldInvs = fieldInvs,
freshArps = arps,
freshConstraints = constraints,
freshSnapshots = snaps,
freshPathSymbols = symbols,
freshMacros = macros)
Expand Down Expand Up @@ -269,6 +278,7 @@ case object NoopFunctionRecorder extends FunctionRecorder {
val freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
val freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
val freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
val freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
val freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
val freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
val freshMacros: InsertionOrderedSet[MacroDecl] = InsertionOrderedSet.empty
Expand All @@ -285,6 +295,7 @@ case object NoopFunctionRecorder extends FunctionRecorder {
def recordFieldInv(inv: InverseFunctions): NoopFunctionRecorder.type = this
def recordSnapshot(fapp: ast.FuncApp, guards: Stack[Term], snap: Term): NoopFunctionRecorder.type = this
def recordArp(arp: Var, constraint: Term): NoopFunctionRecorder.type = this
def recordConstraint(constraint: Term): NoopFunctionRecorder.type = this
def recordFreshSnapshot(snap: Function): NoopFunctionRecorder.type = this
def recordPathSymbol(symbol: Function): NoopFunctionRecorder.type = this
def recordFreshMacro(decl: MacroDecl): NoopFunctionRecorder.type = this
Expand Down
Loading