Skip to content

Commit 0c72d99

Browse files
tautschnigtautschnig
committed
Remove config dependency from CVC and DPLIB solvers
1 parent bbbe601 commit 0c72d99

File tree

4 files changed

+60
-109
lines changed

4 files changed

+60
-109
lines changed

‎src/solvers/cvc/cvc_conv.cpp‎

Lines changed: 31 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ Author: Daniel Kroening, kroening@kroening.com
1313
#include <string>
1414

1515
#include <util/arith_tools.h>
16+
#include <util/c_types.h>
1617
#include <util/std_types.h>
1718
#include <util/std_expr.h>
18-
#include <util/config.h>
1919
#include <util/find_symbols.h>
2020
#include <util/pointer_offset_size.h>
2121
#include <util/string2int.h>
@@ -159,8 +159,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
159159
{
160160
out << "(# object:="
161161
<< pointer_logic.get_null_object()
162-
<< ", offset:="
163-
<< bin_zero(config.ansi_c.pointer_width) << " #)";
162+
<< ", offset:=";
163+
convert_expr(from_integer(0, size_type()));
164+
out << " #)";
164165
}
165166
else
166167
throw "unknown pointer constant: "+id2string(value);
@@ -176,7 +177,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
176177
}
177178
else if(expr.type().id()==ID_array)
178179
{
179-
out << "ARRAY (i: " << array_index_type() << "):";
180+
out << "ARRAY (i: ";
181+
convert_type(index_type());
182+
out << "):";
180183

181184
assert(!expr.operands().empty());
182185

@@ -188,7 +191,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
188191
else
189192
out << "\n ELSIF ";
190193

191-
out << "i=" << array_index(i) << " THEN ";
194+
out << "i=";
195+
convert_expr(from_integer(i, index_type()));
196+
out << " THEN ";
192197
convert_array_value(*it);
193198
i++;
194199
}
@@ -247,7 +252,7 @@ void cvc_convt::convert_plus_expr(const exprt &expr)
247252
out << "(LET P: " << cvc_pointer_type() << " = ";
248253
convert_expr(*p);
249254
out << " IN P WITH .offset:=BVPLUS("
250-
<< config.ansi_c.pointer_width
255+
<< pointer_offset_bits(pointer_type(void_type()), ns)
251256
<< ", P.offset, ";
252257
convert_expr(*i);
253258
out << "))";
@@ -487,52 +492,24 @@ void cvc_convt::convert_literal(const literalt l)
487492
out << ")";
488493
}
489494

490-
std::string cvc_convt::bin_zero(unsigned bits)
495+
std::string cvc_convt::cvc_pointer_type() const
491496
{
492-
assert(bits!=0);
493-
std::string result="0bin";
494-
while(bits!=0)
495-
{
496-
result+='0';
497-
bits--;
498-
}
499-
return result;
500-
}
501-
502-
std::string cvc_convt::cvc_pointer_type()
503-
{
504-
assert(config.ansi_c.pointer_width!=0);
505-
return "[# object: INT, offset: BITVECTOR("+
506-
std::to_string(config.ansi_c.pointer_width)+") #]";
507-
}
508-
509-
std::string cvc_convt::array_index_type()
510-
{
511-
return std::string("BITVECTOR(")+
512-
std::to_string(32)+")";
513-
}
514-
515-
typet cvc_convt::gen_array_index_type()
516-
{
517-
typet t(ID_signedbv);
518-
t.set(ID_width, 32);
519-
return t;
520-
}
521-
522-
std::string cvc_convt::array_index(unsigned i)
523-
{
524-
return "0bin"+integer2binary(i, config.ansi_c.int_width);
497+
return
498+
"[# object: INT, offset: BITVECTOR("+
499+
std::to_string(
500+
integer2size_t(
501+
pointer_offset_bits(pointer_type(void_type()), ns)))+") #]";
525502
}
526503

527504
void cvc_convt::convert_array_index(const exprt &expr)
528505
{
529-
if(expr.type()==gen_array_index_type())
506+
if(expr.type()==index_type())
530507
{
531508
convert_expr(expr);
532509
}
533510
else
534511
{
535-
exprt tmp(ID_typecast, gen_array_index_type());
512+
exprt tmp(ID_typecast, index_type());
536513
tmp.copy_to_operands(expr);
537514
convert_expr(tmp);
538515
}
@@ -547,8 +524,9 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
547524
out
548525
<< "(# object:="
549526
<< pointer_logic.add_object(expr)
550-
<< ", offset:="
551-
<< bin_zero(config.ansi_c.pointer_width) << " #)";
527+
<< ", offset:=";
528+
convert_expr(from_integer(0, size_type()));
529+
out << " #)";
552530
}
553531
else if(expr.id()==ID_index)
554532
{
@@ -581,7 +559,7 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
581559
assert(false);
582560

583561
out << " IN P WITH .offset:=BVPLUS("
584-
<< config.ansi_c.pointer_width
562+
<< pointer_offset_bits(pointer_type(void_type()), ns)
585563
<< ", P.offset, ";
586564
convert_expr(index);
587565
out << "))";
@@ -609,13 +587,10 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
609587
ns);
610588
assert(offset>=0);
611589

612-
typet index_type(ID_unsignedbv);
613-
index_type.set(ID_width, config.ansi_c.pointer_width);
614-
615-
exprt index=from_integer(offset, index_type);
590+
exprt index=from_integer(offset, size_type());
616591

617592
out << " IN P WITH .offset:=BVPLUS("
618-
<< config.ansi_c.pointer_width
593+
<< pointer_offset_bits(pointer_type(void_type()), ns)
619594
<< ", P.offset, ";
620595
convert_expr(index);
621596
out << "))";
@@ -1035,7 +1010,9 @@ void cvc_convt::convert_expr(const exprt &expr)
10351010
{
10361011
assert(expr.type().id()==ID_array);
10371012
assert(expr.operands().size()==1);
1038-
out << "(ARRAY (i: " << array_index_type() << "): ";
1013+
out << "(ARRAY (i: ";
1014+
convert_type(index_type());
1015+
out << "): ";
10391016
convert_array_value(expr.op0());
10401017
out << ")";
10411018
}
@@ -1273,8 +1250,9 @@ void cvc_convt::convert_type(const typet &type)
12731250
{
12741251
const array_typet &array_type=to_array_type(type);
12751252

1276-
out << "ARRAY " << array_index_type()
1277-
<< " OF ";
1253+
out << "ARRAY ";
1254+
convert_type(index_type());
1255+
out << " OF ";
12781256

12791257
if(array_type.subtype().id()==ID_bool)
12801258
out << "BITVECTOR(1)";

‎src/solvers/cvc/cvc_conv.h‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -79,11 +79,7 @@ class cvc_convt:public prop_convt
7979
void convert_array_value(const exprt &expr);
8080
void convert_as_bv(const exprt &expr);
8181
void convert_array_index(const exprt &expr);
82-
static typet gen_array_index_type();
83-
static std::string bin_zero(unsigned bits);
84-
static std::string array_index_type();
85-
static std::string array_index(unsigned i);
86-
static std::string cvc_pointer_type();
82+
std::string cvc_pointer_type() const;
8783
};
8884

8985
#endif // CPROVER_SOLVERS_CVC_CVC_CONV_H

‎src/solvers/dplib/dplib_conv.cpp‎

Lines changed: 27 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -12,56 +12,33 @@ Author: Daniel Kroening, kroening@kroening.com
1212
#include <cctype>
1313

1414
#include <util/arith_tools.h>
15+
#include <util/c_types.h>
1516
#include <util/std_types.h>
1617
#include <util/std_expr.h>
17-
#include <util/config.h>
1818
#include <util/find_symbols.h>
1919
#include <util/pointer_offset_size.h>
2020
#include <util/string2int.h>
2121

2222
#include <ansi-c/string_constant.h>
2323

24-
std::string dplib_convt::bin_zero(unsigned bits)
25-
{
26-
assert(bits!=0);
27-
std::string result="0bin";
28-
while(bits!=0) { result+='0'; bits--; }
29-
return result;
30-
}
31-
3224
std::string dplib_convt::dplib_pointer_type()
3325
{
34-
assert(config.ansi_c.pointer_width!=0);
35-
return "[# object: INT, offset: BITVECTOR("+
36-
std::to_string(config.ansi_c.pointer_width)+") #]";
37-
}
38-
39-
std::string dplib_convt::array_index_type()
40-
{
41-
return std::string("SIGNED [")+std::to_string(32)+"]";
42-
}
43-
44-
typet dplib_convt::gen_array_index_type()
45-
{
46-
typet t(ID_signedbv);
47-
t.set(ID_width, 32);
48-
return t;
49-
}
50-
51-
std::string dplib_convt::array_index(unsigned i)
52-
{
53-
return "0bin"+integer2binary(i, config.ansi_c.int_width);
26+
return
27+
"[# object: INT, offset: BITVECTOR("+
28+
std::to_string(
29+
integer2size_t(
30+
pointer_offset_bits(pointer_type(void_type()), ns)))+") #]";
5431
}
5532

5633
void dplib_convt::convert_array_index(const exprt &expr)
5734
{
58-
if(expr.type()==gen_array_index_type())
35+
if(expr.type()==index_type())
5936
{
6037
convert_dplib_expr(expr);
6138
}
6239
else
6340
{
64-
exprt tmp(ID_typecast, gen_array_index_type());
41+
exprt tmp(ID_typecast, index_type());
6542
tmp.copy_to_operands(expr);
6643
convert_dplib_expr(tmp);
6744
}
@@ -76,8 +53,9 @@ void dplib_convt::convert_address_of_rec(const exprt &expr)
7653
dplib_prop.out
7754
<< "(# object:="
7855
<< pointer_logic.add_object(expr)
79-
<< ", offset:="
80-
<< bin_zero(config.ansi_c.pointer_width) << " #)";
56+
<< ", offset:=";
57+
convert_expr(from_integer(0, size_type()));
58+
dplib_prop.out << " #)";
8159
}
8260
else if(expr.id()==ID_index)
8361
{
@@ -110,7 +88,7 @@ void dplib_convt::convert_address_of_rec(const exprt &expr)
11088
assert(false);
11189

11290
dplib_prop.out << " IN P WITH .offset:=BVPLUS("
113-
<< config.ansi_c.pointer_width
91+
<< pointer_offset_bits(pointer_type(void_type()), ns)
11492
<< ", P.offset, ";
11593
convert_dplib_expr(index);
11694
dplib_prop.out << "))";
@@ -136,13 +114,10 @@ void dplib_convt::convert_address_of_rec(const exprt &expr)
136114
to_struct_type(struct_op.type()), component_name);
137115
assert(offset>=0);
138116

139-
typet index_type(ID_unsignedbv);
140-
index_type.set(ID_width, config.ansi_c.pointer_width);
141-
142-
exprt index=from_integer(offset, index_type);
117+
exprt index=from_integer(offset, size_type());
143118

144119
dplib_prop.out << " IN P WITH .offset:=BVPLUS("
145-
<< config.ansi_c.pointer_width
120+
<< pointer_offset_bits(pointer_type(void_type()), ns)
146121
<< ", P.offset, ";
147122
convert_dplib_expr(index);
148123
dplib_prop.out << "))";
@@ -395,8 +370,9 @@ void dplib_convt::convert_dplib_expr(const exprt &expr)
395370
{
396371
dplib_prop.out << "(# object:="
397372
<< pointer_logic.get_null_object()
398-
<< ", offset:="
399-
<< bin_zero(config.ansi_c.pointer_width) << " #)";
373+
<< ", offset:=";
374+
convert_expr(from_integer(0, size_type()));
375+
dplib_prop.out << " #)";
400376
}
401377
else
402378
throw "unknown pointer constant: "+id2string(value);
@@ -412,7 +388,9 @@ void dplib_convt::convert_dplib_expr(const exprt &expr)
412388
}
413389
else if(expr.type().id()==ID_array)
414390
{
415-
dplib_prop.out << "ARRAY (i: " << array_index_type() << "):";
391+
dplib_prop.out << "ARRAY (i: ";
392+
convert_type(index_type();
393+
dplib_prop.out << "):";
416394

417395
assert(!expr.operands().empty());
418396

@@ -691,7 +669,7 @@ void dplib_convt::convert_dplib_expr(const exprt &expr)
691669
dplib_prop.out << "(LET P: " << dplib_pointer_type() << " = ";
692670
convert_dplib_expr(*p);
693671
dplib_prop.out << " IN P WITH .offset:=BVPLUS("
694-
<< config.ansi_c.pointer_width
672+
<< pointer_offset_bits(pointer_type(void_type()), ns)
695673
<< ", P.offset, ";
696674
convert_dplib_expr(*i);
697675
dplib_prop.out << "))";
@@ -805,7 +783,9 @@ void dplib_convt::convert_dplib_expr(const exprt &expr)
805783
{
806784
assert(expr.type().id()==ID_array);
807785
assert(expr.operands().size()==1);
808-
dplib_prop.out << "(ARRAY (i: " << array_index_type() << "): ";
786+
dplib_prop.out << "(ARRAY (i: ";
787+
convert_type(index_type());
788+
dplib_prop.out << "): ";
809789
convert_array_value(expr.op0());
810790
dplib_prop.out << ")";
811791
}
@@ -1079,8 +1059,9 @@ void dplib_convt::convert_dplib_type(const typet &type)
10791059
{
10801060
const array_typet &array_type=to_array_type(type);
10811061

1082-
dplib_prop.out << "ARRAY " << array_index_type()
1083-
<< " OF ";
1062+
dplib_prop.out << "ARRAY ";
1063+
convert_type(index_type());
1064+
dplib_prop.out << " OF ";
10841065

10851066
if(array_type.subtype().id()==ID_bool)
10861067
dplib_prop.out << "BITVECTOR(1)";

‎src/solvers/dplib/dplib_conv.h‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -46,11 +46,7 @@ class dplib_convt:public prop_convt
4646
void convert_array_value(const exprt &expr);
4747
void convert_as_bv(const exprt &expr);
4848
void convert_array_index(const exprt &expr);
49-
static typet gen_array_index_type();
50-
static std::string bin_zero(unsigned bits);
51-
static std::string array_index_type();
52-
static std::string array_index(unsigned i);
53-
static std::string dplib_pointer_type();
49+
std::string dplib_pointer_type() const;
5450

5551
struct identifiert
5652
{

0 commit comments

Comments
 (0)