full_slicer: do not remove ASSUME false

An ASSUME false has no successors in the control-flow graph, so no
instruction is control dependent on it. The full slicer therefore removed
it unless it was the slicing criterion, which made the instructions that
follow it reachable on paths that it blocked, resulting in spurious
counterexamples. For example, each failing Java assertion is encoded as
ASSERT false followed by ASSUME false, so that with --full-slice any
later assertion was reported as failing with the values that violate the
first one. Loops unwound by goto-instrument --unwind (without unwinding
assertions) and function bodies generated with
--generate-function-body-options assume-false end paths the same way; in
the latter case the slicer removed the call of the function.

Always retain ASSUME false instructions. Their control dependencies, and
the calls of the function that contains them, are then retained as well.
On jbmc/regression/jbmc-strings with --full-slice this fixes 6 tests and
does not cause any new failures.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

jbmc/regression/jbmc/full-slice-assume-false/pom.xml

@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.full-slice-assume-false</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>

jbmc/regression/jbmc/full-slice-assume-false/src/main/java/Test.java

@@ -0,0 +1,7 @@
+public class Test {
+  public static void check(int x) {
+    assert x != 7;
+    // Only reachable if the first assertion holds
+    assert x != 7;
+  }
+}

jbmc/regression/jbmc/full-slice-assume-false/test.desc

@@ -0,0 +1,12 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test
+-cp target/classes --function Test.check --full-slice
+^\[java::Test\.check:\(I\)V\.assertion\.1\] line 3 .*: FAILURE$
+^\[java::Test\.check:\(I\)V\.assertion\.2\] line 5 .*: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+A failing Java assertion ends the path with ASSUME false. The full slicer must
+keep it, else the second assertion becomes reachable with x == 7.

jbmc/regression/jbmc/pom.xml

@@ -158,6 +158,7 @@
         <module>finally7</module>
         <module>float1</module>
         <module>FloatToIntConversion</module>
+        <module>full-slice-assume-false</module>
         <module>function1</module>
         <module>function2</module>
         <module>function3</module>

regression/goto-instrument/slice26/main.c

@@ -0,0 +1,19 @@
+int nondet_int();
+
+int main()
+{
+  int i = nondet_int();
+#ifdef __GNUC__
+  if(i == 2)
+  {
+    __CPROVER_assert(i < 100, "before the assumption");
+    // __builtin_types_compatible_p yields a proper "bool" typed constant,
+    // which makes this an ASSUME false
+    __CPROVER_assume(__builtin_types_compatible_p(double, float));
+  }
+#else
+  __CPROVER_assume(i != 2);
+#endif
+  __CPROVER_assert(i != 2, "only reachable with i != 2");
+  return 0;
+}

regression/goto-instrument/slice26/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--full-slice
+^\[main.assertion.1\] line \d+ before the assumption: SUCCESS$
+^\[main.assertion.2\] line \d+ only reachable with i != 2: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The full slicer must not remove an ASSUME false: it has no successors in the
+control-flow graph, so that no instruction is control dependent on it, but
+removing it makes the second assertion reachable with i == 2.

regression/goto-instrument/slice27/main.c

@@ -0,0 +1,16 @@
+int nondet_int();
+void stop(void);
+
+int main()
+{
+  int i = nondet_int();
+  if(i == 2)
+  {
+    __CPROVER_assert(i < 100, "before the call");
+    // The body of stop is generated using --generate-function-body, it is
+    // just ASSUME false.
+    stop();
+  }
+  __CPROVER_assert(i != 2, "only reachable with i != 2");
+  return 0;
+}

regression/goto-instrument/slice27/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--generate-function-body stop --generate-function-body-options assume-false --full-slice
+^\[main.assertion.1\] line \d+ before the call: SUCCESS$
+^\[main.assertion.2\] line \d+ only reachable with i != 2: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The full slicer must keep the call of a function that does not return, here
+because its body is ASSUME false: removing the call makes the second assertion
+reachable with i == 2.

src/goto-instrument/full_slicer.cpp

@@ -239,6 +239,14 @@ static bool implicit(goto_programt::const_targett target)
   if(statement==ID_array_copy)
     return true;
 
+  // An ASSUME false ends all paths through it. As it has no successors in
+  // the CFG, no instruction is control dependent on it, and neither are the
+  // instructions following a call of a function that does not return because
+  // of it. Removing it would, however, make those instructions reachable on
+  // the paths that it blocks.
+  if(target->is_assume() && target->condition() == false)
+    return true;
+
   if(!target->is_assign())
     return false;