Skip to content

[TG-2365] Parse BootstrapMethods attribute #1804

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged

Conversation

mgudemann
Copy link
Contributor

This is a first step for Java8 lambda support based on invokedynamic. This parses the BootstrapMethods attribute in a class files, verifies that at most one exists and stores the information about referred lambda functions.

This is based on some hypotheses:

  • lambda function invokedynamic will always use LambdaFactory metafactory or altmetafactory for CallSite generation
  • compiled lambda functions start with lambda$ name, followed by new$, static$ or $FunctionName$` and running number

If the above hypotheses are not fulfilled, the entry in lambda_method_handles_map is set to UNKNOWN, no explicit invariants are used here beyond class file format restrictions.

@mgudemann mgudemann self-assigned this Feb 7, 2018
@mgudemann mgudemann force-pushed the feature/parse_bootstrapmethods_attribute branch 2 times, most recently from 014540e to 257e5e2 Compare February 7, 2018 09:18
u2 arg_index2 = read_u2();
u2 arg_index3 = read_u2();

// skip rest
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Clarify in the comment what we lose by ditching this stuff?

real_handle.method_type = pool_entry(arg3.ref1).s;
parsed_class.lambda_method_handle_map[parsed_class.name].push_back(
real_handle);
status()
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is surely debug-level output

}
else
{
// skip arguments here
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Again clarify what we're throwing away

lambda_method_handlet empty_handle;
parsed_class.lambda_method_handle_map[parsed_class.name].push_back(
empty_handle);
// skip arguments here
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same

// where $POSTFIX is $FUN for a function name in which the lambda is define
// "static" when it is a static member of the class
// "new" when it is a class variable, instantiated in <init>
if(has_prefix(id2string(pool_entry(nameandtype_entry.ref1).s), "lambda$"))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

else if.

Also remove linebreaks between end of if and start of else if to clarify that they belong together

handle.handle_type = method_handle_typet::LAMBDA_METHOD_HANDLE;
}

else if(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

else return false ? This can clearly fail; the caller should do something appropriate in that case

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

the handle parameter is initialized with UNKNOWN so if nothing matches this simply stays. Overall probably makes more sense to return an optional method handle, though.

@thk123 thk123 requested a review from majakusber February 8, 2018 10:17
Copy link

@majakusber majakusber left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks good to me, just two minor comments. I was also thinking if a unit test would make sense, to test that the parsed info has the expected form in an example. The regression test here only shows that the attribute is processed.

"only one BootstrapMethods argument is allowed in a class file");

// mark as read in parsed class
parsed_class.read_attribute_bootstrapmethods = true;

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we need to mark it read? According to java specification, there cannot be more than one BootstrapMethods attribute.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it may be worth sanity checking, that we only have one copy of this attribute.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@svorenova this is to validate that this hypothesis holds

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@svorenova the current problem is that this is done in the class loader which is not accessible at the moment.
I agree that a unit test would be good (I had started one but then realized the above) but suggest deferring this to once we now how this information will finally be used and make it accessible in some form then.

@@ -54,6 +54,8 @@ class java_bytecode_parsert:public parsert
method_handle_typet;
typedef java_bytecode_parse_treet::classt::lambda_method_handlest
lambda_method_handlest;

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is renamed in the next line, so should be removed.

u2 num_bootstrap_methods = read_u2();
for(size_t i = 0; i < num_bootstrap_methods; i++)
{
u2 bootstrap_methodhandle_ref = read_u2();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

According to the programming standards, basic words should be separated by _ and abbreviations should be avoided. Therefore bootstrap_methodhandle_ref should be bootstrap_method_handle_reference.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the names were taken from the Java spec: https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.23
So the question is whether to stay consistent with the spec or with general standards. In other parts of our code for parsing bytecode that I've seen, the names follow the Java spec.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we add this link / a reference to the relevant section of the specification in a comment somewhere?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree that names corresponding to specific concepts should match the java spec rather than a strict interpretation of our own naming convention.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am ok with the original java standards naming.


// read method handle pointed to from constant pool entry at index, supports
// reading method handles for bootstrap methods and lambda methods
void java_bytecode_parsert::parse_methodhandle(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should parse_methodhandle be parse_method_handle?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't mind, but just as the cases above, methodhandle is used like this in the JVM class file format spec

// reading method handles for bootstrap methods and lambda methods
void java_bytecode_parsert::parse_methodhandle(
u2 index,
u2 num_bootstrap_arguments,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"num" is an abbreviation which according to the programming standards should be avoided. So, non abbreviated this would be number_bootstrap_arguments, but I think bootstrap_arguments_count might read better.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is ok, as num_bootstrap_arguments is in the java specification.

"reference kind of Methodhandle must be in the range of 1 to 9");

const auto &class_entry = pool_entry(ref_entry.ref1);
const auto &nameandtype_entry = pool_entry(ref_entry.ref2);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nameandtype_entry should be name_and_type_entry

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is ok as it matches the java specification.

{
// skip arguments here
for(size_t i = 0; i < num_bootstrap_arguments; i++)
read_u2();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Although the coding standards states that "Single line blocks without { } are allowed", my preference is that { } is still used for single line blocks. I find that adding the { }, reduces the chance of mistakes when expanding the block to multiple lines later on.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually it may be better to use a call to skip_bytes (or a new skip_u2s) method rather than writing an additional loop each time you want to skip things.

/// for a recognized bootstrap method, for a lambda function or unknown
void java_bytecode_parsert::parse_methodhandle(
const pool_entryt &entry,
lambda_method_handlet &handle)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could handle be the return value instead of an output argument?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok, will change

UNKNOWN_HANDLE
};

struct lambda_method_handlet
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could this be a new class instead of a struct?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

isn't the main difference that struct members are public by default while class members are private ? But yes, no problem to make this a class.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, C++ doesn't make a large differentiation between the struct and class keywords. I am asking for a class to be used with each of the fields accessed through getter and setter methods instead of publicly accessible fields. The production of the debug text on lines 1480-1485, could then be defined as a method instead of inline at the point of building the class.
I know this is a relatively small example of a class to build with getters/setters which feel like boiler plate code. However I think it gives a superior foundation to build on, leading to more compartmentalised code in the end result, instead of large individual files.

const pool_entryt &arg3 = pool_entry(arg_index3);

if(!(arg1.tag == CONSTANT_MethodType &&
arg2.tag == CONSTANT_MethodHandle &&
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we check the tag of arg2 and throw the value away instead of storing for later use?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is just to validate that the format is what we expect a lambda entry to look like

<< id2string(real_handle.lambda_method_name) << " in class \""
<< parsed_class.name << "\""
<< "\n interface type is "
<< id2string(real_handle.interface_type = pool_entry(arg1.ref1).s)
Copy link
Contributor

@thomasspriggs thomasspriggs Feb 8, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why are we performing an assignment in the middle of a status output? Wasn't real_handle.interface_type already assigned to pool_entry(arg1.ref1).s back on line 1476?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

good catch, definitely a copy&paste bug

<< "\n interface type is "
<< id2string(real_handle.interface_type = pool_entry(arg1.ref1).s)
<< "\n method type is "
<< id2string(real_handle.interface_type = pool_entry(arg3.ref1).s)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't real_handle.interface_type = pool_entry(arg3.ref1).s be real_handle.method_type?

{
u2 bootstrap_methodhandle_ref = read_u2();
const pool_entryt &entry = pool_entry(bootstrap_methodhandle_ref);
u2 num_bootstrap_arguments = read_u2();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"num" is an abbreviation, so according to the standards this should be number_bootstrap_arguments, but I think bootstrap_arguments_count would read better.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the naming from the java standards, so it is ok.

{
lambda_method_handlet empty_handle;
parsed_class.lambda_method_handle_map[parsed_class.name].push_back(
empty_handle);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If there are cases where we may need to deal with empty / missing handles, then perhaps the type of the lambda_method_handle_map should be std::map<irep_idt, optionalt<lambda_method_handlest> > instead of std::map<irep_idt, lambda_method_handlest>

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Or perhaps it isn't worth adding them to the map at all?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

best would probably to have a mapping from pairs of class name and entry number to the handle, then a non-existing (or non-parsable) lambda method handle would simply not exist in the map

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Only reviewed first commit so far.

@@ -1381,6 +1403,101 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
{
rRuntimeAnnotation_attribute(parsed_class.annotations);
}
else if(attribute_name == "BootstrapMethods")
{
INVARIANT(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Preferably comment with relevant spec that says this

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Java 8 class file spec §4.4.10

+ id2string(pool_entry(nameandtype_entry.ref2).s);

if(
method_name ==
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Eek! Perhaps we need some kind of interface that specifies whether for a given method name whether it can handle it? Could you add to the PR a summary of how this step is structured:

stores the information about referred lambda functions.

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

mid way through reviewing but have a meeting so thoughts so far (I strongly agree with @svorenova that unit tests would allow much more precise evaulation of whether the parse tree looks like what we want it to)

@@ -1485,6 +1487,8 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
}
else
{
real_handle.interface_type = pool_entry(arg1.ref1).s;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This needs some kind of comment to explain why arg1.ref1 is the interface type!

@@ -0,0 +1,3 @@
interface CustomLambda<T> {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not both? 😛

for(size_t i = 0; i < num_bootstrap_methods; i++)
{
u2 bootstrap_methodhandle_ref = read_u2();
const pool_entryt &entry = pool_entry(bootstrap_methodhandle_ref);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Consider adding invariant that this entry is a CONSTANT_MethodHandle_info?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see this is actually handled in parse_methodhandle

@@ -1381,6 +1390,124 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
{
rRuntimeAnnotation_attribute(parsed_class.annotations);
}
else if(attribute_name == "BootstrapMethods")
{
INVARIANT(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably pull out rBootStrapMethods_attribute method

@@ -1381,6 +1403,101 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
{
rRuntimeAnnotation_attribute(parsed_class.annotations);
}
else if(attribute_name == "BootstrapMethods")
{
INVARIANT(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Java 8 class file spec §4.4.10

status() << "INFO: parse BootstrapMethod handle "
<< num_bootstrap_arguments << " #args"
<< eom;
parse_methodhandle(entry, handle);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not have this return the handle?

{
u2 bootstrap_methodhandle_ref = read_u2();
const pool_entryt &entry = pool_entry(bootstrap_methodhandle_ref);
u2 num_bootstrap_arguments = read_u2();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Rather than reading the arguments below - I'd be tempted to read them all now into an appropriate vector so there's no chance of missing a byte (e.g. if we add more handle_types)

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Got to the bit where we start comparing method_name. Up until the end was looking good, but I think the last view decoding steps are too dense to really follow along even with the spec open next to it.

I also think that we need to design exactly how these different supported times are structured, potentially outside the scope of this PR, which would just read the information into some kind of primitive structure.

const auto &ref_entry = pool_entry(entry.ref2);
INVARIANT(
(entry.ref1 > 0 && entry.ref1 < 10),
"reference kind of Methodhandle must be in the range of 1 to 9");
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps add reference to §5.4.3.5

INVARIANT(
entry.tag == CONSTANT_MethodHandle,
"constant pool entry must be a MethodHandle");
const auto &ref_entry = pool_entry(entry.ref2);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not new code - but I'm a bit confused by this, the spec seems to suggest that a pool entry is a u1 tag followed by an array of u1s dependent on the tag. But our pool_entryt is two u2s, a string, a u8 and an expression. Perhaps should raise a technical debt to have a different class for each pool entry type or at least have the pool_entryt mirror how it looks in the bytecode and have methods that look like:

u1 get_method_handle_reference_kind(const pool_entryt &entry) {
  INVARIANT(entry.get_tag()==CONSTANT_MethodHandle);
  return entry.data[0];
}

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think as a minimum you should introduce that latter method for the new pool_entryt so that is at least obvious that entry.ref2 is the reference_index

(entry.ref1 > 0 && entry.ref1 < 10),
"reference kind of Methodhandle must be in the range of 1 to 9");

const auto &class_entry = pool_entry(ref_entry.ref1);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This bit is kind of complex to follow, suggest mirroring the spec to first create an enum for the different values of the reference_kind:

REF_getField
REF_getStatic
REF_putField
REF_putStatic
REF_invokeVirtual
REF_invokeStatic
REF_invokeSpecial
REF_newInvokeSpecial
REF_invokeInterface

Then switch on these in the same way, breaking into rFieldref_info

I'm pausing here as it has got hard to follow - but the special casing of dealing with which factories we actually support should be abstracted far away from the parse tree IMO (in fact potentially not even part of this PR?)

@thk123
Copy link
Contributor

thk123 commented Feb 9, 2018

For unit tests, can you not do something like:

SCENARIO(
"rclass_attribute",
"[core][java_bytecode][java_bytecode_parse_generics]")
{
  ui_message_handlert message_handler;
  java_bytecode_parse_treet parse_tree;
  java_bytecode_parse("/home/tkiley/workspace/cbmc/regression/cbmc-java/lambda1/Lambdatest.class", parse_tree, message_handler);

  REQUIRE(parse_tree.loading_successful);


  REQUIRE(parse_tree.parsed_class.lambda_method_handle_map.size() > 0);
  // etc.

}

(note this currently fails on the Lambdatest.class - don't know if this is correct (i.e. should there be something in the lambda_method_handle_map) but I think the principle is OK.

I had originally hoped you could test the individual read methods, but of couse you don't know how far through the bytecode you need to go to start reading the class attributes for example. Of course, really nice would be to rather than using real class files, we write subsections of class files that explore all the ways the bytecode for that structure can be. But that is for perhaps another day.


const auto &class_entry = pool_entry(ref_entry.ref1);
const auto &nameandtype_entry = pool_entry(ref_entry.ref2);

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think there should be a double check here that name_and_type_entry.tag is set to CONSTANT_NameAndType

Copy link
Contributor

@thk123 thk123 Feb 15, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe this comment is addressed by mgudemann#1

<< "\n interface type is "
<< id2string(pool_entry(interface_type_argument.ref1).s)
<< "\n method type is "
<< id2string(pool_entry(method_type_argument.ref1).s)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you refactor the generation of this debugging text into a std::string pretty() method of lambda_method_handlet class? I think it would be useful to be able to generate this later whilst debugging lambda functionality, instead of just at the point where the lambda function is parsed.

@thk123
Copy link
Contributor

thk123 commented Feb 14, 2018

@mgudemann I have created mgudemann#1 to address the comments I made, if you like them, I guess you can merge the PR with a rebase and they will appear here?

@thk123
Copy link
Contributor

thk123 commented Feb 15, 2018

As discovered when writing unit tests for this (btw - a strong argument for unit tests 😛 ) - the classt::swap method needs updating as part of this PR

@thk123
Copy link
Contributor

thk123 commented Feb 15, 2018

So I see by removing the special handling in the parse_method_handle I deactivated the code that actually turns the lambdas into the actual function it corresponds to.

That is, we first read a method handle that corresponds to (probably) a lambdafactory method. We then assume the parameters meet a certain criteria that allows us to get a second methodhandle that is referring to the implementation of the lambda.

I had hoped to avoid cluttering the bytecode parsing with the specifics of how lambads work, but since we loose the constants pool we need to do something.

I suggest rather than reusing the lambda_method_handle for both, I introduce another method_handle_infot for the general case, then we have a separate class that takes these, and the constants pool and converts them into a lambda_method_handle to go into the table.

I'll put the first part in an update to mgudemann#1 and carry on with the unit tests. If you'd be able to pull out the bit that starts with // try parsing bootstrap method handle into a separate file then we'll have a good base to build on.

@thk123
Copy link
Contributor

thk123 commented Feb 15, 2018

I've updated mgudemann#1 with the suggested change while leaving the special case handling in java_bytecode_parser.cpp - will now do what I should have been doing and actually write the unit tests!

@mgudemann mgudemann force-pushed the feature/parse_bootstrapmethods_attribute branch from ddbf4f5 to 44b9f07 Compare February 19, 2018 14:01
@mgudemann
Copy link
Contributor Author

@thk123 is there a special reason why you'd like to have the parsing refactored into a separate file? I currently refactored it into its own method in java_bytecode_parsert that is called from rclass_attribute

@thk123
Copy link
Contributor

thk123 commented Feb 19, 2018

@mgudemann Only that it feels like it might expand if/when we support other methods called by invoke_dynamic (and the file is already quite large). I think a similar argument could be made for the structured pool stuff.

@mgudemann
Copy link
Contributor Author

@thk123 ok then I'll split the bootstrapmethods parsing and the structured constant pool stuff into an extra file within the java_bytecode folder. How about a java_lambda_functions file?

@thk123
Copy link
Contributor

thk123 commented Feb 20, 2018

@mgudemann I would put the constants pool stuff into a structured_constant_pool_entries.cpp as I have a vague hope that we can transition to that for all the constants to give us a bit more structure when converting constants.

@mgudemann mgudemann force-pushed the feature/parse_bootstrapmethods_attribute branch from e097cb1 to bf53c54 Compare February 21, 2018 08:25
@mgudemann mgudemann force-pushed the feature/parse_bootstrapmethods_attribute branch from c8bc9cf to 5daf6e1 Compare February 27, 2018 15:52
Copy link

@majakusber majakusber left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good, love the regression/unit tests.

}
else
{
lambda_method_handle->interface_type =
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If parse_method_handle returns an empty optionalt then the code will reach this line and crash due to a failed assertion on .has_value() inside the implementation of the -> operator in optionalt. If we mean to halt execution in this case then we should have a CHECK_RETURN() on the return from parse_method_handle. Assuming of course that we don't have a more elegant way of handling this without halting execution.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like this is now handled ok.

{
lambda_method_handlet lambda_method_handle;
lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE;
lambda_method_handle.u2_values.swap(u2_values);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When I first read this I thought - "Why are we using .swap rather than just assignment with =?" Then I realised that this was an optimisation to avoid having two copies of the data in the vector in memory at once. The C++11 way to do this would be lambda_method_handle.u2_values = std::move(u2_values); I think this makes the intent clearer.

<< " #args" << eom;

// read u2 values of entry into vector
u2_valuest u2_values;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A minor optimisation would be to use u2_valuest u2_values(num_bootstrap_arguments);, so that the vector is created with the correct amount of elements reserved instead of resized as we add them.

@mgudemann mgudemann force-pushed the feature/parse_bootstrapmethods_attribute branch 2 times, most recently from a347a2e to 552c7ae Compare February 27, 2018 16:53
@mgudemann mgudemann force-pushed the feature/parse_bootstrapmethods_attribute branch from 552c7ae to 76d4014 Compare February 27, 2018 17:32
Copy link
Contributor

@thomasspriggs thomasspriggs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, can we get this merged now?

@thk123 thk123 merged commit 5cdfa94 into diffblue:develop Feb 28, 2018
@mgudemann mgudemann deleted the feature/parse_bootstrapmethods_attribute branch February 28, 2018 10:07
smowton pushed a commit to smowton/cbmc that referenced this pull request May 9, 2018
207b801 Merge branch 'develop' into merge_2018-03-26
301cd46 Merge pull request diffblue#1969 from smowton/smowton/cleanup/document_sccs_guarantee
9c04abd Document grapht::SCCs
18478e9 Merge pull request diffblue#1947 from romainbrenguier/dependency-graph/stop-adding-unecessary-constraints#TG-2608
be66b35 Merge pull request diffblue#1961 from danpoe/slice-global-inits-fix
60bfbd0 Reduce string-max-length on String.equals test
50cfe34 Clear constraints at each call to dec_solve
367ca13 Ensure all atomic strings in arguments have node
0bb2fad Define a for_each_atomic_string helper function
805f45f Correct add_constraints in string_dependencies
61b3910 Add length_constraint method to builtin functions
8684e6d Helper functions for length constraints on strings
8a98246 Adapt unit tests for the new interface
c3aed85 Define two helper functions for for_each_successor
a45c64f Add tests for the use of string dependencies
e3da98c Deactivating invariant
2655a9b Rewrite axioms for insert
be5f194 Add double quotes to output_dot
4b342f7 Only add constraints on test function dependencies
3c61cf2 Add a hash function for nodes
23f8cd4 Correct name of builtin function with no eval
c487c4b Generic get_reachable function
46d2507 Add move constructors to builtin_function_nodet
6609247 Add a maybe_testing_function to builtin functions
97ee2d6 Store builtin function pointer inside builtin node
41c0294 Add constraints from the string dependencies
8a7d194 add_constraints method in string_dependencies
b8df2b3 Initialize return_code for all builtin_functions
82f552c Add and add_constraint method to builtin functions
2e7057a Remove use of unknown_dependency
408adbe never return nullptr in to_string_builtin_function
c26b83d Constructor for builtin function with no eval
54a4d7d Add class for builtin function with no eval
8e0f974 Merge pull request diffblue#1970 from tautschnig/java-bytecode-fixes
edb8eeb Merge pull request diffblue#1905 from smowton/smowton/cleanup/broken-regression-tests
c188986 Merge pull request diffblue#1957 from smowton/smowton/cleanup/show-goto-functions-documentation
df1c7e3 Builds require javac as of f66288b
1782e8f Include missing map header
55656ff Include missing invariant header
0b17511 Merge pull request diffblue#1955 from svorenova/bugfix_tg2842
eb1ac7b Merge pull request diffblue#1964 from peterschrammel/documentation/online-docs-link
356a96c Merge pull request diffblue#1953 from smowton/smowton/cleanup/document-java-synthetic-methods
19e5bba Document synthetic methods generated by the Java frontend
706ffa7 Make test lambda1 compatible with symex-driven loading
0759129 Clarify slightly that show-symbol-table et al are restricted to loaded symbols
d7efdd1 Improve docs TOC structure
4043681 Add online documentation to README
076aa5a Improving warnings for unsupported signatures for generics cont.
c63c05b Add unit tests for mocked/unsupported generics cont.
067eeff Refactoring and adding utility functions in require_type
11e9a77 Ignore generic arguments for mocked and unsupported generic classes cont.
3a45ee9 Improving warnings for unsupported signatures for generics
f3cdd97 Add unit tests for mocked/unsupported generics
51a5845 Pull out common generic classes/interfaces for unit tests
fc83526 Ignore generic arguments for mocked and unsupported generic classes
3b00bdc Fix tests with missing EXIT or SIGNAL tests
7b56203 Merge pull request diffblue#1965 from smowton/smowton/fix/reachability-slicer-incompatible-with-symex-driven-loading
5903b62 Merge pull request diffblue#1952 from diffblue/more-builtins
e25a7ac Mark the new reachability-slicer incompatible with symex-driven loading
c5b4e19 Merge pull request diffblue#1963 from tautschnig/dimacs-output
4f3fb8b Merge pull request diffblue#1958 from romainbrenguier/bugfix/insert-offset
cd184f1 Merge pull request diffblue#1780 from Charliemowood/documentation/review-cbmc-docs
1ee0dd9 Merge pull request diffblue#1943 from forejtv/forejtv/reachability-slicer
9aa70a7 Add doc README.md files to each directory
1b7f57d Use doxygen layout file
c22e2e9 Add make doc to Makefile
c50f40d Remove old doxygen module directives from header files
c1f9e34 Move SATABS references to separate from user manual
42f9f36 Improve docs content layout and front page
0afcf90 dimacs: make sure printing a dimacs is fast
a403fdd Fix a bug in slice global inits where guard expressions were disregarded
7e00a30 Merge pull request diffblue#1759 from smowton/smowton/feature/symex-driven-program-loading
22e9b32 Merge pull request diffblue#1960 from smowton/smowton/admin/remove-reuk
f10c697 Remove reuk as a code-owner
c5aa507 Document builtin function constructors
953e2df Enable show-properties with symex-driven lazy loading
6c79494 Fix broken static_init_order test descriptions
ccb2cf3 Fix broken test descriptions
8aa38e7 Add tests for symex-driven lazy loading
7b5d73b JBMC: use symex-driven lazy loading
978ca5b Add callback after symex to bmct
8df9350 Java frontend: rename externally driven loading
98741f9 Java frontend: note availability of synthetic methods
890b8b1 Remove exceptions: add per-function entry point
3ef9ec8 Correct for_each_successor method
aebadee Correct offset in eval for insert
71983b3 Remove mention of size in eval_string
4cca831 Move string_builtin_function class to a new file
6120c17 Changes to the reachability slicer
f6219d4 Merge pull request diffblue#1940 from smowton/smowton/cleanup/remove-virtual-functions
34b2b02 Merge pull request diffblue#1939 from romainbrenguier/bugfix/builtin-string-insert-eval
9d9fafa Merge pull request diffblue#1941 from diffblue/rotate
84186ff Tests for CProverString.append with start/end args
882bbb1 Fix eval of concatenation builtin functions
ad9b86c Fix add_axioms_for_concat_substr
b43bbff Tests for CProverString.substring
4be7532 Test for CProverString.insert
5f96226 Fix string constraints for substring
9ff1e82 Fix eval of insert to match string constraints
f3694af added support for rotation operators
126e90a Remove virtual functions: fix no-fallback-function mode
442f315 Merge pull request diffblue#1951 from zemanlx/support/public-cprover-documentation
8c501cc Use abstract_goto_modelt instead of goto_functionst in bmc reporting phase
760d1ca Lazy goto model: implement abstract_goto_modelt
a4f5d77 goto_modelt: implement abstract_goto_modelt
311ca9c Add abstract_goto_modelt
2fe999c Add gcloud integration to Travis
a5c26a8 Add script for uploading documentation
566539e Add encrypted GCloud key for Travis
07bafd2 move CPROVER built-in functions into the factory
7f3ba30 Merge pull request diffblue#1814 from NlightNFotis/flush-json-stream
7161f17 Merge pull request diffblue#1879 from diffblue/smt2-frontend
ab68848 tests for smt2_solver
246472f an SMT2 solver using boolbv and satcheckt
a75ee3f Add missing langapi dependency to util
d83fa17 Merge pull request diffblue#1932 from romainbrenguier/stop-adding-counter-examples
b5f12ff Correct initial index set computation
c905c2c Remove "Adding counter-examples" message
7085f9c Correct find_index function for `if`-expressions
123be20 Fix goto-diff tests that got broken by streaming json
2ab3b9c Activate JSON streaming when printing goto-traces
54bae24 Refactor huge convert function into multiple ones
a68125c Base JSON UI message handler upon json_streamt
35ac459 Introduce class for streaming JSON to the output
a2a3140 Correct bounds in instantiate method
0910010 Fix string constraints
7586f76 Only add counter examples when index set exhausted
5268c44 a translator from SMT2 into expressions
6dde6b1 add support for let_exprt
37f69b2 added to_mathematical_function_type
7b670cd fix line number counting in SMT2 tokenizer
f3cb5bb Merge pull request diffblue#1938 from romainbrenguier/fix-cmake
213cb57 Fix cmake build
9e11b41 Replace java_int_type by tyep deduced from array
fc67510 Get rid of java_bytecode includes in string solver
461b3a5 Merge pull request diffblue#1922 from romainbrenguier/dependency-graph/get-model#TG-2607
1a874b3 Add name method to builtin functions
8d4a057 Decompose if_expr when adding dependencies
cb72bb7 Correct insert builtin function construction
d0a8868 Constructor and destructor of builtin functions
7bb5aff Make node point to builtin func they result from
a89ceb0 Tests for string solver get with new dependencies
0b3796e Declare a nodet class in string_dependencies
fb676d5 Add a cache for eval in string dependences
095d57b Add concat_char builtin function for strings
44693e8 Use eval of builtin function in get when available
56cb571 Activate dependency computation in string solver
69f31c1 Add eval function to string_dependenciest
357cb44 Add const node_at function in string dependencies
e308bad Rename class to string_dependenciest
06dc6b2 Add an evaluation method to builtin functions
f6a153e Check type before adding dependencies
0139424 Fix linting problem in string_constraint
5108a72 Fix string constraints printing
a2fab10 Linting corrections in string_refinement
05a3426 Merge pull request diffblue#1925 from hannes-steffenhagen-diffblue/testpl_use_env_testpl
8869dd8 Merge pull request diffblue#1920 from diffblue/bugfix/continue_bootstrapmethods_parsing_after_unsupported_entry
d404a55 Merge pull request diffblue#1931 from owen-jones-diffblue/owen-jones-diffblue/fix-release-build-compilation
c6102f7 Merge pull request diffblue#1918 from thk123/tests/tg-2485/lambda-lazy-loading
008de5d Use environment variable for jobs in test.pl
ea6f00f Fixing linter error
0b20a81 Added explanation to the test
1974010 Adjusted the if check to aid readability
42065ec Adjust the interface of the bootstrap methods map
dcd680f Correcting formating on java file
d8edf4f Adjusted test to pass
c0f054a Removing redundant method from test
f494674 Use function that actually contains the lambdas
8615500 Added to readme that the file is compiled using the eclipse compiler
a604b26 !fixup Removed impossible condition (9fc5bfd)
12f049e Added extra information to the warnings to differentaite the different cases
1db68a5 Moved the first condition to after the explanation of our assumptions
c1aa16c Renamed parameter variables
4bb98f0 Removed impossible condition
9749d5a Refactored error reporting method into a seperate function
6400294 Replace nested else ifs with a continue on error conditions
067ccbf Rename j to boostrap_method_index
d7a4e50 Add regression test compiled with ecj
e11163c Continue parsing after unsupported  BootstrapMethods entry
e1961d8 Adding unit tests for verifying the behaviour of lazy methods on lambdas
28c6477 Adding utility for getting symbols out of the symbol table
06ab440 Merge pull request diffblue#1930 from owen-jones-diffblue/owen-jones-diffblue/skip-duplicate-callsites-in-lazy-methods-v1
6eab160 Speed up resolution of virtual callsites in lazy loading v1
c470bdf Replace assert(false) by UNREACHABLE
3af5509 Merge pull request diffblue#1923 from romainbrenguier/author-refinement-util
802b819 Merge pull request diffblue#1926 from tautschnig/fix-json
08ad919 Merge pull request diffblue#1913 from thk123/refactor/lazy-load-java-class-unit-tests
1abbaff Merge pull request diffblue#1927 from peterschrammel/json-xml-timestamps
3864e6c Updating comment with relevant JIRA ticket
72fc31e Add lazy version of load_java_class
5912a04 Refactored java_load_class to allow specifying different cmd line args
9374a1f Remove trailing whitespace from timestamp string
2ae5310 Add timestamp to JSON and XML messages
22b1628 goto-analyzer (un)reachable-functions: build valid json output
1e7f2bc Merge pull request diffblue#1907 from chrisr-diffblue/travis-test-speedups
ee2cf14 Correct author entry
2e7f785 Merge pull request diffblue#1895 from romainbrenguier/dependency-graph#TG-2582
86b3e87 Merge pull request diffblue#1919 from mgudemann/enhancement/fix_diffblue_author
123541f Correct string-max-input-length tests
411e654 Unit tests for dependency graph
c4ba7b4 Separate pointer/function substitutions in solver
a599003 Define function for array_pointer_association
a556d3d Pull out a get_function_name function
859d74c Class for string builtin functions and dependences
bd8ee51 Define function template for output_dot
0b58e31 Move utility functions to string_refinement_util
68ecd9e Make interface of equation_symbol_mappingt clearer
3e688e0 Create string_refinement_util for utility function
e72eacf Pull array_pool class out of constraint generator
42971da Remove default axiom in associate array to pointer
f5adb47 Pull symbol generation out of constraint generator
e2ca928 DiffBlue -> Diffblue
d430ddc Replace copyright notice with author entry
631acab Fix Diffblue author entries
e6e5134 Merge pull request diffblue#1911 from thk123/bugfix/TG-2434/static-constructor-calling-opaque-constructor
1a89e97 Remove lambda in favour of direct construction
bf86af4 Correcting review comments
44153b7 Adding unit tests verifying initalizsers are correctly labelled
80a439d Apply clang-format
6edaaa0 Remove the uncasted member_type so all references use the correct version
e8cbf90 Adding wrappers around whether a code_type is a constructor
e5ff31f Replace checks for <init> with a call to is_constructor
b25301e Remove redundant method and constructor setter
c84cf21 Made member_type_lazy return type match what the method returns
6505e8c Merge pull request diffblue#1875 from peterschrammel/remove-cout-solvers
26ef31c Use invariant instead of abort()
fe40b19 Use invariant instead of printing error message to cerr
066ba51 Merge pull request diffblue#1778 from peterschrammel/java-array-is-object
3548d99 Merge pull request diffblue#1917 from owen-jones-diffblue/owen-jones-diffblue/lazy-methods-do-not-create-stubs-when-resolving-virtual-calls
e7a6769 Merge pull request diffblue#1877 from svorenova/specialized_generics_tg1419
b87661e Do not create stubs when resolving virtual methods
0ac57ba Rename `needed_methods` to `callable_methods`
9fef129 Rename `needed_classes` to `instantiated_classes`
0d524ee Merge pull request diffblue#1893 from diffblue/expression-printer
48024c7 Replace function applications: don't break irep sharing
86bf547 replace_expr: avoid breaking irep sharing
69bef76 Typo in function header
c53cb29 Adding and updating unit tests
a1e9d00 Updating and extending utility functions
2964910 Fix a bug in function for extracting generic interface reference
5c00440 Remove the old way of specializing generics
624cc91 Use the map of parameter-type pairs to specialize generics
3111255 Introduce a map of parameter-type pairs
aaf9477 Use ranged for and const
7018ab4 Clean up commented out code
2529211 Clang-format
f7afe1f Replace assert by invariant
fc44d99 Use invariant instead if printing error message to cout
a15b75f Merge pull request diffblue#1910 from diffblue/builtin-factory
5de436b usage of format() instead of from_expr for debugging
b38ecc3 added format() for exprt and typet
2c8ae92 Makefile: use a variable for all those generated .inc files
17d9897 switch to C++ version of find_pattern
80ee0b1 pass type definitions to the C++ front-end
15ec42f use the builtins factory in the C frontend
1711345 added a factory for builtin function declarations
4a5b952 export all gcc bultin headers
691816b Improve job scheduling when running regression tests with -jN
87526e0 Enable a coarse-grained prallelism when running regression test jobs via Makefiles
76b93e8 Factoring out a private code from module 'remove_virtual_functions.cpp'.
15d7b71 Merge pull request diffblue#1908 from mgudemann/bugfix/fix_bootstrapmethods_empty_optional
0fd6482 Add regression test
5fa3a1a Refactor: improve variable naming
ae276ef Activate two instanceof regression tests
8995fce Java arrays are instanceof Object
881b127 Refactor: use class_typet instead of struct_typet for java class
fdba57c Merge pull request diffblue#1901 from romainbrenguier/fix/quantifier_exprt
782df52 Merge pull request diffblue#1909 from chrisr-diffblue/travis-make-options-cleanup
1edf0e8 Cleanup Travis Makefile build commands
1457849 Merge pull request diffblue#1894 from thomasspriggs/lambdas_compiliers_test
0ed21ca Treat empty optional case separately
3e298ef Formmatting fixes/updates for `java_bytecode_parse_lambda_method_handle` test update.
f1ee826 Update `java_bytecode_parse_lambda_method_handle` tests to run for each java compiler.
fe34bf6 AWS Codebuild: 4th attempt to speed up install
58b4196 AWS Codebuild: 3nd attempt to speed up install
71ab5cd AWS Codebuild: 2nd attempt to speed up install
b95383a Merge branch 'develop' of github.com:diffblue/cbmc into develop
e7bb127 AWS Codebuild: avoid one round of apt-get update
f20e8d7 Merge pull request diffblue#1891 from diffblue/deprecated-exprt-methods
20fc8d1 Merge pull request diffblue#1363 from diffblue/undeclared-return-conflict
92b4873 Merge pull request diffblue#1791 from thk123/feature/make-irep-ids-modifiable-by-all
2fef8fd Merge pull request diffblue#1772 from tautschnig/fix-1771
f6890b3 modernisation of sum_expr and mul_expr
4d87ba1 remove exprt::negate, sum, mul, subtract (deprecated since 2011)
0d0dca4 Merge pull request diffblue#1839 from thomasspriggs/tidy_up1
1b24851 Merge pull request diffblue#1903 from chrisr-diffblue/travis-speedups
b19b4a2 codebuild: enable the tests
44aa443 AWS codebuild: enable ccache
8549ecb AWS codebuild: enable cache
a7cc2a0 Merge pull request diffblue#1885 from tautschnig/use-std-expr
6ef804c Merge pull request diffblue#1888 from tautschnig/linker-script-fixes
d04312f Use std_{code,expr,type} constructors
00ec070 Slightly increase the number of parallel build jobs
f0fc345 Increase ccache size for debug builds
423cd49 Ensure all compile jobs declare their compiler type
7b6f849 Avoid double invoking ccache
a75c4f0 attempt 6 to use AWS Codebuild
d3ebda0 attempt 5 to use AWS Codebuild
a185ae0 fourth attempt to use AWS Codebuild
2948a43 third attempt to use AWS Codebuild
097de57 second attempt to use AWS Codebuild
4331120 first attempt to use AWS Codebuild
5c18ccc Type conflicts on the return value of implicitly declared functions are errors
d074537 test for signature conflict with undeclared function
37a11f9 Merge pull request diffblue#1808 from LAJW/lajw/floating-point-to-java-string
b3f2320 Add unit test for floating_point_to_java_string
7ac4fda Refactor and expose floating point to java conversion in expr2java.h
1a88479 Merge pull request diffblue#1896 from NathanJPhillips/bugfix/erroneous-reference
f5330c9 Correct can_cast_expr for quantifier_exprt
00cc4b1 Merge pull request diffblue#1897 from diffblue/quantifier_exprt
8897709 Merge pull request diffblue#1800 from tautschnig/fix-process_array_expr
fd513a6 added a base class for forall_exprt and exists_exprt
c3ee2a1 Merge pull request diffblue#1010 from danpoe/no-body-inlining
8d8c2e0 Fix bug causing crash on Windows
4dd0f29 Merge pull request diffblue#1892 from diffblue/remove-OPERANDS_IN_GETSUB
b519b41 remove OPERANDS_IN_GETSUB define, which is now simply the only option
80060ea goto-diff is missing dependencies on goto-instrument and goto-symex
7a71c80 Merge pull request diffblue#1884 from mgudemann/enhancement/update_copyright_2018
bb47a84 Merge pull request diffblue#1883 from tautschnig/implement-popcount
90beed4 Merge pull request diffblue#1845 from tautschnig/fix-1837
5cdfa94 Merge pull request diffblue#1804 from mgudemann/feature/parse_bootstrapmethods_attribute
ea7975f Remove unused goto_functions parameters
76d4014 Adding tests for inner classes that capture outer class variables
9b8a73e Adding tests for lambdas as member variables
db1f3b5 Adding tests for local lambdas
ba8b958 Adding tests for static lambdas
ebdcfb1 Adding utiltiy functions required for unit tests
f79e895 Fix format and account for reviewer's comments
51bb367 Merge pull request diffblue#1886 from smowton/smowton/fix/static-inititialisers-doxygen
e0ccb12 Refactor BootstrapMethods attribute reading into function
463ffe1 Refactor parse_method_handle to just deal with the lambda special case
ca5dae4 Fixup Use the strcutured classes to simplify and make more explict the code
b56e42e Fix missing swap for classt
e3ff312 Use the strcutured classes to simplify and make more explict the code
3ac7d09 Introduce classes representing relevant constant pool entries
0e40081 Adding validation on the type of descriptor found
6d44836 Use optionalt<lambda_method_handlet> as return value
f765a0d Rename, some more comments
01dcda5 status()->debug()
603aced Add regression test for lambda functions
e79a655 Initial support for reading BootstrapMethods attribute
b371e28 Linker-scripts: support linker symbols with struct type
e999552 Linker-script processing: mind temporaries
1612f74 Do not modify object_files list while processing it
60487f7 Distribute ls_parse.py with goto-cc
631ea60 Make linker-script processing failures non-fatal
1f753d8 fixup! goto-gcc removes CPROVER macros for native gcc
716103e Implement popcount in SAT back-end
ddde9dc Introduce popcount_exprt
3e793f5 Merge pull request diffblue#1887 from diffblue/string-constant-to-util
683d821 move ansi-c/string_constant.h to util/
3188f10 Merge pull request diffblue#1795 from thk123/bugfix/TG-1358/local-variables
0cfd14b Add missing Doxygen parameter
81d2ea4 Update copyright in help output for {CJ}BM and goto-analyzer
06483f3 Merge pull request diffblue#1881 from tautschnig/fix-runtime-report
3c17453 Merge pull request diffblue#1882 from tautschnig/address_bits
ce600d9 Update copyright in .cpp/.h files
004626c Adding invariant to check instruction is normal wide
60af165 Adding handmade class file exhibiting the same problem
5bdaa64 Adding test demonstrating the too many variables problem
e976d6f Correctly handle wide iload commands
f59092c address_bits need not return an arbitrary-sized integer
3bcb3a5 Fix decision procedure runtime computation
4d33a91 Add missing brackets to multiline if statements.
357bbe4 Fix formatting in assert replacements.
f8c2b09 Replace asserts with new equivalents.
ecbbc73 Remove unused `forall_symbols` macro.
f1670b2 Refactor `forall_symbols` usage into c++11 loop.
a8319a3 Remove unused macro `forall_symbol_module_map`
96bf623 Merge pull request diffblue#1856 from thk123/refactor/fieldref_expr
3819295 Merge pull request diffblue#1797 from thk123/bugfix/TG-1358/long-jumps
7e5922a remove functions without a body
bc2c0cd Inliner fixes
0003d8a Merge pull request diffblue#1864 from owen-jones-diffblue/owen-jones-diffblue/consistent-casts-in-remove-virtual-function
d2e10af Remove the "fieldref" id
2ba794d Introduce fieldref_exprt to represent a field reference
c9f3ea4 Test casts in remove_virtual_function()
9df769a Byte offset to array index translation must use array type
f4fb099 Fix process_array_expr to take into account pointer offset
379705f Process array_equal the same way as array_{replace,copy}
c62b957 Merge pull request diffblue#1551 from tautschnig/perf-test-improvements
1dfb5cd Merge pull request diffblue#1871 from mgudemann/bugfix/superclass_references_for_implicit_generic
71b32f4 Merge pull request diffblue#1777 from romainbrenguier/refactor/java-bytecode-instrument-TG-2331
25eb1a3 Add unit test for implicitly generic super class
590fc2d Make USE_DSTRING conditional and disable it in Ubuntu/Clang/DEBUG Travis job
52290b0 Include string when not using dstringt as irep_idt representation
25ffad4 Do not use dstringt-specific APIs with irep_idt
534f4d2 Include list in expr.h
d87d6e4 Include unordered_map where using a std::unordered_map
a72f52a [TG-2585] Support implicitly generic superclasses
83d9272 Merge pull request diffblue#1870 from diffblue/chrono-precision
2dc9fcd do not round reported durations to seconds
28c3c9f Merge pull request diffblue#853 from owen-jones-diffblue/feature/pointer-function-parameters
ab1b267 Merge pull request diffblue#1832 from diffblue/smt2-backend
11f3699 Merge pull request diffblue#1853 from danpoe/is-threaded-fixes
3e7e840 Merge pull request diffblue#1829 from romainbrenguier/refactor/substitute_array_access#TG-2138
830d519 Merge pull request diffblue#1830 from romainbrenguier/feature/cover-basic-block-java#TG-1404
3a112af Merge pull request diffblue#1846 from hannes-steffenhagen-diffblue/develop-fix_appveyor
9d1e625 Merge pull request diffblue#1641 from karkhaz/kk-big-6-6
7e176f7 Make argument of instrument_code be of type codet
b0df38d Make return type of expr_instrumentation an optional
9c838a1 Documentation improvements in bytecode instrument
ea3ba42 Remove unused includes
f6488d7 Using constant string vector instead of irep_idt
d67fa60 [path explore 7/7] Path exploration documentation
53df567 [path explore 6/7] cpplint & clang-fmt agree on :
e8eec2c [path explore 5/7] Support path-based exploratio2
c88a3ab [path explore 4/7] Factor out common BMC code
d7a70e1 [path explore 3/7] Logical ops for resultt
c53d630 [path explore 2/7] Ignore jbmc binary
6d657a0 Merge pull request diffblue#1779 from diffblue/smt2-integers
63beb71 Update coverage goals in goto-diff test
654418a Unit tests for sparse_arrayt
d65bf9f Class for sparse arrays representations
773721b Refactoring of substitute array access
dc5ffc9 Documentation improvements in string solver
5f54049 Add unit tests for java block instrumentation
105c7e3 Adapt coverage test for new instrumentation
c1045aa Use [] instead of `at` on vector
6811238 cover_block implementation using bytecode location
acf9fe4 Refer to interface rather than cover_basic_blockst
3cd2f0b Put interface to cover_blocks in virtual class
8e7f129 Correct types from unsigned to std::size_t
0fc9c5e Merge pull request diffblue#1866 from romainbrenguier/feature/code-location-in-preprocessing
f270e92 Merge pull request diffblue#1835 from diffblue/remove-goto-templates
d82c586 missing header for std::time_t
fdc5b1e Add source location to code added by preprocessing
0208218 Merge pull request diffblue#1861 from peterschrammel/goto-diff-properties
8192246 Make remove_virtual_function() consistent
9c12abb make linter happy
ba8bbe2 expand goto_programt and goto_functionst templates
b36a90a Merge pull request diffblue#1851 from tautschnig/remove-expr-listt
897e29e Fix CMakeLists to correctly pass test exclusion flags
07e0d58 Merge pull request diffblue#1841 from NathanJPhillips/cleanup/remove-unused-params
4d3ab7a Merge pull request diffblue#1838 from mgudemann/bugfix/catch_unsupported_generics_exception
a8bdb09 Merge pull request diffblue#1817 from allredj/string-primitives-for-exceptions
1ebec11 get values for nondet symbols
a827c77 fix: add missing integer casts and operations
bf9b2c1 Merge pull request diffblue#1862 from diffblue/cbmc-test-results-quantifiers
2b92cd3 Update regression tests to use string primitives
dd5a674 Add jbmc string primitives to CProverString
8f6431c Introduce more string primitives in JBMC
a39fff8 remove iteration count from test result
daab304 remove spurious spaces
482ec4a edit a space
df9aab5 Test for goto-diff show properties
a4d3dc3 Show properties in goto-diff
d3eb1f3 Use CPROVER exit codes
a0e5063 Enable goto check and cover options in goto-diff
a0c45f4 Factor out show properties command line def and docs
937b5f9 Expose conversion of properties of a goto-program into a JSON array
f4a8b0c Replace cout in show_properties
c480d28 Merge pull request diffblue#1842 from NathanJPhillips/feature/depth_iterator_get_mutable
416bbe0 Allow non-const depth_iteratort to be created from a const root
ac37f0b Removed unused parameter/private field
7070296 Add unit test to Makefile
f42eeb2 Add unit test for generic superclass with unsupported signature
e760d6b Catch unsupported generics exception in superclass ref extraction
b0eb45e Merge pull request diffblue#1840 from NathanJPhillips/bugfix/test-name
6f622d1 Fixes for is_threadedt, --is-threaded
13b77d8 Include list where using a std::list and drop forall_expr_list macro
2ccc41b Remove destination directory before trying to move to it in AppVeyor
a094990 Fixed test name
a0bfd42 smt2irep now uses smt2_tokenizert
3587184 added an SMT-LIB2 tokenizer
dea2592 treat real and integer as 'numeric' in C front-end
57ecf15 + is multi-ary in SMT-LIB2
12ae728 fixes for integers in SMT2
698ccdd use a ranged for
bc0ebd3 Bounds checks in fgets, read
dda54c7 Adding test includes a jump to address 2^16
3f202fa Add support for reading nop operations
7a205f0 Correct handling of two byte offsets
cb2c7a8 Adding the irep_ids file to frequently modified low risk files
03095d4 Use svcomp18 as base
f659577 perf-test: build configuration using glucose
98b9ae6 SV-COMP now requires zip files
1c0cf32 Support custom CodeBuild templates
6eeb672 Permit selecting a regular-expression-defined set of tasks
d3b29d2 Update cprover-sv-comp, benchexec to latest version
3269da7 Utility to generate HTML reports from perf-test experiments
cf4eeb2 Move code into code block instead of copying it
7f4a79e Tidy up C symbol factory code
REVERT: f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327

git-subtree-dir: cbmc
git-subtree-split: 207b801
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants