From 7523cafb3e33402d73ead4c82505008ce8d781e2 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 14 Feb 2023 15:55:50 +0000 Subject: [PATCH 1/4] Include `` where needed when building with `NAMED_SUB_IS_FORWARD_LIST == 0` --- .../value_set_pointer_abstract_object.cpp | 1 + src/cprover/generalization.cpp | 1 + src/cprover/inductiveness.cpp | 1 + src/cprover/state_encoding.cpp | 1 + src/goto-instrument/contracts/instrument_spec_assigns.h | 1 + src/goto-instrument/unwindset.cpp | 1 + src/solvers/flattening/boolbv_bitreverse.cpp | 4 +++- src/solvers/flattening/boolbv_get.cpp | 2 ++ src/solvers/smt2_incremental/ast/smt_commands.cpp | 2 ++ src/solvers/smt2_incremental/convert_expr_to_smt.cpp | 2 +- src/util/simplify_expr_int.cpp | 2 ++ 11 files changed, 16 insertions(+), 2 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp index 095ee1d327a..97a01342093 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp @@ -18,6 +18,7 @@ #include "abstract_environment.h" #include "context_abstract_object.h" // IWYU pragma: keep +#include #include static abstract_object_sett diff --git a/src/cprover/generalization.cpp b/src/cprover/generalization.cpp index ac5a469b6e4..098d1aae8cb 100644 --- a/src/cprover/generalization.cpp +++ b/src/cprover/generalization.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "solver.h" +#include #include #include diff --git a/src/cprover/inductiveness.cpp b/src/cprover/inductiveness.cpp index b7975765127..6f4484fae12 100644 --- a/src/cprover/inductiveness.cpp +++ b/src/cprover/inductiveness.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "propagate.h" #include "solver.h" +#include #include #include diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp index 667a43c2f0b..ed3c65e99a0 100644 --- a/src/cprover/state_encoding.cpp +++ b/src/cprover/state_encoding.cpp @@ -26,6 +26,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "state_encoding_targets.h" #include "variable_encoding.h" +#include #include class state_encodingt diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.h b/src/goto-instrument/contracts/instrument_spec_assigns.h index 55ad8cdb368..d899d005fed 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.h +++ b/src/goto-instrument/contracts/instrument_spec_assigns.h @@ -21,6 +21,7 @@ Date: January 2022 #include +#include #include #include diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp index 6c1ee7da68b..eebd8c5682d 100644 --- a/src/goto-instrument/unwindset.cpp +++ b/src/goto-instrument/unwindset.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include void unwindsett::parse_unwind(const std::string &unwind) diff --git a/src/solvers/flattening/boolbv_bitreverse.cpp b/src/solvers/flattening/boolbv_bitreverse.cpp index 4104bc23257..a6e7538fd70 100644 --- a/src/solvers/flattening/boolbv_bitreverse.cpp +++ b/src/solvers/flattening/boolbv_bitreverse.cpp @@ -6,9 +6,11 @@ Author: Michael Tautschnig \*******************************************************************/ +#include + #include "boolbv.h" -#include +#include bvt boolbvt::convert_bitreverse(const bitreverse_exprt &expr) { diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index e32865c929b..03c15a04219 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" #include "boolbv_type.h" +#include + exprt boolbvt::get(const exprt &expr) const { if(expr.id()==ID_symbol || diff --git a/src/solvers/smt2_incremental/ast/smt_commands.cpp b/src/solvers/smt2_incremental/ast/smt_commands.cpp index bd4c1d6e568..ca16b6a3311 100644 --- a/src/solvers/smt2_incremental/ast/smt_commands.cpp +++ b/src/solvers/smt2_incremental/ast/smt_commands.cpp @@ -4,6 +4,8 @@ #include +#include + // Define the irep_idts for commands. #define COMMAND_ID(the_id) \ const irep_idt ID_smt_##the_id##_command{"smt_" #the_id "_command"}; diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 2f1796702a6..6da52fdb9d2 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1,5 +1,4 @@ // Author: Diffblue Ltd. - #include #include #include @@ -22,6 +21,7 @@ #include #include +#include #include #include diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 85a64db3ad6..1bfa8a7d6e7 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -25,6 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_utils.h" #include "std_expr.h" +#include + simplify_exprt::resultt<> simplify_exprt::simplify_bswap(const bswap_exprt &expr) { From 487c28c5ad2ac7e3950393d6b65a4a244c0a96f5 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 14 Feb 2023 15:58:46 +0000 Subject: [PATCH 2/4] Add `emplace` method to `forward_list_as_mapt` and simplify where possible --- src/util/forward_list_as_map.h | 17 +++++++++++++++++ src/util/irep_serialization.cpp | 13 ------------- 2 files changed, 17 insertions(+), 13 deletions(-) diff --git a/src/util/forward_list_as_map.h b/src/util/forward_list_as_map.h index 37d264e1494..49fc84d43a2 100644 --- a/src/util/forward_list_as_map.h +++ b/src/util/forward_list_as_map.h @@ -94,6 +94,23 @@ class forward_list_as_mapt : public std::forward_list> return it->second; } + mappedt &emplace(const keyt &name, const mappedt &irep) + { + iterator it = mutable_lower_bound(name); + + if(it == this->end() || it->first != name) + { + iterator before = this->before_begin(); + while(std::next(before) != it) + ++before; + it = this->emplace_after(before, name, irep); + } + else + it->second = irep; + + return it->second; + } + std::size_t size() const { return narrow(std::distance(this->begin(), this->end())); diff --git a/src/util/irep_serialization.cpp b/src/util/irep_serialization.cpp index f4d6e1da5d3..b9a6d68345d 100644 --- a/src/util/irep_serialization.cpp +++ b/src/util/irep_serialization.cpp @@ -75,31 +75,18 @@ irept irep_serializationt::read_irep(std::istream &in) sub.push_back(reference_convert(in)); } -#if NAMED_SUB_IS_FORWARD_LIST - irept::named_subt::iterator before = named_sub.before_begin(); -#endif while(in.peek()=='N') { in.get(); irep_idt id = read_string_ref(in); -#if NAMED_SUB_IS_FORWARD_LIST - named_sub.emplace_after(before, id, reference_convert(in)); - ++before; -#else named_sub.emplace(id, reference_convert(in)); -#endif } while(in.peek()=='C') { in.get(); irep_idt id = read_string_ref(in); -#if NAMED_SUB_IS_FORWARD_LIST - named_sub.emplace_after(before, id, reference_convert(in)); - ++before; -#else named_sub.emplace(id, reference_convert(in)); -#endif } if(in.get()!=0) From 7cbee89f4a1e89f0f4151e3b9ce08aa695553899 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 14 Feb 2023 16:00:24 +0000 Subject: [PATCH 3/4] Simplify use the `size` method instead of `distance` --- src/util/irep_hash_container.cpp | 5 ----- src/util/lispirep.cpp | 5 ----- 2 files changed, 10 deletions(-) diff --git a/src/util/irep_hash_container.cpp b/src/util/irep_hash_container.cpp index c3c6120812e..292e7ff3aad 100644 --- a/src/util/irep_hash_container.cpp +++ b/src/util/irep_hash_container.cpp @@ -55,12 +55,7 @@ void irep_hash_container_baset::pack( { // we pack: the irep id, the sub size, the subs, the named-sub size, and // each of the named subs with their ids -#if NAMED_SUB_IS_FORWARD_LIST - const std::size_t named_sub_size = - std::distance(named_sub.begin(), named_sub.end()); -#else const std::size_t named_sub_size = named_sub.size(); -#endif packed.reserve(1 + 1 + sub.size() + 1 + named_sub_size * 2); packed.push_back(irep_id_hash()(irep.id())); diff --git a/src/util/lispirep.cpp b/src/util/lispirep.cpp index f5cb589c8ff..46df0e1b81f 100644 --- a/src/util/lispirep.cpp +++ b/src/util/lispirep.cpp @@ -46,12 +46,7 @@ void irep2lisp(const irept &src, lispexprt &dest) dest.value.clear(); dest.type=lispexprt::List; -#if NAMED_SUB_IS_FORWARD_LIST - const std::size_t named_sub_size = - std::distance(src.get_named_sub().begin(), src.get_named_sub().end()); -#else const std::size_t named_sub_size = src.get_named_sub().size(); -#endif dest.reserve(2 + 2 * src.get_sub().size() + 2 * named_sub_size); lispexprt id; From c52c0f689168a97c0db05c7474f67b0000bc7a94 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 14 Feb 2023 16:00:55 +0000 Subject: [PATCH 4/4] Rename `remove` to `erase` to allow simplifications --- src/util/forward_list_as_map.h | 2 +- src/util/irep.cpp | 4 ---- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/util/forward_list_as_map.h b/src/util/forward_list_as_map.h index 49fc84d43a2..d240fa4e744 100644 --- a/src/util/forward_list_as_map.h +++ b/src/util/forward_list_as_map.h @@ -34,7 +34,7 @@ class forward_list_as_mapt : public std::forward_list> { } - void remove(const keyt &name) + void erase(const keyt &name) { const_iterator it = this->lower_bound(name); diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 929a3ea37b3..650e8bc768f 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -94,12 +94,8 @@ void irept::set_size_t(const irep_idt &name, const std::size_t value) void irept::remove(const irep_idt &name) { -#if NAMED_SUB_IS_FORWARD_LIST - return get_named_sub().remove(name); -#else named_subt &s = get_named_sub(); s.erase(name); -#endif } const irept &irept::find(const irep_idt &name) const