Bug: Detection of assertions depending on format

[FahrJo]

Basic Info

• Version: 0.2.3-dev-70e0b1d
• (Optional) Java Version: 11.0.19+7
• Settings:

\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ if\ freed\ pointer\ was\ valid=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Pointer\ to\ allocated\ memory\ at\ dereference=IGNORE
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ division\ by\ zero=IGNORE
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ array\ bounds\ for\ arrays\ that\ are\ off\ heap=IGNORE
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/If\ two\ pointers\ are\ subtracted\ or\ compared\ they\ have\ the\ same\ base\ address=IGNORE
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Pointer\ base\ address\ is\ valid\ at\ dereference=IGNORE
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/How\ to\ treat\ unsigned\ ints\ differently\ from\ normal\ ones=IGNORE
file_export_version=3.0
@de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.1.25
\!/instance/de.uni_freiburg.informatik.ultimate.boogie.preprocessor=
/instance/de.uni_freiburg.informatik.ultimate.boogie.preprocessor/Simplify\ expressions=true
file_export_version=3.0
@de.uni_freiburg.informatik.ultimate.boogie.preprocessor=0.1.25

• Toolchain:

<rundefinition>
	<name>Ultimate Automizer</name>
	<toolchain>
		<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
		<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
		<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
		<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction"/>
	</toolchain>
</rundefinition>

Description

I would expect Ultimate to work steh same way on the following two semantically identical input files:

//#Safe
int nondet() {
    int x;
    return x;
}

int main() {
    int x, y;
    x = 0;
    y = 0;
    while (nondet()) {
        x = x + 1;
    }
    /*@ assert x != -1; */
    /*@ assert y != -1; */
    return 0;
}

Ultimate Result:

--- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * CDTParser took 0.46ms. Allocated memory is still 536.9MB. Free memory was 518.7MB in the beginning and 518.6MB in the end (delta: 178.3kB). There was no memory consumed. Max. memory is 12.9GB.
 * CACSL2BoogieTranslator took 288.84ms. Allocated memory is still 536.9MB. Free memory was 476.2MB in the beginning and 467.5MB in the end (delta: 8.8MB). Peak memory consumption was 8.4MB. Max. memory is 12.9GB.
 * Boogie Preprocessor took 55.28ms. Allocated memory is still 536.9MB. Free memory was 467.5MB in the beginning and 466.2MB in the end (delta: 1.3MB). Peak memory consumption was 2.1MB. Max. memory is 12.9GB.
 * RCFGBuilder took 416.18ms. Allocated memory is still 536.9MB. Free memory was 466.0MB in the beginning and 508.3MB in the end (delta: -42.3MB). Peak memory consumption was 11.7MB. Max. memory is 12.9GB.
 * TraceAbstraction took 1097.10ms. Allocated memory is still 536.9MB. Free memory was 508.3MB in the beginning and 478.9MB in the end (delta: 29.4MB). Peak memory consumption was 29.4MB. Max. memory is 12.9GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Line: 17]: assertion always holds
    For all program executions holds that assertion always holds at this location
  - PositiveResult [Line: 18]: assertion always holds
    For all program executions holds that assertion always holds at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 4 procedures, 17 locations, 2 error locations. Started 1 CEGAR loops. OverallTime: 1.0s, OverallIterations: 3, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.3s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 3 SdHoareTripleChecker+Valid, 0.1s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 3 mSDsluCounter, 46 SdHoareTripleChecker+Invalid, 0.1s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 10 mSDsCounter, 1 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 8 IncrementalHoareTripleChecker+Invalid, 9 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 1 mSolverCounterUnsat, 36 mSDtfsCounter, 8 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 27 GetRequests, 25 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=17occurred in iteration=0, InterpolantAutomatonStates: 8, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.0s AutomataMinimizationTime, 3 MinimizatonAttempts, 0 StatesRemovedByMinimization, 0 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 0.2s InterpolantComputationTime, 30 NumberOfCodeBlocks, 30 NumberOfCodeBlocksAsserted, 3 NumberOfCheckSat, 27 ConstructedInterpolants, 0 QuantifiedInterpolants, 45 SizeOfPredicates, 0 NumberOfNonLiveVariables, 72 ConjunctsInSsa, 5 ConjunctsInUnsatCore, 3 InterpolantComputations, 3 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    2 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2023-04-20 12:14:51,298 INFO  L540       MonitoredProcess]: [MP /home/z3 SMTLIB2_COMPLIANT=true -memory:1024 -smt2 -in -t:12000 (1)] Forceful destruction successful, exit code 0
Received shutdown request...

VS.

//#Safe
int nondet() { int x; return x;}int main() { int x, y; x = 0; y = 0; while (nondet()) { x = x + 1; } /*@ assert x != -1; */ /*@ assert y != -1; */ return 0;}

Ultimate Result:

--- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * CDTParser took 0.34ms. Allocated memory is still 536.9MB. Free memory is still 518.1MB. There was no memory consumed. Max. memory is 12.9GB.
 * CACSL2BoogieTranslator took 232.35ms. Allocated memory is still 536.9MB. Free memory was 475.3MB in the beginning and 466.4MB in the end (delta: 8.9MB). Peak memory consumption was 8.4MB. Max. memory is 12.9GB.
 * Boogie Preprocessor took 41.98ms. Allocated memory is still 536.9MB. Free memory was 466.4MB in the beginning and 465.0MB in the end (delta: 1.4MB). Peak memory consumption was 2.1MB. Max. memory is 12.9GB.
 * RCFGBuilder took 326.17ms. Allocated memory is still 536.9MB. Free memory was 465.0MB in the beginning and 508.9MB in the end (delta: -44.0MB). Peak memory consumption was 12.3MB. Max. memory is 12.9GB.
 * TraceAbstraction took 37.65ms. Allocated memory is still 536.9MB. Free memory was 508.9MB in the beginning and 506.6MB in the end (delta: 2.3MB). Peak memory consumption was 2.1MB. Max. memory is 12.9GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - AllSpecificationsHoldResult: All specifications hold
    We were not able to verify any specification because the program does not contain any specification.
RESULT: Ultimate proved your program to be correct!
[2023-04-20 12:16:48,128 INFO  L540       MonitoredProcess]: [MP /home/z3 SMTLIB2_COMPLIANT=true -memory:1024 -smt2 -in -t:12000 (1)] Forceful destruction successful, exit code 0
Received shutdown request...

In the second case, the Assertions are not even detected.

[danieldietsch]

Sadly, this is a known limitation of our rather ad-hoc ACSL support. Each assertion needs to have its own line.

In what context do you encounter programs written in such a way?

[FahrJo]

I was thinking of automatic annotation of the input program from an easier understandable specification description. By inlining all the generated assertions, the line numbers of the original input file would have been still valid for the Ultimate results (e.g. the counter example) of the "preprocessed" input file. But if it's a konwn issue, I'll find a workaround for it👍

[schuessf]

What other specifications do you want do add? Ultimate already supports various specifications like overflows and memsafety. Checking them can be enabled in the cacsl2boogietranslator settings. Assertions for those specifications are then added directly in the translation process (without adding ACSL assertions), therefore the correct line number occurs in the result.

[FahrJo]

It is for a POC of implementing THADs (temporal HAL-API dependencies) and it probably should be done directly as a Ultimate tool in a longterm perspective, but I didn't want to dive that deep directly at the beginning ;-)

[danieldietsch]

Then you might also want to look at our support for LTL properties, in particular if you are interested in properties of the form "If I call this method, I will eventually call that method".

[FahrJo]

Yes, thanks for the hint, but it isn't possible to check function calls directly, is it? So I still need helper variables?

[danieldietsch]

Yes, although it would be only a small extension.