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.

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

Theory of heaps translation (again) #13

Merged
merged 55 commits into from
Jun 19, 2024
Merged
Changes from 1 commit
Commits
Show all changes
55 commits
Select commit Hold shift + click to select a range
0577ace
Add TheoryOfHeapProcessor and ContractConditionTools
OskarSoderberg May 3, 2023
62b6458
Add EqualityReader and IExpressionProcessor trait
OskarSoderberg May 4, 2023
aec33c9
Add PostconditionSimplifier
OskarSoderberg May 4, 2023
69e9a3e
Add ACSLExpressionProcessor and improve match readability
OskarSoderberg May 7, 2023
d860aba
Add EqualitySwapper
OskarSoderberg May 8, 2023
8d117c6
Add ClauseRemover
OskarSoderberg May 8, 2023
27a6df5
Add ACSLExpressions to ACSLLineariser
OskarSoderberg May 9, 2023
d17525b
Add ADTSimplifier and fix getter extraction in TOHProcessor
OskarSoderberg May 10, 2023
76bb29e
Add struct dereference translation
OskarSoderberg May 15, 2023
aa24644
Fix uniform expression processing
OskarSoderberg May 16, 2023
394b6ab
Replace IExpressionProcessor by ContractProcessor
OskarSoderberg May 16, 2023
aa636fc
Refactor ACSLExpressionProcessor
OskarSoderberg May 16, 2023
3663942
Refactor ADTSimplifier
OskarSoderberg May 16, 2023
7745649
Refactor classes with ContractProcessor
OskarSoderberg May 16, 2023
c3a95e6
Refactor TheoryOfHeapFunApp
OskarSoderberg May 16, 2023
ae50c3f
Move out AssignmentProcessor and fix TheoryOfHeapFunApp
OskarSoderberg May 16, 2023
0794c78
Replace Equalities by ValSet
OskarSoderberg May 16, 2023
17047cc
Refactor EqualitySwapper
OskarSoderberg May 17, 2023
01a89b7
Add HeapPropProcessor and remove PostconditionSimplifier from processors
OskarSoderberg May 17, 2023
c919d9d
Add separated and first write filtering to AssignmentProcessor
OskarSoderberg May 17, 2023
d0f2066
Add getClauses for Assignment- and PointerPropProcessor
OskarSoderberg May 18, 2023
83cc797
Add properties to ContractInfo
OskarSoderberg May 18, 2023
32cf7fe
Add PostconditionSimplifier again
OskarSoderberg May 18, 2023
82dd990
Add ExplicitPointerRemover and TrivialEqualityRemover
OskarSoderberg May 18, 2023
26ae945
Add general removal of explicit pointers
OskarSoderberg May 21, 2023
aeab155
Fix bug where an empty separatedSet would result in no assignments
OskarSoderberg May 21, 2023
e791d0f
Add false check for PostconditionSimplifier
OskarSoderberg May 23, 2023
99cc2d6
Fix bug where equalities within OR clauses were read
OskarSoderberg May 23, 2023
0d6972c
Fix bug where ExplPointerRemover missed pointers
OskarSoderberg May 23, 2023
0963b3e
Fix bug where quantifierDepth wasn't passed
OskarSoderberg May 23, 2023
5fe19fb
Fix bug where ExplicitPointerRemover missed last formula
OskarSoderberg May 24, 2023
a5ce42e
Add HeapEqualityRemover
OskarSoderberg May 24, 2023
b7c21dd
Remove is_O_<sort> to valid translation
OskarSoderberg May 24, 2023
2f09eae
Refactor getStructMap to val
OskarSoderberg May 24, 2023
9a101d2
Rename isCurrentHeap
OskarSoderberg May 24, 2023
548324d
Fix formula shift in EqualitySwapper and fix prints
OskarSoderberg May 30, 2023
267965f
Clean up main function
OskarSoderberg Oct 1, 2023
ca08a61
(WIP) Do not apply heap processor when there is no heap.
zafer-esen Oct 9, 2023
f457942
Fix heap processors running when no heap available
OskarSoderberg Oct 14, 2023
2aacdf7
Add preambles and high-level descriptions
OskarSoderberg Oct 14, 2023
f1917e7
Add -debug option for printing debug messages and clean up some debug…
zafer-esen Oct 18, 2023
19042b1
Update years in preambles and list of contributors
zafer-esen Oct 18, 2023
13f0ced
Fix build issues after rebase to master
May 24, 2024
30d17a0
Remove extraneous 'UNSAFE' printout
May 29, 2024
b9a3251
Draft regression tests for ACSL theory of heap translation
May 29, 2024
a78d299
Second draft regression tests for ACSL theory of heap translation
May 30, 2024
bbfbf9b
Add regression-tests/toh-contract-translation/runtests
May 30, 2024
3869799
Add regression tests to 'runalldirs'
May 31, 2024
be699b7
Removed unused files
May 31, 2024
971f955
Add regression-tests/toh-contract-translation/Answers
May 31, 2024
b081923
Correct projec/build.properties
May 31, 2024
a529938
Remove failing regression test from toh-contract-translation suite
Jun 12, 2024
481819f
Add changes from theory-of-heaps-translation-thesis-version
Jun 10, 2024
c6db602
Merge branch 'ola-theory-of-heaps-translation' of https://github.com/…
Jun 17, 2024
ed405fe
Use empty heap instead of quantified heap variable
Jun 19, 2024
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
Prev Previous commit
Next Next commit
Add general removal of explicit pointers
  • Loading branch information
OskarSoderberg authored and Ola Wingbrant (sssowo) committed May 24, 2024
commit 26ae945ba01ec3f85100b27dc99f669036164834
3 changes: 3 additions & 0 deletions src/tricera/postprocessor/ACSLFunctions.scala
Original file line number Diff line number Diff line change
@@ -17,6 +17,9 @@ object ACSLExpression {
val oldArrow = new IFunction("oldArrow", 2, false, false) // \old(p)->a
val separated = new Predicate("\\separated", 2) // \separated(p1, p2)

val functions = Set(deref, oldDeref, derefOldPointer, arrow, arrowOldPointer, oldArrow)
val predicates = Set(valid, separated)

// Here a ConstantTerm is introduced as a container for the variable name
def derefFunApp(
derefFunction: IFunction,
81 changes: 45 additions & 36 deletions src/tricera/postprocessor/ClauseRemover.scala
Original file line number Diff line number Diff line change
@@ -115,47 +115,56 @@ class ExplicitPointerRemoverVisitor(cci: ContractConditionInfo)
quantifierDepth: Int,
subres: Seq[IExpression]
): IExpression = t match {
case IBinFormula(
IBinJunctor.And,
IEquation(v1: ISortedVariable, v2: ISortedVariable),
f
)
if cci.isPointer(v1, quantifierDepth) && cci.isPointer(
v2,
quantifierDepth
) =>
t update subres
case IBinFormula(
IBinJunctor.And,
f,
IEquation(v1: ISortedVariable, v2: ISortedVariable)
)
if cci.isPointer(v1, quantifierDepth) && cci.isPointer(
v2,
quantifierDepth
) =>
t update subres
case IBinFormula(IBinJunctor.And, IEquation(v: ISortedVariable, _), f)
if cci.isPointer(v, quantifierDepth) =>
f
case IBinFormula(IBinJunctor.And, IEquation(_, v: ISortedVariable), f)
if cci.isPointer(v, quantifierDepth) =>
f
case IBinFormula(IBinJunctor.And, f, IEquation(v: ISortedVariable, _))
if cci.isPointer(v, quantifierDepth) =>
f
case IBinFormula(IBinJunctor.And, f, IEquation(_, v: ISortedVariable))
if cci.isPointer(v, quantifierDepth) =>
f
case IIntFormula(_, v: ISortedVariable)
if cci.isPointer(v, quantifierDepth) =>
IBoolLit(true)
// need to be able to get type of any term to be exhaustive
case IBinFormula(IBinJunctor.And, f1, f2)
if ContainsExplicitPointerVisitor(f1, cci) =>
f2
case IBinFormula(IBinJunctor.And, f1, f2)
if ContainsExplicitPointerVisitor(f2, cci) =>
f1
case _ =>
t update subres
}
}

object ContainsExplicitPointerVisitor {
def apply(expr: IExpression, cci: ContractConditionInfo): Boolean = {
(new ContainsExplicitPointerVisitor(cci))(expr)
}
}

class ContainsExplicitPointerVisitor(cci: ContractConditionInfo) extends CollectingVisitor[Int, Boolean] {
def apply(expr: IExpression): Boolean = {
visit(expr, 0)
}

override def preVisit(t: IExpression, quantifierDepth: Int): PreVisitResult = {
t match {
case vb: IVariableBinder =>
UniSubArgs(quantifierDepth + 1)

case IEquation(v1: ISortedVariable, v2: ISortedVariable) if cci.isPointer(v1, quantifierDepth) && cci.isPointer(v2, quantifierDepth) =>
ShortCutResult(false)
case TheoryOfHeapFunApp(_,_) =>
ShortCutResult(false)
case IFunApp(fun, _) if cci.isACSLFunction(fun) =>
ShortCutResult(false)
case IAtom(pred, _) if cci.isACSLPredicate(pred) =>
ShortCutResult(false)
case IBinFormula(IBinJunctor.And, _, _) =>
ShortCutResult(false)
case _ =>
KeepArg
}
}

override def postVisit(t: IExpression, quantifierDepth: Int, subres: Seq[Boolean]): Boolean = t match {
case v: ISortedVariable if cci.isPointer(v, quantifierDepth) =>
true
case _ =>
if (subres.isEmpty) false else subres.reduce(_ || _)
}
}

object TrivialEqualityRemover {
def apply(expr: IExpression, cci: ContractConditionInfo): IExpression = {
(new TrivialEqualityRemover(cci)).visit(expr, ())
13 changes: 8 additions & 5 deletions src/tricera/postprocessor/ContractProcessorUtils.scala
Original file line number Diff line number Diff line change
@@ -107,6 +107,13 @@ case class ContractConditionInfo(predicate: Predicate, ci: ContractInfo) {
acslContext.getStructMap.get(fun).isDefined
}

def isACSLFunction(fun: IFunction): Boolean = {
ACSLExpression.functions.contains(fun)
}
def isACSLPredicate(pred: Predicate): Boolean = {
ACSLExpression.predicates.contains(pred)
}

def isPrecondition: Boolean = {
contractConditionType == Precondition
}
@@ -180,12 +187,8 @@ case class ContractConditionInfo(predicate: Predicate, ci: ContractInfo) {

if (input.startsWith(prefix) && input.endsWith(suffix)) {
input.substring(prefix.length, input.length - suffix.length)
} else if (
!input.contains("(") && !input.contains(")") && !input.contains("\\")
) {
input
} else {
throw new IllegalArgumentException(s"Invalid input: $input")
input
}
}