Skip to content

Commit

Permalink
Remove qualifierst
Browse files Browse the repository at this point in the history
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 #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`.
  • Loading branch information
tautschnig committed Aug 20, 2024
1 parent 3877e0f commit eabcf9c
Show file tree
Hide file tree
Showing 9 changed files with 45 additions and 84 deletions.
6 changes: 3 additions & 3 deletions jbmc/src/java_bytecode/expr2java.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -242,11 +242,11 @@ std::string expr2javat::convert_constant(

std::string expr2javat::convert_rec(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,
const std::string &declarator)
{
std::unique_ptr<qualifierst> clone = qualifiers.clone();
qualifierst &new_qualifiers = *clone;
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
c_qualifierst &new_qualifiers = *clone;
new_qualifiers.read(src);

const std::string d = declarator.empty() ? declarator : (" " + declarator);
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/expr2java.h
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ class expr2javat:public expr2ct

virtual std::string convert_rec(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,
const std::string &declarator) override;

// length of string representation of Java Char
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_qualifiers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other)
return *this;
}

std::unique_ptr<qualifierst> java_qualifierst::clone() const
std::unique_ptr<c_qualifierst> java_qualifierst::clone() const
{
auto other = std::make_unique<java_qualifierst>(ns);
*other = *this;
Expand Down
12 changes: 6 additions & 6 deletions jbmc/src/java_bytecode/java_qualifiers.h
Original file line number Diff line number Diff line change
Expand Up @@ -23,20 +23,20 @@ class java_qualifierst : public c_qualifierst
protected:
java_qualifierst &operator=(const java_qualifierst &other);
public:
virtual std::unique_ptr<qualifierst> clone() const override;
std::unique_ptr<c_qualifierst> clone() const override;

java_qualifierst &operator+=(const java_qualifierst &other);

const std::vector<java_annotationt> &get_annotations() const
{
return annotations;
}
virtual std::size_t count() const override;
std::size_t count() const override;

virtual void clear() override;
void clear() override;

virtual void read(const typet &src) override;
virtual void write(typet &src) const override;
void read(const typet &src) override;
void write(typet &src) const override;

bool is_subset_of(const java_qualifierst &other) const;
bool operator==(const java_qualifierst &other) const;
Expand All @@ -45,7 +45,7 @@ class java_qualifierst : public c_qualifierst
return !(*this == other);
}

virtual std::string as_string() const override;
std::string as_string() const override;
};

#endif // CPROVER_JAVA_BYTECODE_JAVA_QUALIFIERS_H
10 changes: 2 additions & 8 deletions src/ansi-c/c_qualifiers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -24,11 +24,11 @@ c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other)
return *this;
}

std::unique_ptr<qualifierst> c_qualifierst::clone() const
std::unique_ptr<c_qualifierst> c_qualifierst::clone() const
{
auto other = std::make_unique<c_qualifierst>();
*other = *this;
return std::move(other);
return other;
}

std::string c_qualifierst::as_string() const
Expand Down Expand Up @@ -151,9 +151,3 @@ void c_qualifierst::clear(typet &dest)
dest.remove(ID_C_nodiscard);
dest.remove(ID_C_noreturn);
}

/// pretty-print the qualifiers
std::ostream &operator<<(std::ostream &out, const qualifierst &qualifiers)
{
return out << qualifiers.as_string();
}
49 changes: 9 additions & 40 deletions src/ansi-c/c_qualifiers.h
Original file line number Diff line number Diff line change
Expand Up @@ -10,45 +10,12 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_ANSI_C_C_QUALIFIERS_H
#define CPROVER_ANSI_C_C_QUALIFIERS_H

#include <iosfwd>
#include <memory>
#include <string>

class typet;

class qualifierst
{
protected:
// Only derived classes can construct
qualifierst() = default;

public:
// Copy/move construction/assignment is deleted here and in derived classes
qualifierst(const qualifierst &) = delete;
qualifierst(qualifierst &&) = delete;
qualifierst &operator=(const qualifierst &) = delete;
qualifierst &operator=(qualifierst &&) = delete;

// Destruction is virtual
virtual ~qualifierst() = default;

public:
virtual std::unique_ptr<qualifierst> clone() const = 0;

virtual std::size_t count() const = 0;

virtual void clear() = 0;

virtual void read(const typet &src) = 0;
virtual void write(typet &src) const = 0;

// String conversion
virtual std::string as_string() const = 0;
friend std::ostream &operator<<(std::ostream &, const qualifierst &);
};


class c_qualifierst : public qualifierst
class c_qualifierst
{
public:
c_qualifierst()
Expand All @@ -62,12 +29,14 @@ class c_qualifierst : public qualifierst
read(src);
}

virtual ~c_qualifierst() = default;

protected:
c_qualifierst &operator=(const c_qualifierst &other);
public:
virtual std::unique_ptr<qualifierst> clone() const override;
virtual std::unique_ptr<c_qualifierst> clone() const;

virtual void clear() override
virtual void clear()
{
is_constant=false;
is_volatile=false;
Expand All @@ -91,9 +60,9 @@ class c_qualifierst : public qualifierst

// will likely add alignment here as well

virtual std::string as_string() const override;
virtual void read(const typet &src) override;
virtual void write(typet &src) const override;
virtual std::string as_string() const;
virtual void read(const typet &src);
virtual void write(typet &src) const;

Check warning on line 65 in src/ansi-c/c_qualifiers.h

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/c_qualifiers.h#L63-L65

Added lines #L63 - L65 were not covered by tests

static void clear(typet &dest);

Expand Down Expand Up @@ -141,7 +110,7 @@ class c_qualifierst : public qualifierst
return *this;
}

virtual std::size_t count() const override
virtual std::size_t count() const

Check warning on line 113 in src/ansi-c/c_qualifiers.h

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/c_qualifiers.h#L113

Added line #L113 was not covered by tests
{
return is_constant + is_volatile + is_restricted + is_atomic + is_ptr32 +
is_ptr64 + is_nodiscard + is_noreturn;
Expand Down
24 changes: 11 additions & 13 deletions src/ansi-c/expr2c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -213,16 +213,16 @@ void expr2ct::get_shorthands(const exprt &expr)

std::string expr2ct::convert(const typet &src)
{
return convert_rec(src, c_qualifierst(), "");
return convert_with_identifier(src, "");
}

std::string expr2ct::convert_rec(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,
const std::string &declarator)
{
std::unique_ptr<qualifierst> clone = qualifiers.clone();
c_qualifierst &new_qualifiers = dynamic_cast<c_qualifierst &>(*clone);
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
c_qualifierst &new_qualifiers = *clone;
new_qualifiers.read(src);

std::string q=new_qualifiers.as_string();
Expand Down Expand Up @@ -379,7 +379,7 @@ std::string expr2ct::convert_rec(
for(const auto &c : union_type.components())
{
dest += ' ';
dest += convert_rec(c.type(), c_qualifierst(), id2string(c.get_name()));
dest += convert_with_identifier(c.type(), id2string(c.get_name()));
dest += ';';
}

Expand Down Expand Up @@ -538,7 +538,7 @@ std::string expr2ct::convert_rec(
{
std::string arg_declarator=
convert(symbol_exprt(it->get_identifier(), it->type()));
dest+=convert_rec(it->type(), c_qualifierst(), arg_declarator);
dest += convert_with_identifier(it->type(), arg_declarator);
}
}

Expand Down Expand Up @@ -692,10 +692,8 @@ std::string expr2ct::convert_struct_type(
}

dest+=' ';
dest+=convert_rec(
component.type(),
c_qualifierst(),
id2string(component.get_name()));
dest += convert_with_identifier(
component.type(), id2string(component.get_name()));
dest+=';';
}

Expand All @@ -715,7 +713,7 @@ std::string expr2ct::convert_struct_type(
/// \return A C-like type declaration of an array
std::string expr2ct::convert_array_type(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,

Check warning on line 716 in src/ansi-c/expr2c.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/expr2c.cpp#L716

Added line #L716 was not covered by tests
const std::string &declarator_str)
{
return convert_array_type(
Expand All @@ -732,7 +730,7 @@ std::string expr2ct::convert_array_type(
/// \return A C-like type declaration of an array
std::string expr2ct::convert_array_type(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,

Check warning on line 733 in src/ansi-c/expr2c.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/expr2c.cpp#L733

Added line #L733 was not covered by tests
const std::string &declarator_str,
bool inc_size_if_possible)
{
Expand Down Expand Up @@ -2850,7 +2848,7 @@ expr2ct::convert_code_frontend_decl(const codet &src, unsigned indent)
dest+="inline ";
}

dest+=convert_rec(src.op0().type(), c_qualifierst(), declarator);
dest += convert_with_identifier(src.op0().type(), declarator);

if(src.operands().size()==2)
dest+="="+convert(src.op1());
Expand Down
8 changes: 4 additions & 4 deletions src/ansi-c/expr2c_class.h
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ Author: Daniel Kroening, [email protected]
#include <util/std_code.h>

class annotated_pointer_constant_exprt;
class qualifierst;
class c_qualifierst;
class namespacet;
class r_or_w_ok_exprt;
class pointer_in_range_exprt;
Expand Down Expand Up @@ -57,7 +57,7 @@ class expr2ct

virtual std::string convert_rec(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,
const std::string &declarator);

virtual std::string convert_struct_type(
Expand All @@ -74,12 +74,12 @@ class expr2ct

virtual std::string convert_array_type(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,
const std::string &declarator_str);

std::string convert_array_type(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,
const std::string &declarator_str,
bool inc_size_if_possible);

Expand Down
16 changes: 8 additions & 8 deletions src/cpp/expr2cpp.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ class expr2cppt:public expr2ct

std::string convert_rec(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,
const std::string &declarator) override;
};

Expand Down Expand Up @@ -130,11 +130,11 @@ std::string expr2cppt::convert_constant(

std::string expr2cppt::convert_rec(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,
const std::string &declarator)
{
std::unique_ptr<qualifierst> clone = qualifiers.clone();
qualifierst &new_qualifiers = *clone;
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
c_qualifierst &new_qualifiers = *clone;
new_qualifiers.read(src);

const std::string d = declarator.empty() ? declarator : (" " + declarator);
Expand Down Expand Up @@ -274,15 +274,15 @@ std::string expr2cppt::convert_rec(
typet member;
member.swap(tmp.add(ID_to_member));

std::string dest="("+convert_rec(member, c_qualifierst(), "")+":: *)";
std::string dest = "(" + convert(member) + ":: *)";

Check warning on line 277 in src/cpp/expr2cpp.cpp

View check run for this annotation

Codecov / codecov/patch

src/cpp/expr2cpp.cpp#L277

Added line #L277 was not covered by tests

const auto &base_type = to_pointer_type(src).base_type();

if(base_type.id() == ID_code)
{
const code_typet &code_type = to_code_type(base_type);
const typet &return_type = code_type.return_type();
dest=convert_rec(return_type, c_qualifierst(), "")+" "+dest;
dest = convert(return_type) + " " + dest;

Check warning on line 285 in src/cpp/expr2cpp.cpp

View check run for this annotation

Codecov / codecov/patch

src/cpp/expr2cpp.cpp#L285

Added line #L285 was not covered by tests

const code_typet::parameterst &args = code_type.parameters();
dest+="(";
Expand All @@ -293,14 +293,14 @@ std::string expr2cppt::convert_rec(
{
if(it!=args.begin())
dest+=", ";
dest+=convert_rec(it->type(), c_qualifierst(), "");
dest += convert(it->type());

Check warning on line 296 in src/cpp/expr2cpp.cpp

View check run for this annotation

Codecov / codecov/patch

src/cpp/expr2cpp.cpp#L296

Added line #L296 was not covered by tests
}

dest+=")";
dest+=d;
}
else
dest = convert_rec(base_type, c_qualifierst(), "") + " " + dest + d;
dest = convert(base_type) + " " + dest + d;

Check warning on line 303 in src/cpp/expr2cpp.cpp

View check run for this annotation

Codecov / codecov/patch

src/cpp/expr2cpp.cpp#L303

Added line #L303 was not covered by tests

return dest;
}
Expand Down

0 comments on commit eabcf9c

Please sign in to comment.