diffblue / cbmc Goto Github PK
View Code? Open in Web Editor NEWC Bounded Model Checker
Home Page: https://diffblue.github.io/cbmc
License: Other
C Bounded Model Checker
Home Page: https://diffblue.github.io/cbmc
License: Other
(...or better not!)
I stumbled over this concession to Pascal programmers:
https://gcc.gnu.org/onlinedocs/gcc/Nested-Functions.html
Test case:
https://github.com/JoliOS/grub2/blob/master/util/grub-fstest.c#L211
Note that this feature is not used in the original grub code:
http://git.savannah.gnu.org/cgit/grub.git/tree/util/grub-fstest.c#n240
cbmc --smt2 foo.c with
int main() { assert(0); }
yields
$ cbmc/cbmc --smt2 foo.c
CBMC version 5.4 64-bit x86_64 macos
Parsing foo.c
Converting
Type-checking foo
file foo.c line 1 function main: function `assert' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 30 steps
simple slicing removed 3 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to SMT2 QF_AUFBV using MathSAT
converting SSA
Running SMT2 QF_AUFBV using MathSAT
Runtime decision procedure: 0.008s
** Results:
[main.assertion.1] assertion 0: SUCCESS
** 0 of 1 failed (1 iteration)
VERIFICATION SUCCESSFUL
when I don't have MathSAT anywhere near my PATH.
Best,
Michael
This file returns the following error with cbmc --cover location --unwind 3 --function "com.datastax.driver.core.VersionNumber.hashCode:()I" com/datastax/driver/core/VersionNumber.class
converting SSA
byte_extract flatting of non-constant source size: byte_extract_little_endian
* type: pointer
0: struct
* tag: java::array[reference]
* components:
0:
* type: struct
* incomplete_class: 1
* name: java::java.lang.Object
* tag: java.lang.Object
* base_name: java.lang.Object
* components:
0:
* type: string
* name: @class_identifier
* pretty_name: @class_identifier
* #class: 1
* name: @java.lang.Object
1:
* type: signedbv
* width: 32
* #c_type: signed_int
* name: length
2:
* type: pointer
0: pointer
* #failed_symbol: java::com.datastax.driver.core.VersionNumber.hashCode:()I::this$object
0: empty
* name: data
0: symbol
* type: empty
* identifier: tmp_struct_init$1!0#1
* expression: symbol
* type: empty
* identifier: tmp_struct_init$1
* L0: 0
* L2: 1
* #SSA_symbol: 1
1: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 0000000000000000000000000000000000000000000000000000000000100100
a similar error appears for this method
For the class file of this source, CBMC fails on loading with the following assertion violation:
Converting
cbmc: java_bytecode_typecheck_expr.cpp:114: void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt&): Assertion `has_prefix(id2string(identifier), "java::")' failed.
The problem is the identifier `::ceil`` (line 49/50).
For thie file the following cbmc --unwind 3 --function "com.datastax.driver.core.querybuilder.Utils.containsBindMarker:(Ljava/lang/Object;)Z" com/datastax/driver/core/querybuilder/Utils.class
returns identifier __CPROVER_memory not found
bmct and incremental_bmct can be easily used interchangeably in other BMC-based tools (like cegis)
most of that has already been done in the peter-incremental-unwinding branch
produce JSON formatted output, similar to --xml-ui
When checking for division by zero, the following shows different results when analyzing the static method f
(passes the verification) and g
(fails verification), although non-deterministic choice for the input integer should allow for a = -1
in the first case, too.
public class StaticMethod {
static public void f(int a, int b) {
int c = b/(a+1);
}
static public void g(int a, int b) {
int c = a/(b+1);
}
}
The problem seems to be that the first parameter that is passed to the static method is the result of a malloc, i.e., the memory allocated for a StaticMethod
object instance. Whereas, in the function it is treated as a NONDET(int)
.
// 0 no location
__CPROVER_initialize();
// 1 no location
tmp_struct_init$1 = MALLOC(struct StaticMethod { struct java.lang.Object @java.lang.Object; }, 4);
// 2 no location
tmp_struct_init$1->@java.lang.Object.@class_identifier = "StaticMethod";
// 3 no location
StaticMethod.g:(II)V(tmp_struct_init$1, NONDET(int));
// 4 no location
END_FUNCTION
StaticMethod.f() /* java::StaticMethod.f:(II)V */
// 7 file StaticMethod.java line 4
ASSERT !(arg0i == -1) // division by zero in arg1i / (arg0i + 1)
// 8 file StaticMethod.java line 4
local2i = arg1i / (arg0i + 1);
// 9 no location
END_FUNCTION
For example, when supplying a Class object in the form of String.class
, CBMC fails with
function call: parameter "java::classtest1.f:(Ljava/lang/Class;Z)Z::arg1a" type mismatch: got struct
* incomplete_class: 1
* name: java::java.lang.String
* tag: java.lang.String
* base_name: java.lang.String
* components:
0:
* type: string
* name: @class_identifier
* pretty_name: @class_identifier
* #class: 1, expected pointer
* #reference: 1
0: symbol
* identifier: java::java.lang.Class
* #base_name: java.lang.Class
regression test:
public class classtest1
{
public void test()
{
assert(f(String.class, true));
}
public boolean f(Class c, boolean b)
{
return b;
}
}
This example fails with unexpected statement: monitorenter
public class monitorenter1
{
public boolean doIt(boolean b)
{
boolean a;
synchronized(this) {
a = !b;
}
return a;
}
public void test()
{
assert(doIt(false));
}
}
the critical section is enclosed between monitorenter
and monitorexit
in the bytecode.
regression tests coming...
These are marked KNOWNBUG at the moment, because goto-cc accepts what gcc wouldn't:
Array_Declarator2/main.c:5:18: error: variable length array must be bound in function definition
void fooStar(int x[*])
^
1 error generated.
$ gcc Array_Declarator3/main.c
Array_Declarator3/main.c:7:11: error: type qualifier used in array declarator outside of function prototype
int bar0[restrict] = {0};
^
1 error generated.
$ gcc Array_Declarator4/main.c
Array_Declarator4/main.c:7:11: error: 'static' used in array declarator outside of function prototype
int bar1[static 1U] = {1};
^
1 error generated.
$ gcc Array_Declarator5/main.c
Array_Declarator5/main.c:7:11: error: type qualifier used in array declarator outside of function prototype
int bar2[restrict 2U] = {1, 2};
^
1 error generated.
$ gcc Array_Declarator6/main.c
Array_Declarator6/main.c:7:11: error: 'static' used in array declarator outside of function prototype
int bar3[restrict static 3U] = {1, 2, 3};
^
1 error generated.
$ gcc Array_Declarator7/main.c
Array_Declarator7/main.c:7:11: error: 'static' used in array declarator outside of function prototype
int bar4[static restrict 4U] = {1, 2, 3, 4};
^
1 error generated.
It may be debatable whether the C front end really needs to produce errors here, it safely ignores these extra qualifiers anyway.
Best,
Michael
patches exist, further performance improvements on the todo list...
currently,
goto-cc class-file -o goto-binary
produces a goto-binary, but
cbmc goto-binary
fails with "Multi-language linking not supported", and
goto-instrument goto-binary --show-goto-functions
fils with "symbol `_start' has unknown mode 'java'"
Hi,
This is not an issue but just few queries regarding cbmc in svcomp16.
extract patch from new lock analysis implementation
When analyzing Java bytecode, it is possible to get assignments with a nondet_symbol
on the left hand side. For the following program:
public class nondetassign1
{
class B
{
boolean a;
B f()
{
this.a = true;
return this;
}
}
class A extends B
{
A f()
{
this.a = true;
return this;
}
void g()
{
boolean b = this.a;
boolean c = this.a;
assert(b == c);
}
}
}
when one removes the nondetassign1\$B.class
file, one gets the following result for cbmc --function "nondetassign1\$A.f:()Lnondetassign1\$A;" nondetassign1\$A.class
:
assignment to 'nondet_symbol' not handled
this does work with the temporary fix as follows:
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index c75905f..a9323aa 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -235,6 +235,8 @@ void goto_symext::symex_assign_rec(
symex_assign_rec(state, lhs.op0(), full_lhs, new_rhs, guard, assignment_type);
}
+ else if(lhs.id() == ID_nondet_symbol)
+ return;
else
throw "assignment to `"+lhs.id_string()+"' not handled";
}
in addition, the result for cbmc --function "nondetassign1\$A.g" nondetassign1\$A.class
is:
** Results:
[assertion.1] assertion at file nondetassign1.java line 23: FAILURE
** 1 of 1 failed (1 iteration)
VERIFICATION FAILED
Would it be possible to treat such a variable in the following way:
$nondet1
and assign an initial NONDET value$nondet1
as side effectwhen --function is given, cbmc should analyze the binary regardless of the presence of a main() function
run for example with --unwind 2 --z3
array theory should be used, but "failed to get width of byte_update" is thrown
array index expressions are translated correctly for arrays of variable size
#include <assert.h>
unsigned nondet_unsigned();
int main() {
unsigned n = nondet_unsigned();
__CPROVER_assume(n>0);
// unsigned p[n]; // (1)
unsigned *p = (unsigned *)malloc(sizeof(unsigned) * n); // (2)
for (int i=0; i<n; i++) {
p[i] = i; // correctly translated for (1), error thrown for (2)
}
assert(p[n-1] == n-1);
return 0;
}
byte_update is used for p[i] although the type of p in the goto program is array of size (const * variable). Couldn't an index expression be generated if the access is obviously aligned?
With the command line cbmc --cover location --unwind 3 --function iterator1.f iterator1.class
, the following program unwinds the loop indefinitely:
import java.util.List;
public class iterator1
{
public void f(List<List<String>> list)
{
int i = 0;
for(List<String> l : list)
for(String s : l)
i++;
}
}
leads to
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
Not unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 3 (3 max) file iterator1.java line 10 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 1 (3 max) file iterator1.java line 9 thread 0
Unwinding loop java::iterator1.f:(Ljava/util/List;)V.0 iteration 2 (3 max) file iterator1.java line 10 thread 0
...
The following fails with cbmc --cover location --function bitwise1.f bitwise1.class
with the above error.
public class bitwise1
{
static char c;
void f()
{
int i = (c & 2);
}
}
In boolbvt_bitwise::convert_bitwise
the reported width of the char
operand is 16 (from std::size_t width=boolbv_width(expr.type());
) but the size of the converted operand is 32. Java uses widening numeric promotion to int
in this case. Interestingly, this program does not produce the above error in the following version (1 instead of 2):
public class bitwise1
{
static char c;
void f()
{
int i = (c & 1);
}
}
A continue
statement in the loop disappears after the --dump-c
operation. This bug in --dump-c
can be re-generated as follows. The code used is from regression/cbmc/for2/main.c
int main()
{
int i;
int k;
for (i=0; i<3; i++)
{
k=3;
continue;
k=4;
}
assert(0);
}
goto-cc main.c -o main.goto
goto-instrument main.goto --dump-c
The resulted code after '--dump-c' is shown in below.
#include <assert.h>
// assert
// file main.c line 13 function main
signed int assert(void);
// main
// file main.c line 1
signed int main()
{
signed int i;
signed int k;
i = 0;
for( ; !(i >= 3); i = i + 1)
{
k = 3;
k = 4;
}
/* assertion 0 */
assert((_Bool)0);
}
As we can see, the 'continue' statement disappears in the --dump-c
result.
Meanwhile, the --show-goto-functions
confirms that the continue
statement is still within the goto program.
currently it returns 6
I am trying to build the current master on my mac.
The build fails because zip.h
cannot be found:
$ make
## Entering big-int
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C big-int
make[1]: Nothing to be done for `first_target'.
## Entering util
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C util
make[1]: Nothing to be done for `first_target'.
## Entering langapi
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C langapi
make[1]: Nothing to be done for `first_target'.
## Entering ansi-c
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C ansi-c
make[1]: Nothing to be done for `first_target'.
## Entering linking
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C linking
make[1]: Nothing to be done for `first_target'.
## Entering cpp
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C cpp
make[1]: Nothing to be done for `first_target'.
## Entering xmllang
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C xmllang
make[1]: Nothing to be done for `first_target'.
## Entering assembler
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C assembler
make[1]: Nothing to be done for `first_target'.
## Entering java_bytecode
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C java_bytecode
clang++ -c -MMD -MP -mmacosx-version-min=10.9 -std=c++11 -stdlib=libc++ -D STL_HASH_STD -Wall -O2 -I .. -I ../../libzip/lib -DHAVE_LIBZIP -o jar_file.o jar_file.cpp
jar_file.cpp:15:10: fatal error: 'zip.h' file not found
#include <zip.h>
^
1 error generated.
make[1]: *** [jar_file.o] Error 1
make:
When built with gcc, this program runs and the assertion does not fire:
#include <string.h>
#include <assert.h>
int main() {
char arr[] = { 'a', 'a', 'a', 0};
assert(strchr(arr, 0) == arr + sizeof(arr) - 1);
}
However, cbmc 5.4 says that VERIFICATION FAILED:
CBMC version 5.4 64-bit x86_64 linux
Parsing strend.c
Converting
Type-checking strend
Generating GOTO Program
Adding CPROVER library (x86_64)
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop main.0 iteration 1 file strend.c line 5 function main thread 0
Unwinding loop main.0 iteration 2 file strend.c line 5 function main thread 0
Unwinding loop main.0 iteration 3 file strend.c line 5 function main thread 0
size of program expression: 60 steps
simple slicing removed 3 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
264 variables, 11 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.001s
Building error trace
Counterexample:
State 18 file strend.c line 4 function main thread 0
----------------------------------------------------
arr={ 0, 0, 0, 0 } ({ 00000000, 00000000, 00000000, 00000000 })
State 19 file strend.c line 4 function main thread 0
----------------------------------------------------
arr={ 'a', 'a', 'a', 0 } ({ 01100001, 01100001, 01100001, 00000000 })
Violated property:
file strend.c line 5 function main
assertion strchr(arr, 0) == arr + sizeof(arr) - 1
return_value_strchr$1 == (arr + (signed long int)sizeof(char [4l]) /*4ul*/ ) - (signed long int)1
VERIFICATION FAILED
I think that the implementation of strchr (and probably strrchr, though I did not test it) is defective, because it ignores this statement from the C99 standard: "The terminating null character is considered to be part of the string." (7.21.5.2 in ISO/IEC 9899:TC3 Committee Draft WG14/N1256)
Hi,
I'm using CMBC 5.3 to check pointer safety of following program.
#include<stdio.h>
#include<stdlib.h>
int main()
{
char *c = malloc(1);
printf("%p\n", c);
c = c + 20;
printf("%p\n", c);
printf("%d\n", *c);
free(c - 20);
return 0;
}
Here I'm dereferencing a pointer which is 20 unit away from legally allocated memory. Why CBMC is not reporting this program as unsafe? Am I missing something?
...to be able to distinguish e.g. global/local variables.
For recursive functions in JVM bytecode, CBMC fails with
main method ` ... ' has no body
patches exist, but performance is not yet convincing
The following fails when checking with --ilp32 (for nbytes >=2^24)
uint32_t nondet_uint32_t();
void mk_char_array() {
uint32_t nbytes = nondet_uint32_t();
char memory[nbytes];
char *start = &memory[0];
char *end = &memory[nbytes];
uint32_t diff = end - start;
__CPROVER_assert(diff == nbytes, "Check size match");
}
It's rare to allocate arrays of that size in software, and few people use ILP32, however, the restriction is an unnecessary artefact of the encoding that CBMC uses (upper 8 bits for object reference, remaining bits for offset within the object)...
The problem doesn't occur with LP64 (64-8 > 48).
Issue raised by Nathan Chong, ARM.
This program
public class boolean2
{
public void entry(boolean b)
{
f(b);
assert(true);
}
public boolean f(boolean b)
{
return !b;
}
}
fails with
function call: parameter "java::boolean2.f:(Z)Z::arg1z" type mismatch: got signedbv
* width: 32, expected c_bool
* width: 8
on cbmc --function "boolean2.entry" boolean2.class
with cbmc version that passes boolean1 test.
There is a regression test for this in #89
Both CBMC 5.4 and the current development version (master branch) incorrectly output "VERIFICATION FAILED" when run on the following test case.
#include <assert.h>
#include <stdbool.h>
#include <stdlib.h>
struct list_entry {
struct list_entry *next;
};
struct linked_list {
struct list_entry *head;
struct list_entry **tail;
};
struct linked_list_container {
struct linked_list list;
};
int main(int argc, char* argv[])
{
struct linked_list_container container;
struct linked_list *list = &container.list;
struct list_entry head;
list->head = NULL;
list->tail = &list->head;
*list->tail = &head;
list->tail = &head.next;
assert(list->head);
return 0;
}
I have uploaded CBMC's output for this program to this gist. It looks CBMC thinks that list->tail
points to an invalid object at line 27 of test_case.c.
In the following program the function f
verifies div-by-zero, g
correctly fails this property.
public class StaticMember
{
static int xs;
int x;
public void f()
{
int d = 1 / (1 + xs);
}
public void g()
{
int d = 1 / (1 + x);
}
}
When using either function as entry point, the value of the non-local variable should be considered non-deterministic.
This is currently known as ansi-c/KnR3 regression test, which fails with a parser error.
This program
public class Inheritance2
{
int x;
public class A extends Inheritance2
{
void m1(int i)
{
if (x == 1)
assert(true);
else
assert(false);
}
void m2(int i)
{
switch(x)
{
case 1:
assert(true);
break;
default:
assert(false);
break;
}
}
void test1(int i)
{
m1(i);
}
void test2(int i)
{
m2(i);
}
}
}
correctly reports on cbmc --function "Inheritance2\$A.test1" Inheritance2.class
** Results:
[assertion.1] assertion at file Inheritance2.java line 11: FAILURE
[assertion.2] assertion at file Inheritance2.java line 21: SUCCESS
but fails on cbmc --function "Inheritance2\$A.test2" Inheritance2.class
with
size of program expression: 57 steps
simple slicing removed 8 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
component x not found in structure
In the current implementation, the indices of the variables in the local variable table are used without considering the StackMapTable
code attribute. For larger methods this leads to wrong names and types of the variables.
For example in BasicTikaFSConsumerBuilder.java the following code
if( tikaConfigPath == null) {
Node tikaConfigNode = node.getAttributes().getNamedItem("tikaConfig");
if (tikaConfigNode != null) {
tikaConfigPath = PropsUtil.getString(tikaConfigNode.getNodeValue(), null);
}
}
if (tikaConfigPath != null) {
try (InputStream is = Files.newInputStream(Paths.get(tikaConfigPath))) {
config = new TikaConfig(is);
} catch (Exception e) {
throw new RuntimeException(e);
}
} else {
config = TikaConfig.getDefaultConfig();
}
List<FileResourceConsumer> consumers = new LinkedList<FileResourceConsumer>();
int numConsumers = BatchProcessBuilder.getNumConsumers(runtimeAttributes);
results in the following bytecode
167: ifnonnull 203
170: aload_1
171: invokeinterface #8, 1 // InterfaceMethod org/w3c/dom/Node.getAttributes:()Lorg/w3c/dom/NamedNodeMap;
176: ldc #14 // String tikaConfig
178: invokeinterface #9, 2 // InterfaceMethod org/w3c/dom/NamedNodeMap.getNamedItem:(Ljava/lang/String;)Lorg/w3c/dom/Node;
183: astore 10
185: aload 10
187: ifnull 203
190: aload 10
192: invokeinterface #10, 1 // InterfaceMethod org/w3c/dom/Node.getNodeValue:()Ljava/lang/String;
197: aconst_null
198: invokestatic #15 // Method org/apache/tika/util/PropsUtil.getString:(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;
201: astore 9
203: aload 9
205: ifnull 342
208: aload 9
210: iconst_0
211: anewarray #4 // class java/lang/String
214: invokestatic #16 // Method java/nio/file/Paths.get:(Ljava/lang/String;[Ljava/lang/String;)Ljava/nio/file/Path;
217: iconst_0
218: anewarray #17 // class java/nio/file/OpenOption
221: invokestatic #18 // Method java/nio/file/Files.newInputStream:(Ljava/nio/file/Path;[Ljava/nio/file/OpenOption;)Ljava/io/InputStream;
224: astore 10
...
342: invokestatic #27 // Method org/apache/tika/config/TikaConfig.getDefaultConfig:()Lorg/apache/tika/config/TikaConfig;
345: astore 8
347: new #28 // class java/util/LinkedList
350: dup
351: invokespecial #29 // Method java/util/LinkedList."<init>":()V
354: astore 10
with the following local variable table (irrelevant parts omitted):
LocalVariableTable:
Start Length Slot Name Signature
...
185 18 10 tikaConfigNode Lorg/w3c/dom/Node;
260 7 12 x2 Ljava/lang/Throwable;
309 7 14 x2 Ljava/lang/Throwable;
226 101 10 is Ljava/io/InputStream;
...
356 293 10 consumers Ljava/util/List;
...
in the goto-program, it is the variable consumers
which gets assigned the values intended for tikaConfigNode
// 410 file BasicTikaFSConsumersBuilder.java line 87
return_tmp18 = NONDET(struct org.w3c.dom.Node *);
// 411 file BasicTikaFSConsumersBuilder.java line 87
consumers = (struct java.util.List *)return_tmp18;
// 412 file BasicTikaFSConsumersBuilder.java line 88
IF (void *)(void *)consumers == null THEN GOTO 5
// 413 file BasicTikaFSConsumersBuilder.java line 89
ASSERT false // block 31
// 414 file BasicTikaFSConsumersBuilder.java line 89
(void *)consumers . org.w3c.dom.Node.getNodeValue:()Ljava/lang/String;();
and is
// 437 file BasicTikaFSConsumersBuilder.java line 93
return_tmp24 = NONDET(struct java.io.InputStream *);
// 438 file BasicTikaFSConsumersBuilder.java line 93
consumers = (struct java.util.List *)return_tmp24;
// 439 file BasicTikaFSConsumersBuilder.java line 93
numConsumers = (int)null;
// 440 file BasicTikaFSConsumersBuilder.java line 94
new_tmp25 = MALLOC(struct org.apache.tika.config.TikaConfig, 4);
// 441 file BasicTikaFSConsumersBuilder.java line 94
*new_tmp25 = { .@class_identifier="java::org.apache.tika.config.TikaConfig" };
// 442 file BasicTikaFSConsumersBuilder.java line 94
new_tmp25 . org.apache.tika.config.TikaConfig.<init>:(Ljava/io/InputStream;)V((void *)consumers);
// 443 file BasicTikaFSConsumersBuilder.java line 94
ASSERT false // block 38
// 444 file BasicTikaFSConsumersBuilder.java line 94
config = (struct org.apache.tika.config.TikaConfig *)new_tmp25;
// 445 file BasicTikaFSConsumersBuilder.java line 95
IF (void *)(void *)consumers == null THEN GOTO 7
// 446 file BasicTikaFSConsumersBuilder.java line 95
ASSERT false // block 39
// 447 file BasicTikaFSConsumersBuilder.java line 95
IF (void *)(void *)numConsumers == null THEN GOTO 6
// 448 file BasicTikaFSConsumersBuilder.java line 95
ASSERT false // block 40
// 449 file BasicTikaFSConsumersBuilder.java line 95
(void *)consumers . java.io.InputStream.close:()V();
although consumers
is of type List<FileResourceConsumer>
, which is also the cast in the goto-program in the above example.
The reason for this is that the index of all three variables is 10
and consumers
is the last using this index.
To correct this, one has to take into account the relevant StackMapTable
of the code (if such a table does exists). The relevant frame for the correct usage of consumers
is this:
frame_type = 255 /* full_frame */
offset_delta = 34
locals = [ class org/apache/tika/batch/fs/builders/BasicTikaFSConsumersBuilder, class org/w3c/dom/Node, class java/util/Map, class java/util/concurrent/ArrayBlockingQueue, int, class java/lang/String, class java/lang/Long, class java/lang/String, class org/apache/tika/config/TikaConfig, class java/lang/String, class java/util/List, int, class org/w3c/dom/NodeList, class org/w3c/dom/Node, class org/w3c/dom/Node, class org/w3c/dom/Node, int ]
stack = []
while the correct ones for the preceeding variables with index 10 have to be constructed with the stack frame entries before.
For some class files, --show-symbol-table
fails with identifier java::java.lang.Object not found
For example for the class file of the inner class Responses$Authenticate
generated from: https://github.com/v-l-a-d/java-driver/blob/2.1/driver-core/src/main/java/com/datastax/driver/core/Responses.java
the whole result is:
CBMC version 5.4 64-bit x86_64 linux
Parsing com/datastax/driver/core/Responses$Authenticate.class
Java main class: com.datastax.driver.core.Responses$Authenticate
failed to load class `com.datastax.driver.core.Message'
failed to load class `com.datastax.driver.core.Responses'
failed to load class `com.datastax.driver.core.Message$Decoder'
failed to load class `com.datastax.driver.core.Responses$Authenticate$1'
failed to load class `java.lang.StringBuilder'
failed to load class `java.lang.String'
failed to load class `com.datastax.driver.core.Message$Response'
failed to load class `com.datastax.driver.core.Message$Response$Type'
Converting
Symbols:
Symbol......: __CPROVER_malloc_object
Pretty name.:
Module......:
Base name...: __CPROVER_malloc_object
Mode........: C
Type........: void *
Value.......:
Flags.......: lvalue thread_local state_var
Location....:
Symbol......: __CPROVER_rounding_mode
Pretty name.:
Module......:
Base name...: __CPROVER_rounding_mode
Mode........: C
Type........: signed int
Value.......:
Flags.......: lvalue thread_local state_var
Location....:
identifier java::java.lang.Object not found
This is currently tracked in regression test ansi-c/gcc_builtins2.
For the following program
public class NullPointer5
{
void f()
{
Object o = new Object();
if(null == o)
assert false;
assert true;
}
void g()
{
Object o = new Object();
if(o == null)
assert false;
assert true;
}
}
the result of checking --function NullPointer5.g
is ok, while --function NullPointer.f
fails with the above error.
The same error is triggered with --function Inheritance3.f
in
class Inheritance3
{
class A
{
}
class B extends A
{
}
void f()
{
A a = new A();
B b = new B();
if(a == b)
assert false;
assert true;
}
}
I got the following from Madhukar. The input formula has a single satisfying assignment (0). The output formula has also 2^31-1.
Hi,
There seems to be a bug in the simplify_expr code. For the following input formula:
f.a <= 2147483646 && -((signed __CPROVER_bitvector[33])f.a) <= -1 || FALSE && FALSE || f.a <= -1 && -((signed __CPROVER_bitvector[33])f.a) <= 2147483648 || f.a <= 2147483647 && -((signed __CPROVER_bitvector[33])f.a) <= -2147483647 || FALSE && FALSE
I get an output formula (see below) which is not equisatisfiable to the input formula.
output:
!(f.a >= 0) && !(-((signed __CPROVER_bitvector[33])f.a) >= 2147483649) || !(f.a >= 2147483647) && !(-((signed __CPROVER_bitvector[33])f.a) >= 0) || !(-((signed __CPROVER_bitvector[33])f.a) >= -2147483646)
Best regards,
Madhukar
For non-static (in the Java sense) functions, we need to create a valid this
object (with 'non-deterministic or null' members) in the _start function before invoking a method.
We should refuse to use --function with an interface or abstract class methods.
Constants modified by simplify_expr get printed incorrectly by expr2c. Either update #cformat or remove it and use "value" in expr2c.
create pull request for existing patch
syntactic and semantic diffing of goto programs
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.