Skip to content

Commit 6a42a64

Browse files
kroeningkroening
authored
Merge pull request #57 from diffblue/cbmc-5-91-0-rebase
bump cbmc to 5.91.0
2 parents 8e4f136 + 157b432 commit 6a42a64

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

50 files changed

+231
-279
lines changed

‎.github/workflows/pull-request-checks.yaml

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,6 @@ jobs:
3939
run: ccache -z --max-size=500M
4040
- name: Get minisat
4141
run: |
42-
sudo apt-get install libwww-perl
4342
make -C lib/cbmc/src minisat2-download
4443
- name: Build with make
4544
run: make -C src -j2 CXX="ccache g++"
@@ -54,8 +53,8 @@ jobs:
5453
check-ubuntu-20_04-make-clang:
5554
runs-on: ubuntu-20.04
5655
env:
57-
CC: "ccache /usr/bin/clang"
58-
CXX: "ccache /usr/bin/clang++ -Wno-unknown-warning-option -Wno-range-loop-construct"
56+
CC: "ccache clang"
57+
CXX: "ccache clang++"
5958
steps:
6059
- uses: actions/checkout@v3
6160
with:
@@ -87,11 +86,13 @@ jobs:
8786
run: ccache -z --max-size=500M
8887
- name: Get minisat
8988
run: |
90-
sudo apt-get install libwww-perl
9189
make -C lib/cbmc/src minisat2-download
9290
- name: Build with make
9391
run: |
94-
# expected to fail now
95-
# make -C src -j2
92+
make CXX="ccache clang++" -C src -j2
93+
- name: Run the ebmc tests
94+
run: make -C regression/ebmc test
95+
- name: Run the verilog tests
96+
run: make -C regression/verilog test
9697
- name: Print ccache stats
9798
run: ccache -s

‎lib/cbmc

Submodule cbmc updated 19399 files

‎src/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ hw-cbmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir \
2727
.PHONY: cprover.dir
2828
cprover.dir:
2929
$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR) \
30-
CP_EXTRA_CXXFLAGS='-D"LOCAL_IREP_IDS=<$(EBMC_DIR)/hw_cbmc_irep_ids.h>" -Wno-unused-but-set-variable -Wno-unused-variable -Wno-error=maybe-uninitialized'
30+
CP_EXTRA_CXXFLAGS='-D"LOCAL_IREP_IDS=<$(EBMC_DIR)/hw_cbmc_irep_ids.h>"'
3131

3232
clean: $(patsubst %, %_clean, $(SUBDIRS))
3333

‎src/aiger/aiger_language.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ Function: aiger_languaget::typecheck
106106
\*******************************************************************/
107107

108108
bool aiger_languaget::typecheck(
109-
symbol_tablet &symbol_table,
109+
symbol_table_baset &symbol_table,
110110
const std::string &module)
111111
{
112112
return true;
@@ -124,8 +124,7 @@ Function: aiger_languaget::interfaces
124124
125125
\*******************************************************************/
126126

127-
bool aiger_languaget::interfaces(
128-
symbol_tablet &symbol_table)
127+
bool aiger_languaget::interfaces(symbol_table_baset &symbol_table)
129128
{
130129
return false;
131130
}

‎src/aiger/aiger_language.h

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -33,13 +33,10 @@ class aiger_languaget:public languaget
3333
void modules_provided(
3434
std::set<std::string> &module_set) override;
3535

36-
bool interfaces(
37-
symbol_tablet &symbol_table) override;
36+
bool interfaces(symbol_table_baset &) override;
37+
38+
bool typecheck(symbol_table_baset &, const std::string &module) override;
3839

39-
bool typecheck(
40-
symbol_tablet &symbol_table,
41-
const std::string &module) override;
42-
4340
void show_parse(std::ostream &out) override;
4441

4542
~aiger_languaget() override { }
@@ -58,7 +55,7 @@ class aiger_languaget:public languaget
5855
exprt &expr,
5956
const namespacet &ns) override;
6057

61-
bool generate_support_functions(symbol_tablet &) override
58+
bool generate_support_functions(symbol_table_baset &) override
6259
{
6360
return false;
6461
}

‎src/config.inc

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,5 @@
11
CBMC = ../../lib/cbmc
22

3-
CXXFLAGS += -Wno-unused-variable -Wno-error=unused-but-set-variable
4-
53
include $(CBMC)/src/config.inc
64
include $(CBMC)/src/common
75

‎src/ebmc/ebmc_base.cpp

Lines changed: 25 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -6,19 +6,8 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#include <chrono>
10-
#include <fstream>
11-
#include <iostream>
12-
13-
#include <util/cmdline.h>
14-
#include <util/config.h>
15-
#include <util/expr_util.h>
16-
#include <util/find_macros.h>
17-
#include <util/get_module.h>
18-
#include <util/string2int.h>
19-
#include <util/unicode.h>
20-
#include <util/xml.h>
21-
#include <util/xml_irep.h>
9+
#include "ebmc_base.h"
10+
#include "ebmc_version.h"
2211

2312
#include <trans-netlist/trans_trace_netlist.h>
2413
#include <trans-netlist/ldg.h>
@@ -31,11 +20,25 @@ Author: Daniel Kroening, [email protected]
3120
#include <trans-word-level/unwind.h>
3221
#include <trans-word-level/show_modules.h>
3322

23+
#include <langapi/language.h>
3424
#include <langapi/language_util.h>
3525
#include <langapi/mode.h>
3626

37-
#include "ebmc_base.h"
38-
#include "ebmc_version.h"
27+
#include <solvers/prop/literal_expr.h>
28+
29+
#include <util/cmdline.h>
30+
#include <util/config.h>
31+
#include <util/expr_util.h>
32+
#include <util/find_macros.h>
33+
#include <util/get_module.h>
34+
#include <util/string2int.h>
35+
#include <util/unicode.h>
36+
#include <util/xml.h>
37+
#include <util/xml_irep.h>
38+
39+
#include <chrono>
40+
#include <fstream>
41+
#include <iostream>
3942

4043
/*******************************************************************\
4144
@@ -123,13 +126,14 @@ int ebmc_baset::finish_bmc(prop_conv_solvert &solver) {
123126
continue;
124127

125128
status() << "Checking " << property.name << eom;
126-
127-
or_exprt or_expr;
128-
129+
130+
or_exprt::operandst disjuncts;
131+
disjuncts.reserve(property.timeframe_literals.size());
132+
129133
for(auto l : property.timeframe_literals)
130-
or_expr.operands().push_back(literal_exprt(!l));
134+
disjuncts.push_back(literal_exprt(!l));
131135

132-
auto converted_or = solver.convert(or_expr);
136+
auto converted_or = solver.convert(disjunction(disjuncts));
133137
solver.push({literal_exprt{converted_or}});
134138

135139
decision_proceduret::resultt dec_result=
@@ -1053,9 +1057,7 @@ bool ebmc_baset::parse(const std::string &filename) {
10531057
bool ebmc_baset::typecheck() {
10541058
status() << "Converting" << eom;
10551059

1056-
language_files.set_message_handler(*message_handler);
1057-
1058-
if (language_files.typecheck(symbol_table)) {
1060+
if (language_files.typecheck(symbol_table, *message_handler)) {
10591061
error() << "CONVERSION ERROR" << eom;
10601062
return true;
10611063
}

‎src/ebmc/ebmc_version.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
#define EBMC_VERSION "4.4"
1+
#define EBMC_VERSION "4.5"

‎src/ebmc/output_verilog.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -532,7 +532,7 @@ std::string output_verilog_baset::type_string_base(const typet &type)
532532
}
533533
else if(type.id()==ID_array)
534534
{
535-
return type_string_base(to_array_type(type).subtype());
535+
return type_string_base(to_array_type(type).element_type());
536536
}
537537
else
538538
{
@@ -564,7 +564,7 @@ std::string output_verilog_baset::type_string_array(const typet &type)
564564
auto &array_type = to_array_type(type);
565565
mp_integer size;
566566
to_integer_non_constant(array_type.size(), size);
567-
return type_string_array(array_type.subtype()) +
567+
return type_string_array(array_type.element_type()) +
568568
" [0:" + integer2string(size) + ']';
569569
}
570570

@@ -910,7 +910,7 @@ void output_verilog_baset::invariants(const symbolt &symbol)
910910
assert(symbol.value.id()==ID_trans &&
911911
symbol.value.operands().size()==3);
912912

913-
invariant(symbol.value.op0());
913+
invariant(to_ternary_expr(symbol.value).op0());
914914
}
915915

916916
/*******************************************************************\

‎src/hw-cbmc/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ OBJ+= $(CPROVER_DIR)/goto-checker/goto-checker$(LIBEXT) \
66
$(CPROVER_DIR)/cbmc/cbmc_parse_options$(OBJEXT) \
77
$(CPROVER_DIR)/goto-instrument/cover$(OBJEXT) \
88
$(CPROVER_DIR)/goto-instrument/cover_basic_blocks$(OBJEXT) \
9+
$(CPROVER_DIR)/goto-instrument/cover_instrument_assume$(OBJEXT) \
910
$(CPROVER_DIR)/goto-instrument/cover_instrument_other$(OBJEXT) \
1011
$(CPROVER_DIR)/goto-instrument/cover_instrument_mcdc$(OBJEXT) \
1112
$(CPROVER_DIR)/goto-instrument/cover_instrument_decision$(OBJEXT) \

‎src/hw-cbmc/gen_interface.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ std::string gen_interfacet::type_to_string(const typet& type)
159159
mp_integer size = 0;
160160
to_integer_non_constant(size_expr, size);
161161

162-
std::string stype_str = type_to_string(array_type.subtype());
162+
std::string stype_str = type_to_string(array_type.element_type());
163163
std::string array_str = "[" + integer2string(size)+"]" ;
164164
std::string key_str = stype_str + array_str;
165165

‎src/hw-cbmc/hw_cbmc_parse_options.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,7 @@ int hw_cbmc_parse_optionst::doit()
114114
for (const auto &constraint : constraints) {
115115
// TODO : include the extra constraints using the new custom verifier
116116
// interface
117+
(void)constraint;
117118
}
118119
}
119120

‎src/hw-cbmc/map_vars.cpp

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#include <util/base_type.h>
109
#include <util/c_types.h>
1110
#include <util/config.h>
1211
#include <util/ebmc_util.h>
@@ -241,15 +240,15 @@ bool map_varst::array_types_eq(
241240
}
242241

243242
namespacet ns(symbol_table);
244-
245-
const typet &s1=ns.follow(type1.subtype());
246-
const typet &s2=ns.follow(type2.subtype());
247-
243+
244+
const typet &s1 = ns.follow(type1.element_type());
245+
const typet &s2 = ns.follow(type2.element_type());
246+
248247
if(s1.id()==ID_array && s2.id()==ID_array)
249248
return array_types_eq(to_array_type(s1), to_array_type(s2), error_msg);
250249

251250
// we are strict: the subtype needs to be identical
252-
if(!base_type_eq(s1, s2, ns))
251+
if(s1 != s2)
253252
{
254253
error_msg = "array subtypes differ (E2)";
255254
return true;
@@ -285,7 +284,7 @@ bool map_varst::check_types_rec(
285284
return check_types_rec(type1, ns.follow(type2), error_msg);
286285

287286
// type is the same?
288-
if(base_type_eq(type1, type2, ns))
287+
if(type1 == type2)
289288
return false;
290289

291290
// anything between integral types is fine
@@ -298,7 +297,7 @@ bool map_varst::check_types_rec(
298297
return array_types_eq(to_array_type(type1), to_array_type(type2), error_msg);
299298

300299
// bool-array is mapped to bit-vector
301-
if(to_array_type(type1).subtype().id() != ID_bool)
300+
if(to_array_type(type1).element_type().id() != ID_bool)
302301
{
303302
error_msg = "type `" + from_type(ns, "", type1) +
304303
"' does not match type `" + from_type(ns, "", type2) +
@@ -720,7 +719,7 @@ void map_varst::map_vars(const irep_idt &top_module)
720719
index_exprt expr(
721720
symbol_expr,
722721
timeframe_expr,
723-
to_array_type(ns.follow(symbol_expr.type())).subtype());
722+
to_array_type(ns.follow(symbol_expr.type())).element_type());
724723

725724
top_level_inputs.clear();
726725

‎src/hw-cbmc/next_timeframe.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ void add_next_timeframe(
4545
const plus_exprt plus_expr(
4646
timeframe_expr, from_integer(1, index_type()), index_type());
4747

48-
const code_assignt assignment_increase(timeframe_expr, plus_expr);
48+
const code_frontend_assignt assignment_increase(timeframe_expr, plus_expr);
4949

5050
code_blockt block;
5151
block.add(assignment_increase);
@@ -79,14 +79,14 @@ void add_next_timeframe(
7979

8080
CHECK_RETURN(
8181
member_expr1.compound().type() == member_expr2.compound().type());
82-
const code_assignt member_assignment(member_expr1, member_expr2);
82+
const code_frontend_assignt member_assignment(member_expr1, member_expr2);
8383
block.add(member_assignment);
8484
}
8585

8686
// add code to symbol
8787
symbol.value=block;
8888

8989
// hide and inline
90-
symbol.type.set(ID_C_hide, true);
90+
//symbol.type.set(ID_C_hide, true);
9191
symbol.type.set(ID_C_inlined, true);
9292
}

‎src/hw-cbmc/set_inputs.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,6 @@ void add_set_inputs(
7171
symbol.value=block;
7272

7373
// hide and inline
74-
symbol.type.set(ID_C_hide, true);
74+
// symbol.type.set(ID_C_hide, true);
7575
symbol.type.set(ID_C_inlined, true);
7676
}

‎src/hw_cbmc_irep_ids.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -132,3 +132,4 @@ IREP_ID_ONE(operands)
132132
IREP_ID_ONE(VHDL)
133133
IREP_ID_ONE(init)
134134
IREP_ID_ONE(incomplete_array)
135+
IREP_ID_ONE(next_symbol)

‎src/ic3/dnf_io.hh

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,9 @@ Module: Some type synonyms and prototypes of functions
66
Author: Eugene Goldberg, [email protected]
77
88
******************************************************/
9+
10+
#include <iosfwd>
11+
912
typedef std::vector<int> CUBE;
1013
typedef std::vector<CUBE> DNF;
1114
typedef std::vector<bool> bool_vector;

‎src/ic3/minisat/minisat/core/Solver.cc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -992,11 +992,11 @@ void Solver::printStats() const
992992
{
993993
double cpu_time = cpuTime();
994994
double mem_used = memUsedPeak();
995-
printf("restarts : %"PRIu64"\n", starts);
996-
printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", conflicts , conflicts /cpu_time);
997-
printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time);
998-
printf("propagations : %-12"PRIu64" (%.0f /sec)\n", propagations, propagations/cpu_time);
999-
printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
995+
printf("restarts : %" PRIu64 "\n", starts);
996+
printf("conflicts : %-12" PRIu64 " (%.0f /sec)\n", conflicts , conflicts /cpu_time);
997+
printf("decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time);
998+
printf("propagations : %-12" PRIu64 " (%.0f /sec)\n", propagations, propagations/cpu_time);
999+
printf("conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
10001000
if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
10011001
printf("CPU time : %g s\n", cpu_time);
10021002
}

‎src/smvlang/expr2smv.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -550,7 +550,7 @@ bool type2smv(const typet &type, std::string &code)
550550
else if(type.id()==ID_array)
551551
{
552552
std::string tmp;
553-
if(type2smv(to_array_type(type).subtype(), tmp))
553+
if(type2smv(to_array_type(type).element_type(), tmp))
554554
return true;
555555
code="array ";
556556
code+="..";

‎src/smvlang/parser.y

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -281,7 +281,7 @@ type : ARRAY_Token NUMBER_Token DOTDOT_Token NUMBER_Token OF_Token type
281281

282282
stack_type($$).set(ID_size, end-start+1);
283283
stack_type($$).set(ID_offset, start);
284-
stack_type($$).subtype()=stack_type($6);
284+
stack_type($$).add_subtype()=stack_type($6);
285285
}
286286
| BOOLEAN_Token { init($$, ID_bool); }
287287
| '{' enum_list '}' { $$=$2; }

‎src/smvlang/smv_language.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ bool smv_languaget::parse(
3838

3939
smv_parser.set_file(path);
4040
smv_parser.in=&instream;
41-
smv_parser.set_message_handler(get_message_handler());
41+
smv_parser.log.set_message_handler(get_message_handler());
4242

4343
bool result=smv_parser.parse();
4444

@@ -117,7 +117,7 @@ Function: smv_languaget::typecheck
117117
\*******************************************************************/
118118

119119
bool smv_languaget::typecheck(
120-
symbol_tablet &symbol_table,
120+
symbol_table_baset &symbol_table,
121121
const std::string &module)
122122
{
123123
return smv_typecheck(smv_parse_tree, symbol_table, module,

0 commit comments

Comments
 (0)