From d55e39c21c2020e5ec2c376defddaeee13f7c599 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Sat, 7 Sep 2024 13:34:54 +0200 Subject: [PATCH] fix instrumentation of location invariants at labels --- .../sequential/correctness/many-labels.c | 32 +++++++++++++++++++ .../many-labels.c-witness_v01.yaml | 25 +++++++++++++++ .../witness/ExtractedLocationInvariant.java | 18 ++++++++--- 3 files changed, 71 insertions(+), 4 deletions(-) create mode 100644 trunk/examples/witness-checking/regression/sequential/correctness/many-labels.c create mode 100644 trunk/examples/witness-checking/regression/sequential/correctness/many-labels.c-witness_v01.yaml diff --git a/trunk/examples/witness-checking/regression/sequential/correctness/many-labels.c b/trunk/examples/witness-checking/regression/sequential/correctness/many-labels.c new file mode 100644 index 00000000000..d5e7f49e034 --- /dev/null +++ b/trunk/examples/witness-checking/regression/sequential/correctness/many-labels.c @@ -0,0 +1,32 @@ +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +extern int __VERIFIER_nondet_int(); +void reach_error() { __assert_fail("0", "many-labels.c", 3, "reach_error"); } + +int main() { + int x = __VERIFIER_nondet_int(); + if (x < 0) { + return; + } + + if (x == -8) { + goto LABEL_A; + } + if (x == -16) { + goto LABEL_B; + } + if (x == -32) { + goto LABEL_C; + } + if (x == -64) { + goto LABEL_D; + } + return (0); + + LABEL_A: + LABEL_B: + LABEL_C: + LABEL_D: {reach_error();abort();} + return (-1); +} + diff --git a/trunk/examples/witness-checking/regression/sequential/correctness/many-labels.c-witness_v01.yaml b/trunk/examples/witness-checking/regression/sequential/correctness/many-labels.c-witness_v01.yaml new file mode 100644 index 00000000000..7aa9c0a9dab --- /dev/null +++ b/trunk/examples/witness-checking/regression/sequential/correctness/many-labels.c-witness_v01.yaml @@ -0,0 +1,25 @@ +- entry_type: location_invariant + metadata: + format_version: '0.1' + uuid: 386b0121-a302-415f-af28-bf0db7c36d11 + creation_time: '2024-09-07T13:26:54+01:00' + producer: + name: UNUSED + version: 0.2.4-dev-25b2402-m + task: + input_files: + - C:\ultimate\trunk\examples\witness-checking\regression\correctness\many-labels.c + input_file_hashes: + C:\ultimate\trunk\examples\witness-checking\regression\correctness\many-labels.c: UNUSED + specification: UNUSED + data_model: UNUSED + language: C + location: + file_name: C:\ultimate\trunk\examples\witness-checking\regression\correctness\many-labels.c + file_hash: UNUSED + line: 29 + function: main + location_invariant: + string: '0' + type: assertion + format: C diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedLocationInvariant.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedLocationInvariant.java index 451adce7129..2067c823b41 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedLocationInvariant.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedLocationInvariant.java @@ -28,10 +28,12 @@ package de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.witness; import java.util.List; +import java.util.stream.Collectors; import org.eclipse.cdt.core.dom.ast.IASTNode; import de.uni_freiburg.informatik.ultimate.boogie.ast.AtomicStatement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Label; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.IDispatcher; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResult; @@ -60,15 +62,23 @@ public boolean isBefore() { public ExpressionResult transform(final ILocation loc, final IDispatcher dispatcher, final ExpressionResult expressionResult) { final ExpressionResult invariantExprResult = instrument(loc, dispatcher); + final ExpressionResultBuilder erb = + new ExpressionResultBuilder(expressionResult).addAllExceptLrValueAndStatements(invariantExprResult); + // Make sure that the location invariant (incl. all auxiliary statements) is executed atomically. final Statement invariant = new AtomicStatement(loc, invariantExprResult.getStatements().toArray(Statement[]::new)); + + // Insert the location invariant at the appropriate location. if (mIsBefore) { - return new ExpressionResultBuilder(invariantExprResult).resetStatements(List.of(invariant)) - .addAllIncludingLrValue(expressionResult).build(); + // Push location invariants after leading labels, if there are any. + final var statements = expressionResult.getStatements(); + final List labels = + statements.stream().takeWhile(Label.class::isInstance).collect(Collectors.toList()); + final List remainder = statements.subList(labels.size(), statements.size()); + return erb.resetStatements(labels).addStatement(invariant).addStatements(remainder).build(); } - return new ExpressionResultBuilder(expressionResult).addAllExceptLrValueAndStatements(invariantExprResult) - .addStatement(invariant).build(); + return erb.addStatement(invariant).build(); } @Override