Skip to content

Commit

Permalink
Remove support for irep_idt-as-std::string
Browse files Browse the repository at this point in the history
While diffblue#8040 ensured we were still able to compile the code base with
`irep_idt` typedef'd to `std::string` (via `USE_STD_STRING`),
experiments at that time also demonstrated that performance is
substantially worse, and not all tests would pass.

This commit now removes this untested feature to pave the way for
changes that may break `dstringt` to `std::string` compatibility.
  • Loading branch information
tautschnig committed Jan 10, 2024
1 parent 09dca35 commit ea2643e
Show file tree
Hide file tree
Showing 14 changed files with 6 additions and 106 deletions.
5 changes: 0 additions & 5 deletions src/analyses/goto_rw.h
Original file line number Diff line number Diff line change
Expand Up @@ -203,12 +203,7 @@ class shift_exprt;
class rw_range_sett
{
public:
#ifdef USE_DSTRING
typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
#else
typedef std::unordered_map<
irep_idt, std::unique_ptr<range_domain_baset>, string_hash> objectst;
#endif

virtual ~rw_range_sett();

Expand Down
8 changes: 0 additions & 8 deletions src/analyses/reaching_definitions.h
Original file line number Diff line number Diff line change
Expand Up @@ -274,23 +274,15 @@ class rd_range_domaint:public ai_domain_baset
sparse_bitvector_analysist<reaching_definitiont> *const bv_container;

typedef std::set<std::size_t> values_innert;
#ifdef USE_DSTRING
typedef std::map<irep_idt, values_innert> valuest;
#else
typedef std::unordered_map<irep_idt, values_innert> valuest;
#endif
/// It is an ordered map from program variable names to `ID`s of
/// `reaching_definitiont` instances stored in map pointed to by
/// `bv_container`. The map is not empty only if `has_value` is `UNKNOWN`.
/// Variables in the map are all those which are live at the associated
/// instruction.
valuest values;

#ifdef USE_DSTRING
typedef std::map<irep_idt, ranges_at_loct> export_cachet;
#else
typedef std::unordered_map<irep_idt, ranges_at_loct> export_cachet;
#endif
/// It is a helper data structure. It consists of data already stored in
/// `values` and `bv_container`. It is basically (an ordered) map from (a
/// subset of) variables in `values` to iterators to GOTO instructions where
Expand Down
13 changes: 0 additions & 13 deletions src/goto-programs/graphml_witness.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,6 @@ Author: Daniel Kroening
#include <util/prefix.h>
#include <util/ssa_expr.h>
#include <util/string_constant.h>
#ifndef USE_DSTRING
# include <util/string_container.h>
#endif
#include <util/symbol.h>

#include <ansi-c/expr2c.h>
Expand Down Expand Up @@ -78,12 +75,7 @@ std::string graphml_witnesst::convert_assign_rec(
const irep_idt &identifier,
const code_assignt &assign)
{
#ifdef USE_DSTRING
const auto cit = cache.find({identifier.get_no(), &assign.read()});
#else
const auto cit =
cache.find({get_string_container()[id2string(identifier)], &assign.read()});
#endif
if(cit != cache.end())
return cit->second;

Expand Down Expand Up @@ -219,12 +211,7 @@ std::string graphml_witnesst::convert_assign_rec(
result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";";
}

#ifdef USE_DSTRING
cache.insert({{identifier.get_no(), &assign.read()}, result});
#else
cache.insert(
{{get_string_container()[id2string(identifier)], &assign.read()}, result});
#endif
return result;
}

Expand Down
8 changes: 0 additions & 8 deletions src/libcprover-cpp/verification_result.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,16 +12,8 @@
#include <string>
#include <vector>

#ifndef USE_STD_STRING
# define USE_DSTRING
#endif

#ifdef USE_DSTRING
class dstringt;
typedef dstringt irep_idt;
#else
typedef std::string irep_idt;
#endif

struct property_infot;
using propertiest = std::map<irep_idt, property_infot>;
Expand Down
8 changes: 0 additions & 8 deletions src/pointer-analysis/value_set_fi.h
Original file line number Diff line number Diff line change
Expand Up @@ -191,19 +191,11 @@ class value_set_fit

typedef std::unordered_set<unsigned int> dynamic_object_id_sett;

#ifdef USE_DSTRING
typedef std::map<idt, entryt> valuest;
typedef std::set<idt> flatten_seent;
typedef std::unordered_set<idt> gvs_recursion_sett;
typedef std::unordered_set<idt> recfind_recursion_sett;
typedef std::unordered_set<idt> assign_recursion_sett;
#else
typedef std::unordered_map<idt, entryt, string_hash> valuest;
typedef std::unordered_set<idt, string_hash> flatten_seent;
typedef std::unordered_set<idt, string_hash> gvs_recursion_sett;
typedef std::unordered_set<idt, string_hash> recfind_recursion_sett;
typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
#endif

std::vector<exprt>
get_value_set(const exprt &expr, const namespacet &ns) const;
Expand Down
6 changes: 3 additions & 3 deletions src/util/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -72,9 +72,9 @@ standard data structures as in irept.

\subsection irep_idt_section Strings: dstringt, the string_container and the ID_*

Within cbmc, strings are represented using \ref irep_idt. By default this is
typedefed to \ref dstringt. For debugging purposes you can set `USE_STD_STRING`
to change this typedef to `std::string`. You can also easily convert an
Within cbmc, strings are represented using \ref irep_idt, which is
typedefed to \ref dstringt.
You can also easily convert an
[irep_idt](\ref irep_idt) to a `std::string` using the
[id2string](\ref id2string) function, or to a `char*` using the
[c_str()](\ref dstringt::c_str) member function.
Expand Down
3 changes: 1 addition & 2 deletions src/util/dstring.h
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,7 @@ struct diagnostics_helpert;
/// copies of the same string you only have to store the whole string once,
/// which saves space.
///
/// `irep_idt` is typedef-ed to \ref dstringt in irep.h unless `USE_STD_STRING`
/// is set.
/// `irep_idt` is typedef-ed to \ref dstringt in irep.h.
///
///
/// Note: Marked final to disable inheritance. No virtual destructor, so
Expand Down
8 changes: 0 additions & 8 deletions src/util/irep.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -76,20 +76,12 @@ long long irept::get_long_long(const irep_idt &name) const

void irept::set(const irep_idt &name, const long long value)
{
#ifdef USE_DSTRING
add(name).id(to_dstring(value));
#else
add(name).id(std::to_string(value));
#endif
}

void irept::set_size_t(const irep_idt &name, const std::size_t value)
{
#ifdef USE_DSTRING
add(name).id(to_dstring(value));
#else
add(name).id(std::to_string(value));
#endif
}

void irept::remove(const irep_idt &name)
Expand Down
16 changes: 2 additions & 14 deletions src/util/irep.h
Original file line number Diff line number Diff line change
Expand Up @@ -33,24 +33,13 @@ Author: Daniel Kroening, [email protected]
#include <map>
#endif

#ifdef USE_DSTRING
typedef dstringt irep_idt;
// NOLINTNEXTLINE(readability/identifiers)
typedef dstring_hash irep_id_hash;
#else
#include "string_hash.h"
typedef std::string irep_idt;
// NOLINTNEXTLINE(readability/identifiers)
typedef string_hash irep_id_hash;
#endif

inline const std::string &id2string(const irep_idt &d)
{
#ifdef USE_DSTRING
return as_string(d);
#else
return d;
#endif
}

#ifdef IREP_DEBUG
Expand All @@ -76,9 +65,8 @@ struct ref_count_ift<true>

/// A node with data in a tree, it contains:
///
/// * \ref irept::dt::data : A string (Unless `USE_STD_STRING` is set, this is
/// actually a \ref dstringt and thus an integer which is a reference into a
/// string table.)
/// * \ref irept::dt::data : A \ref dstringt and thus an integer which is a
/// reference into a string table.)
///
/// * \ref irept::dt::named_sub : A map from `irep_idt` (a string) to \ref
/// irept. This is used for named children, i.e. subexpressions, parameters,
Expand Down
9 changes: 0 additions & 9 deletions src/util/irep_ids.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,6 @@ const char *irep_ids_table[]=
nullptr,
};

#ifdef USE_DSTRING

enum class idt:unsigned
{
#define IREP_ID_ONE(the_id) id_##the_id,
Expand All @@ -42,13 +40,6 @@ enum class idt:unsigned
const dstringt ID_##the_id=dstringt::make_from_table_index( \
static_cast<unsigned>(idt::id_##the_id));

#else

#define IREP_ID_ONE(the_id) const std::string ID_##the_id(#the_id);
# define IREP_ID_TWO(the_id, str) const std::string ID_##the_id(# str);

#endif

#include "irep_ids.def" // NOLINT(build/include)

string_containert::string_containert()
Expand Down
17 changes: 0 additions & 17 deletions src/util/irep_ids.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,15 +12,7 @@ Author: Reuben Thomas, [email protected]
#ifndef CPROVER_UTIL_IREP_IDS_H
#define CPROVER_UTIL_IREP_IDS_H

#ifndef USE_STD_STRING
#define USE_DSTRING
#endif

#ifdef USE_DSTRING
#include "dstring.h"
#else
#include <string>
#endif

/// \file
/// The irep_ids are generated using a technique called
Expand All @@ -34,18 +26,9 @@ Author: Reuben Thomas, [email protected]
/// into a const extern irep_idt with the variable name `ID_param` and the
/// string value `"contents"`.

#ifdef USE_DSTRING

#define IREP_ID_ONE(the_id) extern const dstringt ID_##the_id;
#define IREP_ID_TWO(the_id, str) extern const dstringt ID_##the_id;

#else

#define IREP_ID_ONE(the_id) extern const std::string ID_##the_id;
#define IREP_ID_TWO(the_id, str) extern const std::string ID_##the_id;

#endif

#include "irep_ids.def"

#endif
4 changes: 0 additions & 4 deletions src/util/irep_serialization.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -212,11 +212,7 @@ void irep_serializationt::write_string_ref(
std::ostream &out,
const irep_idt &s)
{
#ifdef USE_DSTRING
size_t id = s.get_no();
#else
size_t id = get_string_container()[s];
#endif
if(id>=ireps_container.string_map.size())
ireps_container.string_map.resize(id+1, false);

Expand Down
2 changes: 0 additions & 2 deletions src/util/json.h
Original file line number Diff line number Diff line change
Expand Up @@ -274,12 +274,10 @@ class json_stringt:public jsont
{
}

#ifdef USE_DSTRING
explicit json_stringt(const irep_idt &_value)
: jsont(kindt::J_STRING, id2string(_value))
{
}
#endif

/// Constructon from string literal.
explicit json_stringt(const char *_value) : jsont(kindt::J_STRING, _value)
Expand Down
5 changes: 0 additions & 5 deletions unit/util/irep.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,13 +22,8 @@ SCENARIO("irept_memory", "[core][utils][irept]")
const std::size_t ref_count_size = 0;
#endif

#ifdef USE_DSTRING
const std::size_t data_size = sizeof(dstringt);
REQUIRE(sizeof(dstringt) == sizeof(unsigned));
#else
const std::size_t data_size = sizeof(std::string);
REQUIRE(sizeof(std::string) == sizeof(void *));
#endif

const std::size_t sub_size = sizeof(std::vector<int>);
#ifndef _GLIBCXX_DEBUG
Expand Down

0 comments on commit ea2643e

Please sign in to comment.