From a1acecb5d2ef18092c0ffcfc1abf88d717919174 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 20 Nov 2017 07:59:43 +0000 Subject: [PATCH 1/5] Add call to cproverNondetInitialize in nondet-init This is for the user to be able to provide invariants about the objects in the java programs. This can avoid false positives in the detection of violated properties. For instance many classes in the JDK have a field `size` that will always be positive, providing a cproverNondetInitialize method lets CBMC know about that. --- src/java_bytecode/java_object_factory.cpp | 25 +++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 19e944a3ca3..52837e08e8d 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -926,6 +926,8 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( /// Initializes an object tree rooted at `expr`, allocating child objects as /// necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE /// is set, re-initializes already-allocated objects. +/// After initialization calls validation method +/// `expr.cproverNondetInitialize()` if it was provided by the user. /// /// \param assignments: /// The code block to append the new instructions to. @@ -1028,6 +1030,29 @@ void java_object_factoryt::gen_nondet_struct_init( substruct_in_place); } } + + // If .cproverValidate() can be found in the + // symbol table, we add a call: + // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + // expr.cproverValidate(); + // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + const irep_idt validate_method_name = + "java::" + id2string(class_identifier) + ".cproverNondetInitialize:()V"; + + if(const auto func = symbol_table.lookup(validate_method_name)) + { + const code_typet &type = to_code_type(func->type); + if(type.has_this() && type.parameters().size() == 1) + { + code_function_callt fun_call; + fun_call.function() = func->symbol_expr(); + fun_call.arguments().push_back(address_of_exprt(expr)); + assignments.add(fun_call); + } + else + throw "cproverNondetInitialize should be a non-static function"; + } } /// Initializes a primitive-typed or referece-typed object tree rooted at From 54d943d79217bfa024789b3bd584dd57b0330d10 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 20 Nov 2017 08:43:47 +0000 Subject: [PATCH 2/5] Test for the cproverNondetInitialize feature --- .../cbmc-java/NondetInitValidate/Test.class | Bin 0 -> 896 bytes .../cbmc-java/NondetInitValidate/Test.java | 31 ++++++++++++++++++ .../cbmc-java/NondetInitValidate/test.desc | 5 +++ 3 files changed, 36 insertions(+) create mode 100644 regression/cbmc-java/NondetInitValidate/Test.class create mode 100644 regression/cbmc-java/NondetInitValidate/Test.java create mode 100644 regression/cbmc-java/NondetInitValidate/test.desc diff --git a/regression/cbmc-java/NondetInitValidate/Test.class b/regression/cbmc-java/NondetInitValidate/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..0c2962f9b02a95e3de8b741b52a59a14a8a50504 GIT binary patch literal 896 zcmYLGTTc@~7(KJSY`ZMBrIm{T2_g|<0=~HHPH>@g$?g^te+uzI zeDQ@BFA<|jO?<$_pJa^j%+k__o$s63Gv_I-M|p0(n#aHTFPpJ&Gf_uFAUi-l+1QeHNb{b*+33k{ zEG$PhXq<_3b|@rXSy#?8gNq9-{u3B=WZ?SJIh{zOVTV5$)jG<2j3GW)oF4^qg|ZM; zx&X4{N;~%oL5C1H%WjfYuqJ9p5FglZ5Z7dM7-Khf3SCAlI<3||Lpw&9C3cJnmbg0U zs(tsxTj=rkh{wJnq3E=T&R_-gRj6&8T>{$lJvDX$=g6sq{3JxpdsS3~@1PgoAfX+8 zL~=ixq5Z;$nsAJv@6gwdkouvJTK53elg7CdfeWQb$iV=o_NDp>RiS_Bltqyg>xUeD zqIHHzGA=63F~K})ly{3RZZnFfRKG^ayC_CJhLJQy@h@h@A0$VS;&DINxhN|jH= size || x < 0) + return -1; + + assert(data1 != null || data2 == null); + + if (x >= data1.length) { + i = x - data1.length; + assert(i < data2.length); + return data2[i]; + } else { + assert(x < data1.length); + return data1[x]; + } + + } +} diff --git a/regression/cbmc-java/NondetInitValidate/test.desc b/regression/cbmc-java/NondetInitValidate/test.desc new file mode 100644 index 00000000000..aac61dbb85f --- /dev/null +++ b/regression/cbmc-java/NondetInitValidate/test.desc @@ -0,0 +1,5 @@ +CORE +Test.class +--function Test.check +^VERIFICATION SUCCESSFUL$ +-- From bf9a8c2215564048481d8b294ef7096d05a0f6f7 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 20 Nov 2017 10:21:23 +0000 Subject: [PATCH 3/5] Load cproverNondetInitialize with lazy-methods This allows cproverValidate to be loaded even when lazy methods is activated. --- src/java_bytecode/ci_lazy_methods_needed.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/java_bytecode/ci_lazy_methods_needed.cpp b/src/java_bytecode/ci_lazy_methods_needed.cpp index e7ee2cf8510..ee20b8a1d17 100644 --- a/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -34,8 +34,14 @@ bool ci_lazy_methods_neededt::add_needed_class( { if(!needed_classes.insert(class_symbol_name).second) return false; - const irep_idt clinit_name(id2string(class_symbol_name)+".:()V"); + const std::string &class_name_string = id2string(class_symbol_name); + const irep_idt clinit_name(class_name_string + ".:()V"); if(symbol_table.symbols.count(clinit_name)) add_needed_method(clinit_name); + + const irep_idt cprover_validate( + class_name_string + ".cproverNondetInitialize:()V"); + if(symbol_table.symbols.count(cprover_validate)) + add_needed_method(cprover_validate); return true; } From 6d2d6c4a96bc066b924e78ea3e33227a355ad584 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 20 Nov 2017 09:58:28 +0000 Subject: [PATCH 4/5] Test for cproverNondetInitialize with lazy-methods --- regression/cbmc-java/NondetInitValidate/test_lazy.desc | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 regression/cbmc-java/NondetInitValidate/test_lazy.desc diff --git a/regression/cbmc-java/NondetInitValidate/test_lazy.desc b/regression/cbmc-java/NondetInitValidate/test_lazy.desc new file mode 100644 index 00000000000..9ca92cb5696 --- /dev/null +++ b/regression/cbmc-java/NondetInitValidate/test_lazy.desc @@ -0,0 +1,5 @@ +CORE +Test.class +--function Test.check --lazy-methods +^VERIFICATION SUCCESSFUL$ +-- From 4fd14b29d9b049b9b3fb6d44377e49f9a3a75162 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 20 Nov 2017 17:34:26 +0000 Subject: [PATCH 5/5] Adapt cproverNondetInitialize call for static case --- src/java_bytecode/java_object_factory.cpp | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 52837e08e8d..2d443a2e890 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -1043,15 +1043,12 @@ void java_object_factoryt::gen_nondet_struct_init( if(const auto func = symbol_table.lookup(validate_method_name)) { const code_typet &type = to_code_type(func->type); - if(type.has_this() && type.parameters().size() == 1) - { - code_function_callt fun_call; - fun_call.function() = func->symbol_expr(); + code_function_callt fun_call; + fun_call.function() = func->symbol_expr(); + if(type.has_this()) fun_call.arguments().push_back(address_of_exprt(expr)); - assignments.add(fun_call); - } - else - throw "cproverNondetInitialize should be a non-static function"; + + assignments.add(fun_call); } }