From 97c1a48cfa03365dff64e939a11c0514cf4abe1d Mon Sep 17 00:00:00 2001 From: Zafer Esen Date: Thu, 1 Feb 2024 21:55:59 +0100 Subject: [PATCH] Fix valid-cleanup not being violated at abort statements --- regression-tests/properties/Answers | 3 +++ regression-tests/properties/runtests | 2 +- .../properties/valid-memcleanup-4-false.c | 10 ++++++++++ src/tricera/concurrency/CCReader.scala | 15 +++++++++++---- 4 files changed, 25 insertions(+), 5 deletions(-) create mode 100644 regression-tests/properties/valid-memcleanup-4-false.c diff --git a/regression-tests/properties/Answers b/regression-tests/properties/Answers index 1337d70..f6b2c9f 100644 --- a/regression-tests/properties/Answers +++ b/regression-tests/properties/Answers @@ -85,3 +85,6 @@ SAFE valid-free-12-false.c UNKNOWN (4:7 Casts between pointer and arithmetic types are not supported.) + +valid-memcleanup-4-false.c +UNSAFE diff --git a/regression-tests/properties/runtests b/regression-tests/properties/runtests index 49a86d5..25467e8 100755 --- a/regression-tests/properties/runtests +++ b/regression-tests/properties/runtests @@ -14,7 +14,7 @@ TESTS="valid-free-10-true.c valid-free-3-true.c valid-free-7-false.c \ valid-memcleanup-1-true.c valid-memcleanup-array-true.c \ valid-memtrack-array-true.c valid-memcleanup-2-false.c \ valid-memcleanup-3-false.c valid-memcleanup-3-true.c \ - valid-free-12-false.c" + valid-free-12-false.c valid-memcleanup-4-false.c" for name in $TESTS; do echo diff --git a/regression-tests/properties/valid-memcleanup-4-false.c b/regression-tests/properties/valid-memcleanup-4-false.c new file mode 100644 index 0000000..4a7e42c --- /dev/null +++ b/regression-tests/properties/valid-memcleanup-4-false.c @@ -0,0 +1,10 @@ +#include + +extern int nondet(); +int main() { + int *p = malloc(sizeof(int)); + // p is not freed before program end - violates memcleanup. + // int main with multiple exit paths + abort(); + free(p); +} diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala index ce4574e..63ea9f2 100644 --- a/src/tricera/concurrency/CCReader.scala +++ b/src/tricera/concurrency/CCReader.scala @@ -257,7 +257,6 @@ class CCReader private (prog : Program, } private var globalPreconditions : IFormula = true - private val globalExitPred = newPred("exit", Nil, None) private def lookupVarNoException(name : String, enclosingFunction : String) : Int = { @@ -714,6 +713,14 @@ class CCReader private (prog : Program, variableHints += List() } + /** + * It is important that globalExitPred has arguments for the ghost variables + * and the heap - for instance we want to check that memory is cleaned before + * exit, and it cannot be done if the prophecy variable does not exist at + * that point. This is reachable, for instance, with the `abort` statement. + */ + private val globalExitPred = newPred("exit", allFormalVars, None) + private val structCtorsOffset = predefSignatures.size val defObj = heap.userADTCtors.last val structCount = structInfos.size @@ -1137,12 +1144,12 @@ class CCReader private (prog : Program, * return type, the function can still end without reaching a * return statement - which is why there can be multiple `finalPreds`. */ - val finalPreds = + val finalPreds = Seq(globalExitPred) ++ ( if (returnType != CCVoid) { val exitWithoutReturnPred = translator.translateWithReturn(stm) Seq(exitWithoutReturnPred, exitPred) } - else Seq(translator.translateNoReturn(stm)) + else Seq(translator.translateNoReturn(stm))) /** * Add an assertion that all pointers that are in scope at the @@ -4842,7 +4849,7 @@ private def collectVarDecls(dec : Dec, } case _ : SjumpAbort | _ : SjumpExit => // abort() or exit(int status) output(addRichClause( - Clause(atom(globalExitPred, Nil), + Clause(atom(globalExitPred, allFormalVarTerms take globalExitPred.arity), List(atom(entry, allFormalVarTerms take entry.arity)), true), srcInfo)) }