Skip to content

[SEC-179] Add annotations to java_class_typet #1831

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

NathanJPhillips
Copy link
Contributor

Add the annotations parsed from the byte code to classes/fields/methods and static fields (globals) in the symbol table
This could be generally useful, especially in the short term for @allredj's team.

Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

You may consider avoiding maps-of-maps if all you have is a single entry. But just thoughts, you might have very different plans for the data layout.

valuet(irep_idt name, exprt value)
{
id(name);
set(ID_value, value);
Copy link
Collaborator

Choose a reason for hiding this comment

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

I don't know whether you expect these annotations to grow; if you don't, then I'd be more conservative on memory and do class valuet : public exprt with valuet(const irep_idt &name, const exprt &value) : exprt(name) { copy_to_operands(value); }, with const exprt &get_value() { return op0(); }.

{
return static_cast<const exprt &>(find(ID_value));
}
};
Copy link
Collaborator

Choose a reason for hiding this comment

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

I note that java_annotationt has no id() set?!

Copy link
Contributor

Choose a reason for hiding this comment

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

That's in common with many ireps whose ID is implied by its position in the irep graph though, for example struct components.

explicit java_annotationt(const typet &type)
{
set(ID_type, type);
add(ID_values);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Equally, I'd do class java_annotationt : public exprt with get_values() just doing return operands();.

Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

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

Agree with @tautschnig's compaction plan, otherwise lgtm

valuet(irep_idt name, exprt value)
{
id(name);
set(ID_value, value);
Copy link
Contributor

Choose a reason for hiding this comment

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

Ah yes, agreed, make the value an operand rather than named-operand (vector vs. map allocation).

{
return static_cast<const exprt &>(find(ID_value));
}
};
Copy link
Contributor

Choose a reason for hiding this comment

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

That's in common with many ireps whose ID is implied by its position in the irep graph though, for example struct components.

@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch from de8d056 to 7bc32c1 Compare February 14, 2018 17:47
@NathanJPhillips
Copy link
Contributor Author

I've not used exprt as a base since java_annotationt doesn't have operands and java_annotationt::valuet doesn't have a type. Essentially neither of them are actually expressions. But I've gained the equivalent efficiency by implementing the equivalent operations by hand.

@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch from 7bc32c1 to 715f389 Compare February 14, 2018 17:55
std::vector<java_annotationt> &get_annotations()
{
// This cast should be safe as java_annotationt doesn't add data to irept
return reinterpret_cast<std::vector<java_annotationt> &>(
Copy link
Collaborator

Choose a reason for hiding this comment

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

+1 for using reinterpret_cast (and thus something that one can efficiently search for) instead of the C-style cast. Really, we should rid of all of those...

Copy link
Contributor

Choose a reason for hiding this comment

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

This makes me shiver. I'd much prefer a loop/std::transform since this bit shouldn't affect performance (in practice it would be iterated over only once). But at least it's not a c-style cast.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Just curious: how would that work as really you want to return a reference to the same storage?

Copy link
Contributor

@LAJW LAJW left a comment

Choose a reason for hiding this comment

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

Some minor comments. I'm not a fan of reinterpret_cast as performance shouldn't be an issue here. Other than that, it's okay.

get_sub().push_back(value);
}

const irep_idt &get_name()
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 method be const?

return id();
}

const exprt &get_value()
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 method be const?


const exprt &get_value()
{
return static_cast<const exprt &>(get_sub()[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'm not a fan of magic constants. That includes magic index access.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Please suggest alternative code.

Copy link
Collaborator

Choose a reason for hiding this comment

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

@LAJW Would .front() be more adequate?

Copy link
Contributor

Choose a reason for hiding this comment

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

Nope. I'd like an explanation of what the first sub is. Add documentation at the top of the class specifying which ID does what; is there only one; etc. (there's none ATM).

But this is the problem with irept-based classes in general. There are no member variable names, only indices. There's no documentation for indices. In regular classes, even if there's no documentation, you can look at the header and see all members and their types at a glance. Here, the best we can do is just add documentation.

Also, an idea. Use constants named after the intended type: static constexpr size_t FIELD_NAME=0, .... That way at least we'd get variable names.

Copy link
Contributor Author

@NathanJPhillips NathanJPhillips Feb 16, 2018

Choose a reason for hiding this comment

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

He wants this:

      get_sub() = irept::subt(value_id + 1);
      get_sub()[value_id] = value;

Unfortunately this is not a good idea. More unfortunately it's proving difficult to convince him of this.

Copy link
Contributor

Choose a reason for hiding this comment

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

In this warped world of irept it is a goo idea.

Copy link
Contributor

@LAJW LAJW Feb 16, 2018

Choose a reason for hiding this comment

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

Example:

enum {
  key_id,
  value_id,
  member_count
}

subs = vector<...>(member_count);
subs[key_id] = key;
subs[value_id] = value;

get_key() {
  return subs[key_id];
}

get_value() {
  return subs[value_id];
}

That way it would be almost like:

struct {
 string key;
 string value;
 getKey() { return key; }
 getValue() { return value; }
};

What we have now is:

struct {
  string v1;
  string v2;
  getKey() { return v1; }
  getValue() { return v2; }
}

This pattern is scalable to any number of members. Using .front()/push_back() is not and obstructs the structure even more.

Copy link
Contributor

@LAJW LAJW Feb 16, 2018

Choose a reason for hiding this comment

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

Reminds me of this: https://github.com/raxod502/TerrariaClone

Frankly horrifying inline data tables:
static boolean[] solid = {false, true, true, true, true, true, true, ...

Copy link
Contributor

Choose a reason for hiding this comment

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

But I don't care all that much, since I'm not the author, hence my approval.

Copy link
Collaborator

Choose a reason for hiding this comment

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

It might be redundant, but back to basics: there are multiple options for implementing expression trees. One option is to have a class for each kind of expression, with methods and fields specific to each kind of class. Another option is to have one very generic underlying storage and just put an API on top of that for each kind of expression. The latter provides less insight to the compiler (and thus less type checking), but is easier to extend. The former requires dedicated serialisation, deserialisation, hashing, etc. With irept we've got the latter. The ESBMC folks have by now moved over from irept to dedicated, fixed classes. You might check with @lucasccordeiro on the advantages and disadvantages of doing so.

For as long as we stick with irept, the purpose of a class such as the above is to provide a clear API and hide all implementation details (such as the placement of members in the internal storage). While and index 0 might be magic, it is also an information that is very local. The full scope of where one needs to know this fits on a single screen. Have we always got it perfectly right? No, there have been bugs (I do recall c33266a, maybe there have been others). The idea of using an enum instead of a magic number is probably a good one, as long as it doesn't get in the way of keeping the code compact.

set(ID_type, type);
}

const typet &get_type()
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 method be const?

std::vector<java_annotationt> &get_annotations()
{
// This cast should be safe as java_annotationt doesn't add data to irept
return reinterpret_cast<std::vector<java_annotationt> &>(
Copy link
Contributor

Choose a reason for hiding this comment

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

This makes me shiver. I'd much prefer a loop/std::transform since this bit shouldn't affect performance (in practice it would be iterated over only once). But at least it's not a c-style cast.

const java_bytecode_parse_treet::annotationst &parsed_annotations,
std::vector<java_annotationt> &annotations)
{
for(const java_bytecode_convert_classt::annotationt &annotation
Copy link
Contributor

Choose a reason for hiding this comment

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

I'd use auto as the type name is exceptionally verbose (unless the interface is different).

annotation.element_value_pairs.end(),
std::back_inserter(values),
[](
const java_bytecode_convert_classt::annotationt::element_value_pairt
Copy link
Contributor

Choose a reason for hiding this comment

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

You could use const decltype(annotation.element_value_pairs)::value_type &.

class_type.components().push_back(class_typet::componentt());
class_typet::componentt &component=class_type.components().back();
class_type.components().emplace_back();
java_componentt &component =
Copy link
Contributor

Choose a reason for hiding this comment

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

Use auto, since the type is already declared on the right-hand side.

@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch 2 times, most recently from 7d26d8e to 9d4afcc Compare February 19, 2018 17:17
@tautschnig
Copy link
Collaborator

I have restarted the Travis job; assuming this was a transient failure, could someone with sufficient insight please make a call whether this needs approval from test-gen or can be merged straightaway?

@NathanJPhillips
Copy link
Contributor Author

Created test-gen bump https://github.com/diffblue/test-gen/pull/1522

@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch from dadbfdf to 749f119 Compare February 23, 2018 17:41
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.

Passing TG

@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch 3 times, most recently from 0519984 to c11525a Compare February 28, 2018 18:55
@thk123
Copy link
Contributor

thk123 commented Mar 1, 2018

@NathanJPhillips looks like a real compile error here:

/home/travis/build/diffblue/cbmc/src/java_bytecode/java_qualifiers.h:12: undefined reference to `vtable for java_qualifierst'

@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch 2 times, most recently from 9e9328d to 6ede63b Compare March 7, 2018 14:33
@NathanJPhillips
Copy link
Contributor Author

@thk123 indeed - forgot you still need to update Makefile with new files on CBMC.

@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch from 6ede63b to d005b6c Compare March 7, 2018 15:26
@NathanJPhillips
Copy link
Contributor Author

NathanJPhillips commented Mar 9, 2018

Could I get at least one re-review on this one? It changed enough while adding tests that I feel it needs it. In particular the commit "Pretty printing of java_class_typet"

@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch from d005b6c to f27a314 Compare March 9, 2018 18:07
Copy link
Contributor

@smowton smowton 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, if surprisingly involved!

@@ -1,4 +1,3 @@

Copy link
Contributor

Choose a reason for hiding this comment

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

Probably accidental?


java_qualifierst &operator=(const java_qualifierst &other);
java_qualifierst &operator=(java_qualifierst &&other);
virtual c_qualifierst &operator=(const c_qualifierst &other) override;
Copy link
Member

Choose a reason for hiding this comment

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

virtual redundant with override

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 seems like good redundancy from a documentation perspective. Being able to see whether a function is virtual in a single place without having to check the beginning and the end of the declaration is a benefit in my view. As long as it's consistent within a class I think there are examples of both using and not using virtual with override in CBMC. Do you want to make a general policy on this or accept that it's a style issue on which developers can disagree?

Copy link
Collaborator

Choose a reason for hiding this comment

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

If there is a decision to avoid virtual ... override then a7c24fb should be revisited: cpplint.py would happily warn about those, but this had been commented out (by @peterschrammel :-) ). Actually there is more to revisit when it comes to a7c24fb, such as operator spacing...

Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

I believe the introduction of java_qualifierst needs more work. In particular I don't understand the additional assignment and clone operators.

@@ -9,6 +9,27 @@ Author: Daniel Kroening, [email protected]
#include "c_qualifiers.h"

#include <ostream>
#include <util/make_unique.h>

c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why would you even want to do this?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

To implement clone in derived classes we create an instance of the derived object, use this assignment to copy the base class data members to the new instance and then copy the derived class data.

return *this;
}

std::unique_ptr<c_qualifierst> c_qualifierst::clone() const
Copy link
Collaborator

Choose a reason for hiding this comment

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

What is this good for?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Answered on your comment at the call site.

@@ -28,7 +29,13 @@ class c_qualifierst
read(src);
}

void clear()
c_qualifierst(const c_qualifierst &other) = delete;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

To prevent constructing a c_qualifiert from a java_qualifiert and consequently losing data.

@@ -165,7 +165,8 @@ std::string expr2ct::convert_rec(
const c_qualifierst &qualifiers,
const std::string &declarator)
{
c_qualifierst new_qualifiers(qualifiers);
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
c_qualifierst &new_qualifiers = *clone;
Copy link
Collaborator

Choose a reason for hiding this comment

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

?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Not entirely sure what you're asking, so I'll give a full answer, much of which you probably already know.
This code takes the existing qualifiers, adds some more to them and uses them on sub-elements. It doesn't update the qualifiers collection passed in. It therefore needs to make a copy of the qualifiers passed in. The qualifiers are passed by reference to a c_qualifierst but might be of a derived type, such as java_qualifierst. To allow this we need a virtual "copy" function, which is normally called clone. clone has to return by reference/pointer and so normally returns a unique_ptr. The unique pointer defines the scope of the variable to be this function and handles the destruction of the returned object but within this scope and in order to reduce code churn, it is possible to take a reference to the pointed to value and use it in this function.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Thank you very much for the elaboration! Maybe I was aware of most of that, but having it written down helped nonetheless.

I don't think that having expr2ct call functions with a C-specific parameter type is ideal for re-use, but it should be possible to resolve most of that through double dispatch. Let me try to make detailed comments to that effect in the individual places.

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 agree that the type of the parameter to a virtual function intended to be overridden for various languages should be a non-language-specific qualifiers class and I can add such an abstract base class if you like, deriving c_qualifierst from it.

Copy link
Collaborator

Choose a reason for hiding this comment

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

My apologies that I have not actually come back with a double-dispatch solution. I have started working on one, noticed that this was way more work than I had initially thought, and then got dragged into another matter.

Here are my updated thoughts: I concur that there should be a non-language-specific parameter type. Since you can't do a virtual copy constructor, you might anyhow end up with the clone approach that you have already implemented. What I do hope to be avoidable is the dynamic_cast, which would be avoided by calling a virtual member of the parameter. All that is still a bit cumbersome, so you might actually consider implementation qualifiers via irept, which would make it easy to customise and would avoid all the clone/cast games.

Copy link
Collaborator

@tautschnig tautschnig Mar 23, 2018

Choose a reason for hiding this comment

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

Yes, all agreed. Overall it seems pretty painful to me and I am wondering whether you might just want a type_qualifierst that isn't exactly language-agnostic, but instead caters for several languages. For a start you might just put all the extra information that you added to java_qualifierst into c_qualifierst and reduce the size of your patch a fair bit.

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've added 2162f8a, which brings in a base class, though it doesn't do everything we'd like. If you need more than this I'll need some more pointers.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Our comments seem to have crossed. Would you prefer I swap all this out for a single type_qualifiert class now? I can see pros and cons both ways.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I think (but you might convince me otherwise) that a single type_qualifiert class would make the code a lot simpler, yes.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Oh no, it would definitely make the code simpler. But it would add Java specific stuff to a class used by CBMC. Pros and cons...
Does @peterschrammel have an opinion?

@@ -132,7 +132,8 @@ std::string expr2cppt::convert_rec(
const c_qualifierst &qualifiers,
const std::string &declarator)
{
c_qualifierst new_qualifiers(qualifiers);
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
c_qualifierst &new_qualifiers = *clone;
Copy link
Collaborator

Choose a reason for hiding this comment

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

?

void java_qualifierst::write(typet &src) const
{
c_qualifierst::write(src);
auto &annotated_type = static_cast<annotated_typet &>(src);
Copy link
Collaborator

Choose a reason for hiding this comment

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

to_annotated_type

annotated_type.get_annotations() = annotations;
}

c_qualifierst &java_qualifierst::operator+=(const c_qualifierst &c_other)
Copy link
Collaborator

Choose a reason for hiding this comment

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

There should be an operator+= defined with parameter type java_qualifierst. The cast should be unnecessary.

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 an override of the virtual function with this signature on the base class.

return *this;
}

bool java_qualifierst::operator==(const c_qualifierst &c_other) const
Copy link
Collaborator

Choose a reason for hiding this comment

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

Define operator== with parameter type java_qualifierst. No need for a dynamic cast.

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 an override of the virtual function with this signature on the base class.
This is needed to prevent a c_qualifierst comparing equal to a java_qualifierst that has annotations and to consequently to make sure that operator== is commutative.

c_qualifierst::operator==(c_other) && annotations == other->annotations;
}

bool java_qualifierst::is_subset_of(const c_qualifierst &c_other) const
Copy link
Collaborator

Choose a reason for hiding this comment

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

Define it for a parameter type java_qualifierst?

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 an override of the virtual function with this signature on the base class.

@@ -0,0 +1,38 @@
// Copyright 2018 DiffBlue Limited. All Rights Reserved.
Copy link
Collaborator

Choose a reason for hiding this comment

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

See #1919.

@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch 2 times, most recently from f9bc847 to dd99cb3 Compare March 12, 2018 17:34
@NathanJPhillips NathanJPhillips changed the title Add annotations to java_class_typet [SEC-179] Add annotations to java_class_typet Mar 21, 2018
@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch from 9b15b0b to bbc079a Compare March 23, 2018 16:33
@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch from bbc079a to 06f31c5 Compare April 6, 2018 15:28
Add the annotations parsed from the byte code to classes/fields/methods and static fields (globals) in the symbol table
Add type_dynamic_cast and friends for struct_typet, class_typet and java_class_typet
Remove virtual keyword from methods that are specific to this class
Add comment on method that hides a non-virtual base method and remove virtual keyword from it
Mark overrides with override
Added java_qualifierst that adds annotations as qualifiers to types
@NathanJPhillips NathanJPhillips force-pushed the feature/class-annotations branch from 06f31c5 to 9a8d937 Compare April 12, 2018 13:39
Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

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

LGTM, apart from redundant virtual/override

@peterschrammel peterschrammel merged commit d77f6a2 into diffblue:develop Apr 13, 2018
@NathanJPhillips NathanJPhillips deleted the feature/class-annotations branch April 13, 2018 16:02
smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018
ad62682 Merge pull request diffblue#2071 from thk123/refactor/split-string-unit-tests
fc8ba88 Revert to aborting precondition for function inputs
3e2ab6f Merge pull request diffblue#2080 from diffblue/java-bytecode-dependency
6ff1eec cbmc: remove dependency on java_bytecode
0bff19b Merge pull request diffblue#2049 from karkhaz/kk-factor-goto-model-processing
79e3b25 Merge pull request diffblue#2084 from tautschnig/has_subtype-test
cd45b0b Test has_subtype on recursive data types
85ac315 Merge pull request diffblue#2082 from thomasspriggs/default_dstring_hash
28c2e8b Merge pull request diffblue#2065 from tautschnig/be-constructor
afa6023 Merge pull request diffblue#2061 from tautschnig/simplify-extractbits
014d151 Factor out getting & processing goto-model
06b3adc Merge pull request diffblue#2077 from peterschrammel/stable-tmp-var-names
0b3170d Stabilize clinit wrapper function type parameters
3cd8bf4 Temporary vars tests for goto-diff
9f0626c  Prefix temporary var names with function id
ca678aa More permissive regression tests regarding tmp var suffixes
47951ca Merge pull request diffblue#2079 from romainbrenguier/bugfix/has-subtype-recursion
dd73b1a Specify default hash function of `dstringt` to STL.
fe8e589 Avoid infinite recursion in has_subtype
00b9bf6 Merge pull request diffblue#2051 from svorenova/generics_tg2717
cd4bfc3 Merge pull request diffblue#2078 from romainbrenguier/bool-literal-in-while-loop
67ea889 Use bool literal in while loop
d229ad9 Merge pull request diffblue#2056 from diffblue/fix-regression-cbmc-memcpy1
506faf0 Refactor a function for base existence
617d388 Utility functions for generic types
c07e6ca Update generic specialization map when replacing pointers
ed26d0a Merge pull request diffblue#2058 from peterschrammel/stable-disjuncts
b663734 Simplify extractbits(concatenation(...))
b091560 Typing and refactoring of simplify_extractbits
49ad1bd Merge pull request diffblue#974 from tautschnig/fix-assert-encoding
16e9599 Merge pull request diffblue#2063 from tautschnig/has-subtype
950f58b Merge pull request diffblue#2060 from tautschnig/opt-local-map
4222a94 Regression tests for unstable instanceof and virtual method disjuncts
b44589e Make disjuncts in instanceof removal independent of class loading
3afff86 Make disjuncts in virtual method removal independent of class loading
a385d9b Allowed split_string to be used on whitespace if not also trying to strip
fe4a642 Merge pull request diffblue#2062 from tautschnig/no-has-deref
145f474 Adding tests for empty string edge cases
07009d4 Refactored test to run all combinations
252c24c Migrate old string utils unit tests
e87edbf Removing wrong elements from the make file
b165c52 make test work on 32-bit Linux
b804570 Merge pull request diffblue#2048 from JohnDumbell/improvement/adding_null_object_id
61f14d8 Merge pull request diffblue#1962 from owen-jones-diffblue/owen-jones-diffblue/simplify-replace-java-nondet
fdee7e8 Merge pull request diffblue#2059 from tautschnig/generalise-test
4625cc5 Extend global has_subexpr to take a predicate as has_subtype does
e9ebd59 has_subtype(type, pred, ns) to search for contained type matching pred
1f1f67f Merge pull request diffblue#1889 from hannes-steffenhagen-diffblue/develop-feature_generate_function_bodies
048c188 Add unit test for java_replace_nondet
0fe48c9 Make remove_java_nondet work before remove_returns
bcc4dc4 Use byte_extract_exprt constructor
a1814a3 Get rid of thin (and duplicate) has_dereference wrapper
4122a28 Test to demonstrate assert bug on alpine
d44bfd3 Also simplify assert structure found on alpine linux
c5cde18 Do not generate redundant if statements in assert expansions
4fb0603 Make is_skip publicly available and use constant argument
5832ffd Negative numbers should also pass the test
3c23b28 Consistently disable simplify_exprt::local_replace_map
da63652 Merge pull request diffblue#2054 from romainbrenguier/bugfix/clear-equations
d77f6a2 Merge pull request diffblue#1831 from NathanJPhillips/feature/class-annotations
60c8296 Clear string_refinement equations (not dependencies)
314ed53 Correcting the value of ID_null_object
751a882 Factor out default CBMC options to static method
6f24009 Can now test for an option being set in optionst
9a8d937 Add to_annotated_type and enable type_checked_cast for annotated_typet
ca77b4e Add test for added annotations
b06a27d Introduce abstract qualifierst base class
e6fb3bf Pretty printing of java_class_typet
e22b95b Fix spurious virtual function related keywords
3ac6d17 Add type_dynamic_cast and friends for java_class_typet
ce1f4d2 Add annotations to java_class_typet, its methods and fields
f84753d Merge pull request diffblue#2042 from hannes-steffenhagen-diffblue/add_deprecate_macro
7a38669 Merge pull request diffblue#2017 from NathanJPhillips/feature/overlay-classes
75a4aec Revert "the deprecation will need to wait until codebase is clean"
67735b5 Disable deprecation warnings by default
0764f77 Merge pull request diffblue#2036 from romainbrenguier/id_array_list
690b606 Merge pull request diffblue#2039 from peterschrammel/fix-duplicate-msg-json-ui
bba17d9 the deprecation will need to wait until codebase is clean
822c757 Regression test for redundant JSON message output
de0644d Only force end of previous message if there actually is one.
5a637bf Merge pull request diffblue#2037 from hannes-steffenhagen-diffblue/add_deprecate_macro
bff456a Merge pull request diffblue#2040 from tautschnig/remove-swp
87ebe90 Remove vim temp file
228c019 Fix duplicate message output in json-ui
0a2c43e Add DEPRECATED to functions documented as \deprecated
47f4b35 interval_sparse_arrayt constructor from array-list
026c4ca Declare an array_list_exprt class
50a2696 Define ID_array_list
513b67a Merge pull request diffblue#2038 from romainbrenguier/bugfix/assign-at-malloc-site
c207106 Test with array of strings
60183a3 Assign string at malloc site
116fffd Add DEPRECATED macro to mark deprecated functions and variables
7952f2c Add option to generate function body to goto-instrument
3d4183a Add ability to overlay classes with new definitions of existing methods
dbc2f71 Improve code and error message in infer_opaque_type_fields
7c0ea4d Tidied up java_class_loader_limitt

git-subtree-dir: cbmc
git-subtree-split: ad62682
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Aug 20, 2024
We only ever inherit from `c_qualifierst` and can safely avoid the use
of `dynamic_cast` by making `expr2ct` use `c_qualifierst` instead of
`qualifierst`. The `clone()` facility introduced in diffblue#1831 (where
`qualifierst` was introduced) remains in place to support derived
implementations (like `java_qualifierst`).

Also, reduce the number of explicit `c_qualifierst()` calls by making
use of `convert` and `convert_with_identifier`.
@tautschnig tautschnig mentioned this pull request Aug 20, 2024
3 tasks
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Aug 20, 2024
We only ever inherit from `c_qualifierst` and can safely avoid the use
of `dynamic_cast` by making `expr2ct` use `c_qualifierst` instead of
`qualifierst`. The `clone()` facility introduced in diffblue#1831 (where
`qualifierst` was introduced) remains in place to support derived
implementations (like `java_qualifierst`).

Also, reduce the number of explicit `c_qualifierst()` calls by making
use of `convert` and `convert_with_identifier`.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Aug 20, 2024
We only ever inherit from `c_qualifierst` and can safely avoid the use
of `dynamic_cast` by making `expr2ct` use `c_qualifierst` instead of
`qualifierst`. The `clone()` facility introduced in diffblue#1831 (where
`qualifierst` was introduced) remains in place to support derived
implementations (like `java_qualifierst`).

Also, reduce the number of explicit `c_qualifierst()` calls by making
use of `convert` and `convert_with_identifier`.
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.

6 participants