diff --git a/regression/cbmc-java-concurrency/CMakeLists.txt b/regression/cbmc-java-concurrency/CMakeLists.txt new file mode 100644 index 00000000000..afe0ea5761a --- /dev/null +++ b/regression/cbmc-java-concurrency/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "$" +) diff --git a/regression/cbmc-java-concurrency/Makefile b/regression/cbmc-java-concurrency/Makefile new file mode 100644 index 00000000000..e94b327bb43 --- /dev/null +++ b/regression/cbmc-java-concurrency/Makefile @@ -0,0 +1,32 @@ +default: tests.log + +test: + @../test.pl -p -c ../../../src/jbmc/jbmc + +tests.log: ../test.pl + @../test.pl -p -c ../../../src/jbmc/jbmc + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.java" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + $(RM) tests.log + +%.class: %.java ../../src/org.cprover.jar + javac -g -cp ../../src/org.cprover.jar:. $< + +nondet_java_files := $(shell find . -name "Nondet*.java") +nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) + +.PHONY: nondet-class-files +nondet-class-files: $(nondet_class_files) + +.PHONY: clean-nondet-class-files +clean-nondet-class-files: + -rm $(nondet_class_files) diff --git a/regression/cbmc-java-concurrency/explicit_thread_blocks/A.class b/regression/cbmc-java-concurrency/explicit_thread_blocks/A.class new file mode 100644 index 00000000000..d43adf8fcd6 Binary files /dev/null and b/regression/cbmc-java-concurrency/explicit_thread_blocks/A.class differ diff --git a/regression/cbmc-java-concurrency/explicit_thread_blocks/A.java b/regression/cbmc-java-concurrency/explicit_thread_blocks/A.java new file mode 100644 index 00000000000..c3ca69524f3 --- /dev/null +++ b/regression/cbmc-java-concurrency/explicit_thread_blocks/A.java @@ -0,0 +1,61 @@ +import java.lang.Thread; +import org.cprover.CProver; + +public class A +{ + static int x = 0; + + // verification success + public void me() + { + x = 5; + CProver.startThread(333); + x = 10; + CProver.endThread(333); + assert(x == 5 || x == 10); + } + + // verification failed + public void me2() + { + x = 5; + CProver.startThread(333); + x = 10; + CProver.endThread(333); + assert(x == 10); + } + + // Known-bug, thread id mismatch, this should be detected by the conversation + // process. It is currently not and thus will result in an assertion violation + // during symbolic execution. + public void me3() + { + x = 5; + CProver.startThread(22333); + x = 10; + CProver.endThread(333); + assert(x == 10); + } + + // Known-bug, see: https://github.com/diffblue/cbmc/issues/1630 + public void me4() + { + int x2 = 10; + CProver.startThread(22333); + x = x2; + assert(x == 10); + CProver.endThread(333); + } + + // Known-bug, symex cannot handle nested thread-blocks + public void me5() + { + CProver.startThread(333); + x = 5; + CProver.startThread(222); + x = 8; + CProver.endThread(222); + CProver.endThread(333); + assert(x == 5 || x == 0 || x == 8); + } +} diff --git a/regression/cbmc-java-concurrency/explicit_thread_blocks/test.desc b/regression/cbmc-java-concurrency/explicit_thread_blocks/test.desc new file mode 100644 index 00000000000..9dd422bc973 --- /dev/null +++ b/regression/cbmc-java-concurrency/explicit_thread_blocks/test.desc @@ -0,0 +1,7 @@ +CORE +A.class +--function "A.me:()V" --lazy-methods --java-threading + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/regression/cbmc-java-concurrency/explicit_thread_blocks/test2.desc b/regression/cbmc-java-concurrency/explicit_thread_blocks/test2.desc new file mode 100644 index 00000000000..10a64a0e08b --- /dev/null +++ b/regression/cbmc-java-concurrency/explicit_thread_blocks/test2.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function "A.me2:()V" --lazy-methods --java-threading + +^SIGNAL=0$ +^VERIFICATION FAILED diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 13aa8e6c2ca..1dc0f78daca 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -7,6 +7,7 @@ SRC = bytecode_info.cpp \ jar_file.cpp \ java_bytecode_convert_class.cpp \ java_bytecode_convert_method.cpp \ + java_bytecode_convert_threadblock.cpp \ java_bytecode_instrument.cpp \ java_bytecode_internal_additions.cpp \ java_bytecode_language.cpp \ diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index e4f3773b4f5..632c741d629 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2834,6 +2834,11 @@ void java_bytecode_convert_method( "nondetWithNull", "nondetWithoutNull", "notModelled", + "atomicBegin", + "atomicEnd", + "startThread", + "endThread", + "getCurrentThreadID" }; if(std::regex_match( diff --git a/src/java_bytecode/java_bytecode_convert_threadblock.cpp b/src/java_bytecode/java_bytecode_convert_threadblock.cpp new file mode 100644 index 00000000000..13e6c43894d --- /dev/null +++ b/src/java_bytecode/java_bytecode_convert_threadblock.cpp @@ -0,0 +1,363 @@ +/*******************************************************************\ + +Module: Java Convert Thread blocks + +Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com + +\*******************************************************************/ + +#include "java_bytecode_convert_threadblock.h" +#include "expr2java.h" +#include "java_types.h" + +#include +#include +#include +#include +#include + +// Disable linter to allow an std::string constant. +const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id";// NOLINT(*) +const std::string thread_id = CPROVER_PREFIX "_thread_id";// NOLINT(*) + +/// Adds a new symbol to the symbol table if it doesn't exist. Otherwise, +/// returns the existing one. +/// /param name: name of the symbol to be generated +/// /param base_name: base name of the symbol to be generated +/// /param type: type of the symbol to be generated +/// /param value: initial value of the symbol to be generated +/// /param is_thread_local: if true this symbol will be set as thread local +/// /param is_static_lifetime: if true this symbol will be set as static +/// /return returns new or existing symbol. +static symbolt add_or_get_symbol( + symbol_tablet &symbol_table, + const irep_idt &name, + const irep_idt &base_name, + const typet &type, + const exprt &value, + const bool is_thread_local, + const bool is_static_lifetime) +{ + const symbolt* psymbol = nullptr; + namespacet ns(symbol_table); + ns.lookup(name, psymbol); + if(psymbol != nullptr) + return *psymbol; + symbolt new_symbol; + new_symbol.name = name; + new_symbol.pretty_name = name; + new_symbol.base_name = base_name; + new_symbol.type = type; + new_symbol.value = value; + new_symbol.is_lvalue = true; + new_symbol.is_state_var = true; + new_symbol.is_static_lifetime = is_static_lifetime; + new_symbol.is_thread_local = is_thread_local; + new_symbol.mode = ID_java; + symbol_table.add(new_symbol); + return new_symbol; +} + +/// Retrieve the first label identifier. This is used to mark the start of +/// a thread block. +/// /param id: unique thread block identifier +/// /return: fully qualified label identifier +static const std::string get_first_label_id(const std::string &id) +{ + return CPROVER_PREFIX "_THREAD_ENTRY_" + id; +} + +/// Retrieve the second label identifier. This is used to mark the end of +/// a thread block. +/// /param id: unique thread block identifier +/// /return: fully qualified label identifier +static const std::string get_second_label_id(const std::string &id) +{ + return CPROVER_PREFIX "_THREAD_EXIT_" + id; +} + +/// Retrieves a thread block identifier from a function call to +/// CProver.startThread:(I)V or CProver.endThread:(I)V +/// /param code: function call to CProver.startThread or CProver.endThread +/// /return: unique thread block identifier +static const std::string get_thread_block_identifier( + const code_function_callt &f_code) +{ + PRECONDITION(f_code.arguments().size() == 1); + const exprt &expr = f_code.arguments()[0]; + mp_integer lbl_id = binary2integer(expr.op0().get_string(ID_value), false); + return integer2string(lbl_id); +} + +/// Transforms the codet stored in in \p f_code, which is a call to function +/// CProver.startThread:(I)V into a block of code as described by the +/// documentation of function convert_thread_block +/// +/// The resulting code_blockt is stored in the output parameter \p code. +/// +/// \param f_code: function call to CProver.startThread:(I)V +/// \param [out] code: resulting transformation +/// \param symbol_table: a symbol table +static void instrument_start_thread( + const code_function_callt &f_code, + codet &code, + symbol_tablet &symbol_table) +{ + PRECONDITION(f_code.arguments().size() == 1); + + // Create global variable __CPROVER__next_thread_id. Used as a counter + // in-order to to assign ids to new threads. + const symbolt &next_symbol = + add_or_get_symbol( + symbol_table, next_thread_id, next_thread_id, + java_int_type(), + from_integer(0, java_int_type()), false, true); + + // Create thread-local variable __CPROVER__thread_id. Holds the id of + // the thread. + const symbolt ¤t_symbol = + add_or_get_symbol( + symbol_table, thread_id, thread_id, java_int_type(), + from_integer(0, java_int_type()), true, true); + + // Construct appropriate labels. + // Note: java does not have labels so this should be safe. + const std::string &thread_block_id = get_thread_block_identifier(f_code); + const std::string &lbl1 = get_first_label_id(thread_block_id); + const std::string &lbl2 = get_second_label_id(thread_block_id); + + // Instrument the following codet's: + // + // A: codet(id=ID_start_thread, destination=__CPROVER_THREAD_ENTRY_) + // B: codet(id=ID_goto, destination=__CPROVER_THREAD_EXIT_) + // C: codet(id=ID_label, label=__CPROVER_THREAD_ENTRY_) + // C.1: codet(id=ID_atomic_begin) + // D: CPROVER__next_thread_id += 1; + // E: __CPROVER__thread_id = __CPROVER__next_thread_id; + // F: codet(id=ID_atomic_end) + + codet tmp_a(ID_start_thread); + tmp_a.set(ID_destination, lbl1); + code_gotot tmp_b(lbl2); + code_labelt tmp_c(lbl1); + tmp_c.op0() = codet(ID_skip); + + exprt plus(ID_plus, java_int_type()); + plus.copy_to_operands(next_symbol.symbol_expr()); + plus.copy_to_operands(from_integer(1, java_int_type())); + code_assignt tmp_d(next_symbol.symbol_expr(), plus); + code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol.symbol_expr()); + + code_blockt block; + block.add(tmp_a); + block.add(tmp_b); + block.add(tmp_c); + block.add(codet(ID_atomic_begin)); + block.add(tmp_d); + block.add(tmp_e); + block.add(codet(ID_atomic_end)); + block.add_source_location() = f_code.source_location(); + + code = block; +} + +/// Transforms the codet stored in in \p f_code, which is a call to function +/// CProver.endThread:(I)V into a block of code as described by the +/// documentation of the function convert_thread_block. +/// +/// The resulting code_blockt is stored in the output parameter \p code. +/// +/// \param f_code: function call to CProver.endThread:(I)V +/// \param [out] code: resulting transformation +/// \param symbol_table: a symbol table +static void instrument_endThread( + const code_function_callt &f_code, + codet &code, + symbol_tablet symbol_table) +{ + PRECONDITION(f_code.arguments().size() == 1); + + // Build id, used to construct appropriate labels. + // Note: java does not have labels so this should be safe + const std::string &thread_block_id = get_thread_block_identifier(f_code); + const std::string &lbl2 = get_second_label_id(thread_block_id); + + // Instrument the following code: + // + // A: codet(id=ID_end_thread) + // B: codet(id=ID_label,label= __CPROVER_THREAD_EXIT_) + codet tmp_a(ID_end_thread); + code_labelt tmp_b(lbl2); + tmp_b.op0() = codet(ID_skip); + + code_blockt block; + block.add(tmp_a); + block.add(tmp_b); + block.add_source_location() = code.source_location(); + + code = block; +} + +/// Transforms the codet stored in in \p f_code, which is a call to function +/// CProver.getCurrentThreadID:()I into a code_assignt as described by the +/// documentation of the function convert_thread_block. +/// +/// The resulting code_blockt is stored in the output parameter \p code. +/// +/// \param f_code: function call to CProver.getCurrentThreadID:()I +/// \param [out] code: resulting transformation +/// \param symbol_table: a symbol table +static void instrument_getCurrentThreadID( + const code_function_callt &f_code, + codet &code, + symbol_tablet symbol_table) +{ + PRECONDITION(f_code.arguments().size() == 0); + + const symbolt& current_symbol = + add_or_get_symbol(symbol_table, + thread_id, + thread_id, + java_int_type(), + from_integer(0, java_int_type()), + true, true); + + code_assignt code_assign(f_code.lhs(), current_symbol.symbol_expr()); + code_assign.add_source_location() = f_code.source_location(); + + code = code_assign; +} + +/// Iterate through the symbol table to find and appropriately instrument +/// thread-blocks. +/// +/// A thread block is a sequence of codet's surrounded with calls to +/// CProver.startThread:(I)V and CProver.endThread:(I)V. A thread block +/// corresponds to the body of the thread to be created. The only parameter +/// accepted by these functions is an integer used to differentiate between +/// different thread blocks. Function startThread() is transformed into a codet +/// ID_start_thread, which carries a target label in the field 'destination'. +/// Similarly endThread() is transformed into a codet ID_end_thread, which +/// marks the end of the thread body. Both codet's will later be transformed +/// (in goto_convertt) into the goto instructions START_THREAD and END_THREAD. +/// +/// Additionally the variable __CPROVER__thread_id (thread local) will store +/// the ID of the new thread. The new id is obtained by incrementing a global +/// variable __CPROVER__next_thread_id. +/// +/// The ID of the thread is made accessible to the Java program by having calls +/// to the function 'CProver.getCurrentThreadID()I' replaced by the variable +/// __CPROVER__thread_id. We also perform this substitution in here. The +/// substitution that we perform here assumes that calls to +/// getCurrentThreadID() are ONLY made in the RHS of an expression. +/// +/// Example: +/// +/// \code +/// CProver.startThread(333) +/// ... // thread body +/// CProver.endThread(333) +/// \endcode +/// +/// Is transformed into: +/// +/// \code +/// codet(id=ID_start_thread, destination=__CPROVER_THREAD_ENTRY_333) +/// codet(id=ID_goto, destination=__CPROVER_THREAD_EXIT_333) +/// codet(id=ID_label, label=__CPROVER_THREAD_ENTRY_333) +/// codet(id=ID_atomic_begin) +/// __CPROVER__next_thread_id += 1; +/// __CPROVER__thread_id = __CPROVER__next_thread_id; +/// ... // thread body +/// codet(id=ID_end_thread) +/// codet(id=ID_label, label=__CPROVER_THREAD_EXIT_333) +/// \endcode +/// +/// Observe that the semantics of ID_start_thread roughly corresponds to: fork +/// the current thread, continue the execution of the current thread in the +/// next line, and continue the execution of the new thread at the destination +/// field of the codet (__CPROVER_THREAD_ENTRY_333). +/// +/// Note: the current version assumes that a call to startThread(n), where n is +/// an immediate integer, is in the same scope (nesting block) as a call to +/// endThread(n). Some assertion will fail during symex if this is not the case. +/// +/// Note': the ID of the thread is assigned after the thread is created, this +/// creates bogus interleavings. Currently, it's not possible to +/// assign the thread ID before the creation of the thead, due to a bug in +/// symex. See https://github.com/diffblue/cbmc/issues/1630/for more details. +/// +/// \param symbol_table: a symbol table +void convert_threadblock(symbol_tablet &symbol_table) +{ + using instrument_callbackt = + std::function; + using expr_replacement_mapt = + std::unordered_map; + + namespacet ns(symbol_table); + + for(auto entry : symbol_table) + { + expr_replacement_mapt expr_replacement_map; + const symbolt &symbol = entry.second; + + // Look for code_function_callt's (without breaking sharing) + // and insert each one into a replacement map along with an associated + // callback that will handle their instrumentation. + for(auto it = symbol.value.depth_begin(), itend = symbol.value.depth_end(); + it != itend; ++it) + { + instrument_callbackt cb; + + const exprt &expr = *it; + if(expr.id() != ID_code) + continue; + + const codet &code = to_code(expr); + if(code.get_statement() != ID_function_call) + continue; + + const code_function_callt &f_code = to_code_function_call(code); + const std::string &f_name = expr2java(f_code.function(), ns); + if(f_name == "org.cprover.CProver.startThread:(I)V") + cb = std::bind(instrument_start_thread, std::placeholders::_1, + std::placeholders::_2, std::placeholders::_3); + else if(f_name == "org.cprover.CProver.endThread:(I)V") + cb = std::bind(&instrument_endThread, std::placeholders::_1, + std::placeholders::_2, std::placeholders::_3); + else if(f_name == "org.cprover.CProver.getCurrentThreadID:()I") + cb = std::bind(&instrument_getCurrentThreadID, std::placeholders::_1, + std::placeholders::_2, std::placeholders::_3); + + if(cb) + expr_replacement_map.insert({expr, cb}); + } + + if(!expr_replacement_map.empty()) + { + symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first); + // Use expr_replacment_map to look for exprt's that need to be replaced. + // Once found, get a non-const exprt (breaking sharing in the process) and + // call it's associated instrumentation function. + for(auto it = w_symbol.value.depth_begin(), + itend = w_symbol.value.depth_end(); it != itend;) + { + expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it); + if(m_it != expr_replacement_map.end()) + { + codet &code = to_code(it.mutate()); + const code_function_callt &f_code = to_code_function_call(code); + m_it->second(f_code, code, symbol_table); + it.next_sibling_or_parent(); + + expr_replacement_map.erase(m_it); + if(expr_replacement_map.empty()) + break; + } + else + ++it; + } + } + } +} diff --git a/src/java_bytecode/java_bytecode_convert_threadblock.h b/src/java_bytecode/java_bytecode_convert_threadblock.h new file mode 100644 index 00000000000..ef02f92b79e --- /dev/null +++ b/src/java_bytecode/java_bytecode_convert_threadblock.h @@ -0,0 +1,15 @@ +/*******************************************************************\ + +Module: Java Convert Thread blocks + +Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com + +\*******************************************************************/ +#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_THREADBLOCK_H +#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_THREADBLOCK_H + +#include + +void convert_threadblock(symbol_tablet &symbol_table); + +#endif diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 72deab72194..74dc65c008c 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_convert_class.h" #include "java_bytecode_convert_method.h" +#include "java_bytecode_convert_threadblock.h" #include "java_bytecode_internal_additions.h" #include "java_bytecode_instrument.h" #include "java_bytecode_typecheck.h" @@ -749,8 +750,14 @@ bool java_bytecode_languaget::typecheck( get_message_handler()); // now typecheck all - return java_bytecode_typecheck( + bool res = java_bytecode_typecheck( symbol_table, get_message_handler(), string_refinement_enabled); + + // now instrument thread-blocks + if(threading_support) + convert_threadblock(symbol_table); + + return res; } bool java_bytecode_languaget::generate_support_functions( diff --git a/src/java_bytecode/library/src/org/cprover/CProver.java b/src/java_bytecode/library/src/org/cprover/CProver.java index 6aadd228e9e..a040d29f1e5 100644 --- a/src/java_bytecode/library/src/org/cprover/CProver.java +++ b/src/java_bytecode/library/src/org/cprover/CProver.java @@ -4,6 +4,7 @@ public final class CProver { public static boolean enableAssume=true; public static boolean enableNondet=true; + public static boolean enableConcurrency=true; public static boolean nondetBoolean() { @@ -115,6 +116,52 @@ public static T nondetWithoutNull() return null; } + public static void startThread(int id) + { + if(enableConcurrency) + { + throw new RuntimeException( + "Cannot execute program with CProver.startThread()"); + } + } + + public static void endThread(int id) + { + if(enableConcurrency) + { + throw new RuntimeException( + "Cannot execute program with CProver.endThread()"); + } + } + + public static void atomicBegin() + { + if(enableConcurrency) + { + throw new RuntimeException( + "Cannot execute program with CProver.atomicBegin()"); + } + } + + public static void atomicEnd() + { + if(enableConcurrency) + { + throw new RuntimeException( + "Cannot execute program with CProver.atomicEnd()"); + } + } + + public static int getCurrentThreadID() + { + if(enableConcurrency) + { + throw new RuntimeException( + "Cannot execute program with CProver.getCurrentThreadID()"); + } + return 0; + } + public static void assume(boolean condition) { if(enableAssume && !condition)