Skip to content

Commit 88acdfd

Browse files
kroeningkroening
authored
Merge pull request #1355 from diffblue/cleanout-config-dependency
[depends: #1333] pointers now come with a width
2 parents c0ce9de + 32dcad8 commit 88acdfd

File tree

14 files changed

+87
-113
lines changed

14 files changed

+87
-113
lines changed

‎regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,9 @@ CORE
22
main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
5-
^\s*IF fp == \(const void_fp\)f2 THEN GOTO [0-9]$
6-
^\s*IF fp == \(const void_fp\)f3 THEN GOTO [0-9]$
7-
^\s*IF fp == \(const void_fp\)f4 THEN GOTO [0-9]$
5+
^\s*IF fp == \(.*\)f2 THEN GOTO [0-9]$
6+
^\s*IF fp == \(.*\)f3 THEN GOTO [0-9]$
7+
^\s*IF fp == \(.*\)f4 THEN GOTO [0-9]$
88
^SIGNAL=0$
99
--
1010
^warning: ignoring

‎src/ansi-c/ansi_c_convert_type.cpp‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,9 @@ Author: Daniel Kroening, [email protected]
1414
#include <cassert>
1515

1616
#include <util/c_types.h>
17+
#include <util/config.h>
1718
#include <util/namespace.h>
1819
#include <util/simplify_expr.h>
19-
#include <util/config.h>
2020
#include <util/arith_tools.h>
2121
#include <util/std_types.h>
2222

@@ -221,9 +221,11 @@ void ansi_c_convert_typet::read_rec(const typet &type)
221221
// We turn ID_frontend_pointer to ID_pointer
222222
// Pointers have a width, much like integers,
223223
// which is added here.
224-
typet tmp(type);
225-
tmp.id(ID_pointer);
226-
tmp.set(ID_width, config.ansi_c.pointer_width);
224+
pointer_typet tmp(type.subtype(), config.ansi_c.pointer_width);
225+
tmp.add_source_location()=type.source_location();
226+
const irep_idt typedef_identifier=type.get(ID_C_typedef);
227+
if(!typedef_identifier.empty())
228+
tmp.set(ID_C_typedef, typedef_identifier);
227229
other.push_back(tmp);
228230
}
229231
else if(type.id()==ID_pointer)

‎src/ansi-c/c_preprocess.cpp‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
2525

2626
#include <util/c_types.h>
2727
#include <util/config.h>
28+
#include <util/invariant.h>
2829
#include <util/message.h>
2930
#include <util/tempfile.h>
3031
#include <util/unicode.h>
@@ -430,14 +431,17 @@ bool c_preprocess_visual_studio(
430431
command_file << "/D__CPROVER__" << "\n";
431432
command_file << "/D__WORDSIZE=" << config.ansi_c.pointer_width << "\n";
432433

433-
if(config.ansi_c.pointer_width==64)
434+
if(pointer_diff_type()==signed_long_long_int_type())
434435
{
435436
command_file << "\"/D__PTRDIFF_TYPE__=long long int\"" << "\n";
436437
// yes, both _WIN32 and _WIN64 get defined
437438
command_file << "/D_WIN64" << "\n";
438439
}
439440
else
440441
{
442+
DATA_INVARIANT(
443+
pointer_diff_type()==signed_int_type(),
444+
"Pointer difference expected to be int typed");
441445
command_file << "/D__PTRDIFF_TYPE__=int" << "\n";
442446
command_file << "/U_WIN64" << "\n";
443447
}

‎src/ansi-c/padding.cpp‎

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -73,20 +73,15 @@ mp_integer alignment(const typet &type, const namespacet &ns)
7373
type.id()==ID_signedbv ||
7474
type.id()==ID_fixedbv ||
7575
type.id()==ID_floatbv ||
76-
type.id()==ID_c_bool)
76+
type.id()==ID_c_bool ||
77+
type.id()==ID_pointer)
7778
{
78-
std::size_t width=to_bitvector_type(type).get_width();
79-
result=width%8?width/8+1:width/8;
79+
result=pointer_offset_size(type, ns);
8080
}
8181
else if(type.id()==ID_c_enum)
8282
result=alignment(type.subtype(), ns);
8383
else if(type.id()==ID_c_enum_tag)
8484
result=alignment(ns.follow_tag(to_c_enum_tag_type(type)), ns);
85-
else if(type.id()==ID_pointer)
86-
{
87-
std::size_t width=config.ansi_c.pointer_width;
88-
result=width%8?width/8+1:width/8;
89-
}
9085
else if(type.id()==ID_symbol)
9186
result=alignment(ns.follow(type), ns);
9287
else if(type.id()==ID_c_bit_field)

‎src/cpp/cpp_convert_type.cpp‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -162,9 +162,12 @@ void cpp_convert_typet::read_rec(const typet &type)
162162
else if(type.id()==ID_frontend_pointer)
163163
{
164164
// add width and turn into ID_pointer
165-
typet tmp=type;
166-
tmp.id(ID_pointer);
167-
tmp.set(ID_width, config.ansi_c.pointer_width);
165+
pointer_typet tmp(type.subtype(), config.ansi_c.pointer_width);
166+
tmp.add_source_location()=type.source_location();
167+
if(type.get_bool(ID_C_reference))
168+
tmp.set(ID_C_reference, true);
169+
if(type.get_bool(ID_C_rvalue_reference))
170+
tmp.set(ID_C_rvalue_reference, true);
168171
other.push_back(tmp);
169172
}
170173
else if(type.id()==ID_pointer)

‎src/cpp/cpp_typecheck_type.cpp‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/source_location.h>
1515
#include <util/simplify_expr.h>
1616
#include <util/c_types.h>
17-
#include <util/config.h>
1817

1918
#include <ansi-c/c_qualifiers.h>
2019

@@ -79,12 +78,10 @@ void cpp_typecheckt::typecheck_type(typet &type)
7978
}
8079
else if(type.id()==ID_pointer)
8180
{
82-
// the pointer might have a qualifier, but do subtype first
81+
// the pointer/reference might have a qualifier,
82+
// but do subtype first
8383
typecheck_type(type.subtype());
8484

85-
// we add a width, much like with integers
86-
to_pointer_type(type).set_width(config.ansi_c.pointer_width);
87-
8885
// Check if it is a pointer-to-member
8986
if(type.find("to-member").is_not_nil())
9087
{

‎src/goto-instrument/accelerate/polynomial_accelerator.cpp‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,6 @@ Author: Matt Lewis
3737
#include <util/simplify_expr.h>
3838
#include <util/replace_expr.h>
3939
#include <util/arith_tools.h>
40-
#include <util/config.h>
4140

4241
#include "accelerator.h"
4342
#include "util.h"
@@ -345,9 +344,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced(
345344
return false;
346345
}
347346

348-
unsigned width=to_bitvector_type(var.type()).get_width();
349-
if(var.type().id()==ID_pointer)
350-
width=config.ansi_c.pointer_width;
347+
std::size_t width=to_bitvector_type(var.type()).get_width();
351348
assert(width>0);
352349

353350
for(std::vector<expr_listt>::iterator it=parameters.begin();

‎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, [email protected]
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/flattening/boolbv_update.cpp‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
1212
#include <util/std_expr.h>
1313
#include <util/arith_tools.h>
1414
#include <util/base_type.h>
15-
#include <util/config.h>
1615
#include <util/pointer_offset_size.h>
1716

1817
#include <util/c_types.h>

0 commit comments

Comments
 (0)