Adding concurrency to Java #1718

dcattaruzza · 2018-01-10T15:12:04Z

There are two minor fixes found in the course of our work and an an initial set that sets up the code to detect concurrency in java.

thk123

It would be good to have some tests (either regression or unit) that demonstrate the new fixed behaviour. I guess I would expect to see one that uses the new block for dealing with thread starting and the issue with static initaliser order.

Can I request a test-gen pointer bump as well to verify fixing the static initaliser isn't going to reveal some other bugs for us (I can do it if you'd like)

thk123 · 2018-01-10T16:27:15Z

src/goto-programs/goto_convert.cpp

@@ -344,14 +344,49 @@ void goto_convertt::convert_label(

  goto_programt tmp;

-  // magic thread creation label?
+  // magic thread creation label, see ansi-c/library/pthread_lib.c


It would be good if this comment is now understood, to elaborate here on what it means

... and the change should go in a different commit.

thk123 · 2018-01-10T16:27:43Z

src/goto-programs/goto_convert.cpp

+    // E: END_THREAD
+    // Z: SKIP
+
+    thread_started_counter+=1;


Nit: ++thread_started_counter;

thk123 · 2018-01-10T16:28:25Z

src/goto-programs/goto_convert.cpp

+    // Z: SKIP
+
+    thread_started_counter+=1;
+    const std::string &lbl1 = "TS_" +


Could these variable names be given more informative names (what does lbl stand for?)

lbl = label, these variables hold names of the label that the goto instruction is targeting. will name them as following instead label_name_c/z

thk123 · 2018-01-10T16:29:54Z

src/goto-programs/goto_convert.cpp

-    tmp_code.copy_to_operands(code.op0());
-    tmp_code.add_source_location()=code.source_location();
-    convert(tmp_code, tmp);
+    // A: START_THREAD : C


👍 for documenting the GOTO being generated, if you could label it as such and explain what the block does

// Generate GOTO to ... // A: START_THREAD : C // ...

Or consider pulling this generation out into a function that returns a code_blockt which allows you to document it more clearly.

thk123 · 2018-01-10T16:31:30Z

src/java_bytecode/java_bytecode_convert_method.cpp

  const irep_idt &clinit_wrapper_name=
    id2string(classname)+"::clinit_wrapper";
  auto findit=symbol_table.symbols.find(clinit_wrapper_name);
  if(findit!=symbol_table.symbols.end())
    return findit->second.symbol_expr();

-  // Create the wrapper now:
+  // Otherwise, assume that class C extends class C' and implements interfaces


tautschnig · 2018-01-10T17:19:14Z

The commit "Folder build/ ignored" would benefit from a commit-message body that explains the "why?" (my assumption is that people use cmake and follow the readme, which suggests that name).

tautschnig · 2018-01-10T17:23:11Z

Commit message comment no 2: " This commit modifies the way __CPROVER_ASYNC is converted into goto." with "This change is needed to make it possible to make CBMC recognise java
threads."

What went wrong before? Would it be possible to be more specific about the change? The subject has many words with very little info.

tautschnig

I'm with @thk123, tests are really necessary here.

General strategy comment: This PR has four commits, and IMHO solves four different problems. It's overall not too big so reviewing is doable, but some of them would be almost trivial to approve while others might have a longer back-and-forth. The time-to-merge is governed by the slowest of the commits.

tautschnig · 2018-01-10T17:30:11Z

src/goto-programs/goto_convert.cpp

+    // C  SKIP
+    // D: BLOCK
+    // E: END_THREAD
+    // Z: SKIP


I'd really like to understand why this is necessary?

@tautschnig The use of labels starting with a specific prefix (__CPROVER_ASYNC_) is a viable way to insert a goto instruction START_THREAD in the goto program only for C programs. In a Java program you can write labels and goto them, but those labels get removed by the Java compiler, they are not present in the .class file. As a result, this is not a viable way to tell to CBMC where to insert a START_THREAD.

What we instead have done to support both C and Java concurrency is as follow:

In this point of the file, instead of inserting a codet ID_start_thread, we insert the actual goto instructions that will be inserted when ID_start_thread was later parsed (in this file), namely, the pseudocode instructions in the comment above this line.

In Java, we have exported two new functions in the org.cprover.CProver class that enable us to insert the START_THREAD and END_THREAD at precise locations (PR to come next week). We will parse calls to those two methods in the CProver class before the execution reaches goto_convertt, and transform them into codets ID_{start,end}_thread.

We have stored in the codet for ID_start_thread a label to the first instruction of the thread, and goto_convertt::convert_start_thread() uses the standard mechanisms in goto_convertt to resolve label targets to resolve the target of the START_THREAD instruction.

Thanks a lot for the info. Really all of that must go in the source code, whether as comments or additional code.

Can you please clarify why you need the END_THREAD to be specified in the Java code? To me, that seems to be the only reason that you need to make those changes in the transformation?

@tautschnig, previously 'end_thread' , was inserted in the same function where the start_thread instruction was converted into goto (goto_convertt::convert_start_thread). This was viable since, the entire body of the thread was in op0 of the label, and thus the end of a thread is easily determined. Since In java we can not use labels, the only way to determine (in a generic way), where a thread starts and thread ends, is by inserting a some sort of place holder (i.e org.cprover.CProver.startThread() ...... org..cprover.CProver.endThread())

Caveat: As I don't know in sufficient detail how you are doing this in the Java front-end I may be making silly comments.

So you generate and ID_start_thread code in the Java front-end - what about putting a code_blockt into its operand? I believe that block would then nicely capture the end of the thread?

And no, we are not doing the "involved analysis" that Kurt described above. It is not necessary to insert START_THREAD and END_THREAD in the code snippet of my previous commit, but would be necessary if we were to transform <code> (in previous snippet) to an isolated codet to pass around. All we do is to substitute the calls to CProver.{start,end}_thread() with the appropriate goto instructions, and generate the labels of the GOTO instructions for the parent thread using the general label mechanism in goto_convertt.

I really want to see the Java front-end part to this. Constructing codet with labels that look like those a user may have provided is confusing and possibly dangerous. It will also break dump-c.

@tautschnig You need to make the above observation factual, otherwise it's going to be difficult to continue the discussion.

What is confusing in constructing those codet? Please be concrete
What is dangerous about it?
What will break in dump-c?

@tautschnig It seems that you are going over the same thinking process that @Degiorgio and I already went 3 months ago. In order to avoid repeating the same and getting on the same page I propose that we do a telephone call. I will write you a mail.

Phone call scheduled; in the meantime: the labels you are using can legitimately occur in source code. Is it unlikely? Yes, probably. But this risk seems unnecessary to take here. Doing --show-goto-functions or --dump-c will make those labels visible, and thus users may be confused to see something they never put in there in the first place. Running it through dump-c will yield code including those labels, and re-compiling the code will yield new labels in addition to the old ones.

I appreciate that you may have gone through all this, but neither the code nor its comments reflected any of those discussions.

tautschnig · 2018-01-10T17:31:25Z

src/goto-programs/goto_convert.cpp

+      std::to_string(thread_started_counter);
+    thread_started_counter+=1;
+    const std::string &lbl2 = "TS_" +
+      std::to_string(thread_started_counter);


Introducing labels here caters the risk of clashing with labels that the original source code uses. At least use a __CPROVER prefix.

Also might be worth pulling the TS prefix into an ID_ThreadStartLabel so easier to identify and fix and clashes.

tautschnig · 2018-01-10T17:32:44Z

src/ansi-c/expr2c.cpp

@@ -2914,6 +2914,12 @@ std::string expr2ct::convert_code(
  if(statement=="unlock")
    return convert_code_unlock(src, indent);

+  if(statement=="atomic_begin")


Use ID_atomic_begin

tautschnig · 2018-01-10T17:32:55Z

src/ansi-c/expr2c.cpp

+  if(statement=="atomic_begin")
+    return indent_str(indent)+"ATOMIC_BEGIN";
+
+  if(statement=="atomic_end")


Use ID_atomic_end

tautschnig · 2018-01-10T17:34:08Z

src/ansi-c/expr2c.cpp

@@ -2914,6 +2914,12 @@ std::string expr2ct::convert_code(
  if(statement=="unlock")
    return convert_code_unlock(src, indent);

+  if(statement=="atomic_begin")
+    return indent_str(indent)+"ATOMIC_BEGIN";


I'd say the output should be __CPROVER_atomic_begin()

tautschnig · 2018-01-10T17:35:19Z

src/goto-programs/goto_convert.cpp

@@ -344,14 +344,49 @@ void goto_convertt::convert_label(

  goto_programt tmp;

-  // magic thread creation label?
+  // magic thread creation label, see ansi-c/library/pthread_lib.c


... and the change should go in a different commit.

dcattaruzza · 2018-01-11T08:47:37Z

@tautschnig, we have 40+ commits on the back of this for some work we did offline, so we still need to wait for the slowest of these to continue (we should not have been offline so long, but that's a different discussion).
Getting feedback on one PR is faster and less than on several because there is less backand forth, sofor these we will aim for a bit less granularity.

Degiorgio · 2018-01-11T16:30:45Z

The commit "Folder build/ ignored" would benefit from a commit-message body that explains the "why?" (my assumption is that people use cmake and follow the readme, which suggests that name).

@tautschnig your assumption is correct, will modify the comment body to make it clear.

Degiorgio · 2018-01-12T13:53:20Z

@tautschnig @thk123 Regarding unit tests, I will write a unit test for the commit related to static initializers , Regarding the other commit, what kind of tests would you expect to see exactly? The reason I am asking is because this a refactoring-commit, it does not introduce or modify functionality, it is needed to facilitate the support of both C and Java concurrency. Support for the latter will be introduced in future PRs.

tautschnig · 2018-01-12T14:08:19Z

I'm not sure whether the same is true for @thk123, but at least I reviewed this PR commit-by-commit. Thus "Fixes wrong invocation order for static initializers" was the last one, and my comment asking for test was certainly distorted by that one. So: from my point of view, please add tests that document that new/previously wrong behaviour; all other bits are fine as far as testing is concerned.

Degiorgio · 2018-01-14T11:37:51Z

@tautschnig and @thk123 , Latest commit should address most of the issues you raised

tautschnig

The goto conversion should not be introducing artificial labels, but instead be generating goto program instructions directly.

tautschnig · 2018-01-15T09:07:20Z

src/ansi-c/expr2c.cpp

@@ -2914,6 +2914,12 @@ std::string expr2ct::convert_code(
  if(statement=="unlock")
    return convert_code_unlock(src, indent);

+  if(statement==ID_atomic_begin)
+    return indent_str(indent)+"__CPROVER_atomic_begin()";


Needs a ; at the end.

tautschnig · 2018-01-15T09:10:31Z

src/goto-programs/goto_convert.cpp

+  //
+  // note: this technique for using a label as a way
+  // to instrument a thread block is only viable
+  // for C programs (see ansi-c/library/pthread_lib/pthread.c)


No. codet is independent of C and code_labelt could be generated in any front-end.

tautschnig · 2018-01-15T09:14:24Z

src/goto-programs/goto_convert.cpp

@@ -344,14 +344,40 @@ void goto_convertt::convert_label(

  goto_programt tmp;

-  // magic thread creation label?
+  // magic thread creation label.
+  // The "__CPROVER_ASYNC_" signals the start


It's actually the single statement that's labelled in this way that is the new thread. Typically, this statement will be a function call.

can you clarify this comment please? There is nothing preventing you from having something like __CPROVER_ASYNC: statement1, statement2, statement3, ... ;

If you use a comma, then those are expressions, not statements. That is, statement1, statement2, statement3 is a single statement.

tautschnig · 2018-01-15T09:19:53Z

src/goto-programs/goto_convert.cpp

+    // the body of the thread is expected to be
+    // in the operand.
+    INVARIANT(code.op0().is_not_nil(),
+      "op0 in magic thread creation label is null!.");


No punctation (let alone duplicate) at end of message

tautschnig · 2018-01-15T09:23:48Z

src/goto-programs/goto_convert.cpp

+  // these are used to jump in and out of the thread block.
+  ++thread_started_counter;
+  const std::string &label_name_c = "__CPROVER_TS_" +
+    std::to_string(thread_started_counter);


Reference to a temporary.

tautschnig · 2018-01-15T09:25:08Z

src/goto-programs/goto_convert.cpp

+  codet tmp_a(ID_start_thread);
+  tmp_a.set(ID_destination, label_name_c);
+
+  code_gotot tmp_b(label_name_z);


In my opinion you should not be generating code_gotot here, but instead generate goto program instructions. That would make those artificially generated labels unnecessary.

romainbrenguier · 2018-01-15T10:24:13Z

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1038,8 +1054,18 @@ exprt java_bytecode_convert_methodt::get_or_create_clinit_wrapper(
    init_body.move_to_operands(call_base);
  }

+  // call java::C::<clinit>(), if the class has one static initializer
+  const irep_idt &real_clinit_name=id2string(classname)+".<clinit>:()V";
+  auto findsymit=symbol_table.symbols.find(real_clinit_name);


find_sym_it would be more readable

romainbrenguier · 2018-01-15T10:25:08Z

src/java_bytecode/java_bytecode_convert_method.cpp

+  {
+    code_function_callt call_real_init;
+    call_real_init.function()=findsymit->second.symbol_expr();
+    init_body.move_to_operands(call_real_init);


can you use .add instead? I think using the codet specific method is clearer than the generic exprt one

romainbrenguier · 2018-01-15T10:29:41Z

src/goto-programs/goto_convert.cpp

@@ -2242,3 +2243,47 @@ void goto_convert(

  ::goto_convert(to_code(symbol.value), symbol_table, dest, message_handler);
 }
+
+void goto_convertt::generate_thread_block(


This function should be documented

romainbrenguier · 2018-01-15T10:35:00Z

regression/cbmc-java/static_init_order/test.desc

+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$


I think one positive test is not enough to show the feature works. There should be at least one test where an assertion can fail.

romainbrenguier · 2018-01-15T10:37:19Z

regression/cbmc-java/static_init_order/static_init_order.java

+    // of the class in question.
+    if(object2.x == 20)
+        // order of Init:  C.clint, A.clint, B.clint
+        assert(true);


I don't think asserting true is useful.
Actually if we have 2 assert false and jbmc says the first can fail but not the second, I find this more interesting.

Agreed, will address this.

Degiorgio · 2018-01-18T16:08:52Z

@tautschnig latest commit should address the issue you raised, i.e: we are instrumenting goto instructions directly instead of codet. Can you take a look? Thanks!

Degiorgio · 2018-01-19T10:47:25Z

@thk123 . @romainbrenguier latest commit should address most of the issue you raised can you take look a please? Thanks!

thk123

Couple of small non-critical suggestions. However I still have some concern about the thread change. You describe it as a refactor - but my reading of the commit message is that actually changes/enhances the behaviour to work with Java as well as with C? Could a test of it working with Java not be provided?

In-order to facilitate the support of both C and Java concurrency, this commit does the following change:

thk123 · 2018-01-19T11:13:33Z

src/goto-programs/goto_convert.cpp

+  // magic thread creation label.
+  // The "__CPROVER_ASYNC_" signals the start
+  // of a sequence of instructions
+  // that can be executed in parallel, i.e a


Nit: these are really short lines, certainly new thread fits on the same line and would make the comment easier to read.

thk123 · 2018-01-19T11:27:47Z

src/goto-programs/goto_convert.cpp

+/// \param thread_body: sequence of codet's that can be executed
+///   in parallel.
+/// \param [out] dest: resulting goto-instructions.
+void goto_convertt::generate_thread_block(


I would prefer if the preable, body and postamble could be glued together and then returned for the caller to append to the dest - I don't know if this is practical

AFAICT this method is not modifying the state and should either be const or static however, it calls convert which might be neither const nor static so won't block if it ends up being a rabbit hole to fix this.

convert, which calls a bunch of functions is not static or constant :(

thk123 · 2018-01-19T13:38:41Z

src/ansi-c/expr2c.cpp

@@ -2914,6 +2914,12 @@ std::string expr2ct::convert_code(
  if(statement=="unlock")
    return convert_code_unlock(src, indent);

+  if(statement==ID_atomic_begin)
+    return indent_str(indent)+"__CPROVER_atomic_begin();";


Here I think you can use CPROVER_PREFIX as opposed to __CPROVER_

Throughout the file (expr2c.cpp) __CPROVER_ is being used as a prefix, for the sake of consistency I think it is better to stick with __CPROVER_

Good point. Leave it as is, I've created #1758 to clean this up at a later point.

Degiorgio · 2018-01-19T14:06:06Z

@thk123 , this refactoring is necessary step towards adding concurrency support for Java. Subsequent PR's will be adding this support, in which tests for Java will be present.

tautschnig

I believe convert_start_thread is now broken.

tautschnig · 2018-01-19T13:32:07Z

src/goto-programs/goto_convert.cpp

-  }
+  // remember it to do target later
+  targets.gotos.push_back(
+    std::make_pair(start_thread, targets.destructor_stack));


How is this supposed to work?

@tautschnig In the case of C, this function will not be triggered in the case of Java, it will be. (we are still using labels at the java front end, that change is not part of this pr).

Is the code that is set a few statements above just nil, or is it actually meaningful? I don't think it will ever be executed.

@tautschnig code is actually, of type ID_start_thread, with the ID_destination field set. It is used by goto_convertt:finish_gotos to generate the actual target.

Thanks a lot, I should have taken a closer look!

tautschnig · 2018-01-19T13:34:07Z

src/goto-programs/goto_convert.cpp

+  dest.destructive_append(body);
+  dest.destructive_append(postamble);
+}
+


No blank line at end-of-file, please.

thk123 · 2018-01-19T14:51:47Z

@Degiorgio Fair enough - is there a test-gen bump for this PR?

romainbrenguier · 2018-01-19T15:25:10Z

regression/cbmc-java/static_init_order/static_init_order.java

@@ -0,0 +1,51 @@
+public class static_init_order


Java class names usually use CamelCase

romainbrenguier · 2018-01-19T15:28:19Z

src/goto-programs/goto_convert.cpp

-    convert(tmp_code, tmp);
+    // the body of the thread is expected to be
+    // in the operand.
+    INVARIANT(code.op0().is_not_nil(),


can you use code.code() instead of code.op0() ?

romainbrenguier · 2018-01-19T15:28:48Z

src/goto-programs/goto_convert.cpp

+    // replace the magic thread creation label with a
+    // thread block (START_THREAD...END_THREAD).
+    code_blockt thread_body;
+    thread_body.add(to_code(code.op0()));


thread_body.add(code.code());

This is needed due the to the introduction of cmake, which by convention generates build files in a folder named "build"

…rly displayed when the "show-symbol-table" flag is specified.

The current use of labels starting with a specific prefix (__CPROVER_ASYNC_) is a viable way to insert concurrency related goto-instructions in the goto program for C programs. However, in the context of a java program, where labels are removed by the compiler this is not possible. In-order to facilitate the support of both C and Java concurrency, this commit does the following change: In 'goto_convertt::convert_label' instead of inserting a codet(ID_start_thread) we insert the actual goto-instructions that would have previously been generated by 'goto_convertt::convert_start_thread' when 'ID_started_thread' is being parsed.

The Java Virtual Machine Specification, section 5.5, p. 359 defines that the static initializers of both the parent class or interfaces of a given class must be invoked **before** the class initializer of the class. They were previously being invoked in the opposite order. Two Regression tests added to enforce this behaviour.

allredj · 2018-01-22T11:26:10Z

regression/cbmc-java/static_init_order/static_init_order.java

+public class static_init_order
+{
+  // as per the Java Virtual Machine Specification,
+  // section 5.5, p. 35 we expect the static initializer of


Remove p. 35

thk123

TG pointer bump passed

f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327 906aeb3 Merge pull request diffblue#349 from diffblue/owen-jones-diffblue/fix-compilation-for-release 3d8423c Merge pull request diffblue#350 from diffblue/owen-jones-diffblue/skip-duplicate-callsites-in-lazy-methods 73fb488 bugfix from upstream repo for generic crash fd76555 Speed up resolution of virtual callsites in lazy loading 3fd28f3 Replace assert(X) by UNREACHABLE/INVARIANT(X) 557158e Merge pull request diffblue#334 from diffblue/pull-support-20180216 1e48132 Merge from master, 20180216 ad7b28e Updates requsted in the PR: mostly rename 'size -> length'. e3fcb9b Introducing MAX_FILE_NAME_SIZE constant. bb88574 Merge pull request diffblue#1806 from thk123/refactor/address-review-comments-from-1796 db9c214 Merge pull request diffblue#1850 from tautschnig/include-cleanup 78fbf08 Merge pull request diffblue#1844 from smowton/smowton/feature/prepare-symex-for-lazy-loading 4098ed5 Merge pull request diffblue#1849 from smowton/smowton/cleanup/java-main-function-types 06f3e83 Use C++ headers instead of their C variants e918a91 Goto-symex: add support for general function accessor 9e31303 Symex: switch to incrementally populating address-taken locals ac5af68 Address-taken locals analysis: support incremental analysis fe775f3 Merge pull request diffblue#1843 from peterschrammel/instructions-function a6fd729 Cleanup tests with anomalous main functions 5df3fca Clean up get_function_id hacks 552b100 Set function member of each goto instruction in goto program passes 38e6e4a Merge pull request diffblue#1813 from smowton/smowton/fix/cleanup-unused-clinits 278e4e6 Merge pull request diffblue#1826 from smowton/smowton/fix/java-inherited-static-fields a2ebb33 Merge pull request diffblue#1713 from karkhaz/kk-debug-timestamps 7b5dd17 Merge pull request diffblue#1834 from diffblue/library-preconditions 1da5be1 Add tests for inherited static fields 19d622b Add tests to verify that synthetic method removal is performed adc9fd4 Java frontend: clean up unused clinit symbols f15c312 Exclude j.l.O from possible static field hosts. afa443c US spelling of initialize d4d4a9a Tolerate stub static fields defined on non-stub types 873e1f6 Guess public access for stub globals d6783d8 Java method converter: look for inherited static fields 32cc538 Insert stub static globals onto any incomplete ancestor class b2d3d61 Search static fields inherited from interfaces 045ac05 Create stub globals on the first parent incomplete class 5b3cde5 Use a common instance of class_hierarchyt in get_inherited_component e73e756 Create stub globals: check for inherited globals bea6371 Annotate static fields with accessibility 168c2a8 Generalise get_inherited_method f3160e1 resolve_concrete_function_callt -> resolve_inherited_componentt 82549de Emit timestamps on each line of output 3f6965b Replace util/timer* with std::chrono ef08ae2 Merge pull request diffblue#1820 from smowton/smowton/fix/remove-string-solver-iteration-limit 0f20482 Merge pull request diffblue#1836 from karkhaz/kk-remove-unused-lambda-capture e8105bd Merge pull request diffblue#1833 from diffblue/symex_class_cleanup f6f45fc turn some assertions in the stdlib.h models into preconditions 9ea0cc6 pre-conditions for strings fbd54df Remove unused lambda capture 9620802 Merge pull request diffblue#1815 from smowton/smowton/feature/replace-clinit-unwinder 9b59631 Merge pull request diffblue#1828 from smowton/smowton/cleanup/remove-recreate-initialize 1ac9abe Remove string refinement iteration limit c94548c preconditions for delete and delete[] 9ba7fe2 cleanup of some noise (mostly obvious declarators) in the goto_symext class bb64ea6 clean up symex_assign vs. symex_assign_rec 932a38f Merge pull request diffblue#1827 from karkhaz/kk-symex-operator-tidy 968d97e Remove __CPROVER_initialize recreation 06a220a Reimplement remove-static-init-loops to avoid need to inspect GOTO program 2bb98d9 Merge pull request diffblue#1819 from romainbrenguier/refactor/coverage-instrumentation 6492b3a Rearrange cover_basic_blocks header a9549e7 Define constants as const fa35ccd Pull continuation_of_block function out 560d712 Declare constants as const 35422f3 Make update_covered_lines a static function b4cadf8 [path explore 1/8] Tidy up symext top-level funs 0f3ae1a Make representative_inst an optional dc696a4 Make format_number_range function instead of class 678218a Merge pull request diffblue#1825 from thk123/refactor/corrected-path-of-language-file ba76a8f Merge pull request diffblue#1751 from tautschnig/fix-1748 b665269 Correcting path to a file d0889a8 Merge pull request diffblue#1822 from diffblue/legacy-language 441f706 Merge pull request diffblue#1823 from diffblue/cleanup 11714b2 use constant_exprt version of to_integer 733f3b8 remove old-style constructor for member_exprt 63f09ac remove unused function make_next_state 77c8b9c remove translation for certain boolean program constructs 1bac484 cleanout decision_proceduret::in_core d8967f5 moving language.h and language_file.h to langapi folder f9b9599 Merge pull request diffblue#1761 from diffblue/function_typet dd040e5 Added function_typet. bcd88a0 Merge pull request diffblue#1821 from smowton/smowton/feature/test-pl-tags 45f0939 test.pl: add support for tagging test-cases 40b8c03 Updates requested in PR - mainly rename of functions. 7f868e2 Reused private code in 'remove_virtual_functions.cpp' by making it public. ae6775a Merge pull request diffblue#1790 from martin-cs/fix/correct-domain-interface d7bb937 Catch the case when a GOTO instruction is effectively a SKIP. b2fba97 Correct domain transformers so that they meet the preconditions. d447c26 Document the invariants on iterators arguments to transform and merge. e3db794 Whitespace changes to keep clang-format happy. 1990994 Revert "Add edge type parameter to ai transform method" 3ca91bc Revert "Fix iterator comparison bug in reaching_definitions.cpp" ac036fd Revert "Fix iterator equality check bug in dependence_graph.cpp" 86cadcd Revert "Fix iterator equality check bug in custom_bitvector_analysis.cpp" db925de Revert "Fix iterator equality check bug in constant_propagator.cpp" 2c69364 Merge pull request diffblue#1811 from cesaro/iterator-fix 807268e Fixes the symbol_base_tablet iterator 0df054c Merge pull request diffblue#1781 from smowton/smowton/feature/java-create-stub-globals-earlier e163ab6 Java frontend: create synthetic static initialisers for stub globals fbcb423 Merge pull request diffblue#1802 from NathanJPhillips/feature/symbol_iterator e106cf8 Merge pull request diffblue#1793 from smowton/smowton/cleanup/remove-java-new-lowering-pass 52dfc36 Merge pull request diffblue#1731 from diffblue/bugfix/all_resolved_calls f123ae9 Adding comment referencing where the invariant comes from f7c89e1 Add iterator for symbol_table_baset 150f826 Merge pull request diffblue#1801 from hannes-steffenhagen-diffblue/add-idea-gitignore 745afbc Merge pull request diffblue#1796 from thk123/refactor/bytecode-parsing-tidy 6362295 Add .idea (CLion) directory to .gitignore 31da890 Revert "Do lowering of java_new as a function-level pass" 6f6fda7 Merge pull request diffblue#1794 from smowton/smowton/fix/goto-diff-test-escapes 4a538d2 Adding comments on the non-standard patternt 9bfe177 Adding an early guard for correctly parsed exception table 6fe1808 Improved error reporting on invalid constant pool index 93dab4c Escape curly braces in regexes 814cfcc Adapt failing unit test for value set analysis 3ff90bc Add unit test e67a96e Add regression test 3df5348 Adapt regression tests for virtual functions. 09efc90 Re-Resolve function calls if only java.lang.Object was found. a619e48 Merge pull request diffblue#1763 from jeannielynnmoulton/base_class_info_tg1287 0b8dd57 Merge pull request diffblue#1785 from smowton/smowton/fix/core-models-cmake-script 50dcec8 Adding unit tests for extracting generic bases' info 54df3a1 Correcting generic parameters in bases for implicitly generic classes 6d691d7 Parsing generic bases' information into the class symbol 7d041f0 Defining a new type for generic bases f10eb71 Fix Java core-models build script 8d66028 Merge pull request diffblue#1774 from smowton/smowton/feature/java-create-clinit-state-earlier 679d9b8 Java frontend: create static initialiser globals ahead of time 4a93a29 Merge pull request diffblue#1788 from smowton/smowton/fix/java_tcmp_nan 6ad8ffd Fix Java ternary-compare against NaN 1e0ac30 Turn get_may, set_may, etc into irep_ids b0cb1ee Merge pull request diffblue#1766 from smowton/smowton/feature/java-frontend-create-literal-globals-early a2e3af5 Merge pull request diffblue#1744 from smowton/smowton/feature/instrument_cover_per_function 22ae7aa Merge pull request diffblue#1637 from tautschnig/bswap a1a972f Merge pull request diffblue#1776 from smowton/smowton/feature/class-hierarchy-grapht ef3c598 Merge pull request diffblue#1775 from diffblue/refactor/set_classpath 45dd840 Merge pull request diffblue#1728 from romainbrenguier/refactor/split-axiom-vectors 8a27950 Java frontend: create String an Class literals earlier d95cb12 Move string literal initialisation into separate file 515ebdd CI lazy methods: scan global initialisers for global references cab7b52 C front-end: fix promotion order for types ranking lower than int c450328 Support for --16 on Visual Studio, no _WIN64 in 32-bit mode b2c4188 Do not use non-trivial system headers with --32 80b972b Use split_string in set_classpath fdb2ebc Merge pull request diffblue#1773 from smowton/smowton/feature/string-solver-ensure-class-graph-consistency a6eed7c Add class-hierarchy variant based on grapht 311af6d Coverage: fully support instrumenting one function at a time ceafd85 Java string solver: ensure base types are loaded 1e17db6 Merge pull request diffblue#1735 from cesaro/core-models 6844760 Merge pull request diffblue#1769 from smowton/smowton/fix/nondet-initialize-after-initialize a8e659c Fixed CMake linker ODR violations caused by a regression-test f66288b Internalize core models of the Java Class Library 34216f5 Refactor jar loading ed008f9 Add constructors for having memory-loaded jar files This allows the jar_file class to load from a buffer (c array) as opposed to a file 86a34c9 Merge pull request diffblue#1765 from smowton/smowton/fix/ci-lazy-methods-array-element-types 1e11f6d Add test for multiple array types in single method 5009cbb CI lazy methods: re-explore array types with different element types 857fcf9 Cleanup unused fields in string refinement 51d86f5 Adapt unit tests for splitted axiom vectors 1843e44 Split string generator axioms into separate vectors 5669d9b Java: run nondet-initialize method *after* initialization 0b5a5c3 Rename test case 3440018 Provide function name in goto_model_functiont f17e2c8 Merge pull request diffblue#1741 from smowton/smowton/feature/add_failed_symbols_per_function f65f0fd Merge pull request diffblue#1764 from smowton/smowton/feature/java-infer-opaque-type-fields-earlier dbc00a7 Add doxygen to add-failed-symbols 3788467 JBMC: add failed symbols on a per-function basis e934867 Provide a journalling symbol table to process-goto-function e86e2a0 Java: infer opaque type fields before method conversion f0f50e3 Journalling symbol table: enable nesting 58d5980 Merge pull request diffblue#1740 from smowton/smowton/feature/adjust_float_expressions_per_function c91ff69 JBMC: adjust float expressions per function eed983a JBMC: add property checks on a per-function basis db3bc99 JBMC: run convert-nondet on a per-function basis 99ea8fe JBMC: run replace-Java-nondet on function-by-function basis bfd4f50 Merge pull request diffblue#1730 from smowton/smowton/feature/remove_returns_per_function 96569c3 JBMC: remove return values on a per-function basis a7595c1 Remove returns: support running per-function fd6e195 Merge pull request diffblue#1718 from cesaro/concurrency-team-small-fixes e6fe617 Merge pull request diffblue#1705 from jgwilson42/goto-diff-tests 22afc5c Fixes wrong invocation order for static initializers 5c3997d Refectors how CBMC interprets a codet thread-block 001c1a2 ireps of type "ID_atomic_begin" and "ID_atomic_end" will now be properly displayed when the "show-symbol-table" flag is specified. d978ef9 Folder build/ ignored. bc145fd Merge pull request diffblue#1756 from romainbrenguier/tests/index-of-corrections#TG-2246 47b4ee9 Merge pull request diffblue#1725 from cesaro/exception-handlig-fixes d397d6a Merge pull request diffblue#1726 from diffblue/multi_ary_expr2c bd95317 Merge pull request diffblue#1753 from diffblue/xor_exprt 1d4af6d Merge pull request diffblue#1747 from NathanJPhillips/feature/upstream-cleanup 9c7debb Merge pull request diffblue#1750 from pkesseli/feature/sat-interrupt f11c995 Merge pull request diffblue#1749 from pkesseli/ci/remove-unapproved 981c8e0 Merge pull request diffblue#1743 from tautschnig/dump-c-fix bcb076b Correct tests for String.indexOf ef5c6f0 Merge pull request diffblue#1742 from owen-jones-diffblue/owen-jones-diffblue/small-shared-ptr 6c9f05e Fixes to exception handling behaviour 80dd48a added multi-ary xor_exprt 703e4a3 Remove unapproved C++11 header warning. bf7ed1a Merge pull request diffblue#313 from diffblue/owen-jones-diffblue/add-structured-lhs-to-value-set cc9398d Expose MiniSAT's `interrupt()` 8360233 Merge pull request diffblue#1646 from peterschrammel/list-goto-functions e4a2763 Tests for scope changes for variables and functions 8ee1956 goto-diff tests for package name changes ce3a5e9 Basic tests for java goto-diff 3bf9987 Compare access qualifiers in goto-diff f71cc7f Attach class name to method symbol 1f06d35 Merge pull request diffblue#312 from diffblue/pull-support-20180112 fda9daa Cleanup of create-and-swap to emplace e42e97a Merge commit '23666e3af35673c734c9816ffc131b6b9a379e86' into pull-support-20180112 53f1a41 Populate structured_lhs in all `entryt`s d7121f2 dump-c: fix support of use-system-headers eb5ec24 Merge pull request diffblue#1736 from hannes-steffenhagen-diffblue/develop_fix-bitfield-pretty-printing 7a0de46 Add comment suggested by @owen-jones-diffblue b741d4b Use small intrusive pointer in irep 434cc99 Merge pull request diffblue#1732 from peterschrammel/catch-sat-memout 8ae53bb Merge pull request diffblue#1733 from peterschrammel/mem-limit 574101c Add `structured_lhs` field to entryt 4f1a67a Uses alternatives to get_string in type2name when possible b46149d Merge pull request diffblue#1719 from smowton/smowton/cleanup/remove_exceptions_single_global 82a7ec6 Adds regression test for bitfield naming bug 651d8d1 Fixes use of wrong identifier when pretty printing bitfield types 638937a Merge pull request diffblue#1709 from romainbrenguier/doc/string-solver-intro 1d1be4c Move non-string-specific part of doc to solvers 549eb57 Delete trailing whitespaces db3e044 Add introduction to string solver documentation 74be7fb Merge pull request diffblue#1729 from romainbrenguier/refactor/unused-nonempty-option d101b22 Set memory limit utility ef45a1d Replace assertions by invariants 84e04a7 Catch Glucose::OutOfMemoryException 89fc48d Replace assertions by invariants 5e85701 Catch Minisat::OutOfMemoryException b8cee29 Enable list-goto-functions in clobber d902ec8 Replace cout by message stream in show-goto-functions d970673 Move show-loops in the right place in goto-diff e1227ef Enable list-goto-functions in goto diff 7e1110c Enable list-goto-functions in goto-instrument 0fb4868 Enable list-goto-functions in goto-analyzer e67abfa Remove exceptions: switch to single inflight exception global 2fabbd4 Enable list-goto-functions in JBMC 9e1705f Enable list-goto-functions in CBMC ebd8248 Add list-goto-functions command line option 2fe43a9 Add parameter to list goto functions without printing bodies 3d492fe Add documentation of return values 5a8eea5 Remove the string-non-empty option 9810f92 Drop string_non_empty field for string refinement fec16d7 expr2c now distinguishes binary and multi-ary expressions d16a918 C library: network byteorder functions 05bc9ed Implement bswap in SAT back-end 4f37035 Introduce bswap_exprt git-subtree-dir: cbmc git-subtree-split: f7602af

dcattaruzza requested review from cesaro, chrisr-diffblue, kroening, mgudemann, peterschrammel, smowton, tautschnig and thk123 as code owners January 10, 2018 15:12

thk123 reviewed Jan 10, 2018

View reviewed changes

tautschnig reviewed Jan 10, 2018

View reviewed changes

Degiorgio force-pushed the concurrency-team-small-fixes branch 4 times, most recently from 210ca68 to 3dfb831 Compare January 13, 2018 15:30

tautschnig requested changes Jan 15, 2018

View reviewed changes

romainbrenguier reviewed Jan 15, 2018

View reviewed changes

Degiorgio force-pushed the concurrency-team-small-fixes branch 3 times, most recently from 560ca5f to 6822f9c Compare January 17, 2018 23:26

thk123 reviewed Jan 19, 2018

View reviewed changes

Degiorgio force-pushed the concurrency-team-small-fixes branch from 6822f9c to 3bf9f6e Compare January 19, 2018 14:13

tautschnig requested changes Jan 19, 2018

View reviewed changes

Degiorgio force-pushed the concurrency-team-small-fixes branch from 3bf9f6e to 418e193 Compare January 19, 2018 14:56

romainbrenguier reviewed Jan 19, 2018

View reviewed changes

romainbrenguier approved these changes Jan 19, 2018

View reviewed changes

tautschnig approved these changes Jan 19, 2018

View reviewed changes

cesaro and others added 4 commits January 22, 2018 10:39

Folder build/ ignored.

d978ef9

This is needed due the to the introduction of cmake, which by convention generates build files in a folder named "build"

ireps of type "ID_atomic_begin" and "ID_atomic_end" will now be prope…

001c1a2

…rly displayed when the "show-symbol-table" flag is specified.

Degiorgio force-pushed the concurrency-team-small-fixes branch from 418e193 to 22afc5c Compare January 22, 2018 10:39

allredj reviewed Jan 22, 2018

View reviewed changes

thk123 approved these changes Jan 22, 2018

View reviewed changes

thk123 merged commit fd6e195 into diffblue:develop Jan 23, 2018

cesaro deleted the concurrency-team-small-fixes branch May 11, 2018 15:34

Adding concurrency to Java #1718

Adding concurrency to Java #1718

Conversation

dcattaruzza commented Jan 10, 2018

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Jan 10, 2018

tautschnig commented Jan 10, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Jan 12, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cesaro Jan 15, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dcattaruzza commented Jan 11, 2018

Degiorgio commented Jan 11, 2018 • edited Loading

Degiorgio commented Jan 12, 2018 • edited Loading

tautschnig commented Jan 12, 2018

Degiorgio commented Jan 14, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig Jan 15, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio commented Jan 18, 2018

Degiorgio commented Jan 19, 2018

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 Jan 19, 2018 • edited Loading

Choose a reason for hiding this comment

Degiorgio Jan 19, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio commented Jan 19, 2018 • edited Loading

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Jan 19, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Jan 19, 2018 • edited Loading

Degiorgio Jan 12, 2018 •

edited

Loading

cesaro Jan 15, 2018 •

edited

Loading

Degiorgio commented Jan 11, 2018 •

edited

Loading

Degiorgio commented Jan 12, 2018 •

edited

Loading

tautschnig Jan 15, 2018 •

edited

Loading

thk123 Jan 19, 2018 •

edited

Loading

Degiorgio Jan 19, 2018 •

edited

Loading

Degiorgio commented Jan 19, 2018 •

edited

Loading

Degiorgio Jan 19, 2018 •

edited

Loading

Degiorgio Jan 19, 2018 •

edited

Loading