From 46849e9d3e3457fb0a9cc5ff4aaab35a621a95bd Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Wed, 9 May 2018 16:36:45 +0100 Subject: [PATCH 1/3] Adding concurrency related methods to CProver.java Specifically: startThread, endThread, atomicBegin, atomicEnd and getCurrentThreadID. --- .../java_bytecode_convert_method.cpp | 5 ++ .../library/src/org/cprover/CProver.java | 47 +++++++++++++++++++ 2 files changed, 52 insertions(+) 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/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) From bc539b5614d55eb6150a70238252b54a6c84bc28 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Tue, 23 Jan 2018 17:05:55 +0000 Subject: [PATCH 2/3] Adds support for concurrency in java programs This commit enables basic support (creation of threads) for concurrency in java programs using the CAV 13 encoding. To this end, new functions haven been introduced 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. The instrumentation process transforms both functions into the appropriate codet's. This mandates the creation of a new variable per thread, '__CPROVER__thread_id' which is used to store the thread ID. A global counter, '__CPROVER__next_thread_id' is used to keep track of thread id's. Calls to 'CProver.getCurrentThreadID:()I' are also instrumented such that the thread ID of the current thread is returned. Note: instrumentation of thread block's is only enabled when the '--java-threading' command line option is specified. --- src/java_bytecode/Makefile | 1 + .../java_bytecode_convert_threadblock.cpp | 363 ++++++++++++++++++ .../java_bytecode_convert_threadblock.h | 15 + src/java_bytecode/java_bytecode_language.cpp | 9 +- 4 files changed, 387 insertions(+), 1 deletion(-) create mode 100644 src/java_bytecode/java_bytecode_convert_threadblock.cpp create mode 100644 src/java_bytecode/java_bytecode_convert_threadblock.h 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_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( From 25e58205232e6663ceada529bd79b6e7bb4f3b21 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Fri, 16 Feb 2018 16:09:32 +0000 Subject: [PATCH 3/3] Java concurrency regression tests --- .../cbmc-java-concurrency/CMakeLists.txt | 3 + regression/cbmc-java-concurrency/Makefile | 32 +++++++++ .../explicit_thread_blocks/A.class | Bin 0 -> 1149 bytes .../explicit_thread_blocks/A.java | 61 ++++++++++++++++++ .../explicit_thread_blocks/test.desc | 7 ++ .../explicit_thread_blocks/test2.desc | 6 ++ 6 files changed, 109 insertions(+) create mode 100644 regression/cbmc-java-concurrency/CMakeLists.txt create mode 100644 regression/cbmc-java-concurrency/Makefile create mode 100644 regression/cbmc-java-concurrency/explicit_thread_blocks/A.class create mode 100644 regression/cbmc-java-concurrency/explicit_thread_blocks/A.java create mode 100644 regression/cbmc-java-concurrency/explicit_thread_blocks/test.desc create mode 100644 regression/cbmc-java-concurrency/explicit_thread_blocks/test2.desc 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 0000000000000000000000000000000000000000..d43adf8fcd6ca7946533a033b606e62c2d714d2d GIT binary patch literal 1149 zcmaiy+fEZv6o&sjop#z`ume~q1r%sOpg;`=kJU&36B1Dqh(_+F?G6m~K&Aun0elI$ z;nHg%5u=IT`w+f}#`w?f0izHuX6@swZ~gz;-+zDp3Sa@VCQJ;*5XF#*Yq%bS;b1vp zVAMneg9g$jG8i*3E+F3UTNCKXIQ6>pe79Duuef!mP?ja0Yzaj2Zq@Z43WO#mUkK>S zwUQKwKXI$_>3*dkz0KgVfL3AX-0+>^>vdk6EldTW6ITS1!IfOuscz?%T1BsVUd>~{O9rwQ zrZFR6pIv)a*p)?}Dr??$uDIvb4y2b`ey&D=j=Jx7{^pJ+9ctDm)&iX|SuM4;;%Awb z%k)X0wd=Jz)l90bH@O!gU#5*)euL)F+6n&@qrV8 zZpMh()ERr)S9h2!xH=y_fz~C~KOtnBt*L&D@F7yi(4t4^;b5Cb==g%jt5X=?g2b9i zoMLLQBAqpvtSHW!5{z@iT;)j!VvdwVo9Z;F(-%`O#U+UAC9aR4By;y8i&P7jC9d}Z z+{*{&h`baxLfj~EY2q@(jS)BgH?FUZD^Q(A*;BTe?^3h@I;y<<52GyC|Ftqp%cc>- z49%P+GKWdrR514N7t%p{lWpGHrkksc{wYuKBM{l1>J5&nVYt!Heh%*%U1fLA>FOw7 z8L-IS-lFc?#NDCpyBNSdzQp@jL0**K%zVP5wSxU`g`c16NLF` XXJSodlg{5F%}kp0DA1N7Si`^{;4H4% literal 0 HcmV?d00001 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