Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 76d5fe0

Browse files
kroeningkroening
committedJan 9, 2025·
introduce __CPROVER_map type
This introduces C syntax for a type __CPROVER_map(domain, codomain) where domain is a list of types and codomain is a type. The type is internal, for modeling purposes within our own library only, and hence not added to user-facing documentation. It replaces arrays with size __CPROVER_infinity, which are now deprecated.
1 parent 36b2335 commit 76d5fe0

18 files changed

+152
-7
lines changed
 

‎regression/cbmc/map-type/basic1.c

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
int main()
2+
{
3+
__CPROVER_map(int, int) my_map;
4+
5+
my_map = __CPROVER_lambda
6+
{
7+
int i;
8+
i == 1 ? 10 : 20
9+
};
10+
11+
// should pass
12+
__CPROVER_assert(my_map(1) == 10, "(1)");
13+
__CPROVER_assert(my_map(2) == 20, "(2)");
14+
15+
// should fail
16+
__CPROVER_assert(my_map(0) == 10, "(0)");
17+
18+
return 0;
19+
}

‎regression/cbmc/map-type/basic1.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
basic1.c
3+
4+
^\[.*\] line \d+ \(1\): FAILURE$
5+
^\[.*\] line \d+ \(2\): FAILURE$
6+
^\[.*\] line \d+ \(0\): FAILURE$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
^VERIFICATION FAILED$
10+
--
11+
^warning: ignoring

‎regression/cbmc/map-type/basic2.c

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
__CPROVER_map(int, int) nondet_map();
2+
3+
int main()
4+
{
5+
__CPROVER_map(int, int) my_map = nondet_map();
6+
7+
__CPROVER_assume(my_map(1) == 10);
8+
__CPROVER_assume(my_map(2) == 20);
9+
10+
// should pass
11+
__CPROVER_assert(my_map(1) == 10, "(1)");
12+
__CPROVER_assert(my_map(2) == 20, "(2)");
13+
14+
// should fail
15+
__CPROVER_assert(my_map(0) == 10, "(0)");
16+
17+
return 0;
18+
}

‎regression/cbmc/map-type/basic2.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
basic2.c
3+
4+
^\[.*\] line \d+ \(1\): SUCCESS$
5+
^\[.*\] line \d+ \(2\): SUCCESS$
6+
^\[.*\] line \d+ \(0\): FAILURE$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
^VERIFICATION FAILED$
10+
--
11+
^warning: ignoring

‎src/ansi-c/c_typecheck_base.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
2323

2424
class ansi_c_declarationt;
2525
class c_bit_field_typet;
26+
class mathematical_function_typet;
2627
class shift_exprt;
2728

2829
class c_typecheck_baset:
@@ -261,6 +262,7 @@ class c_typecheck_baset:
261262
virtual void typecheck_code_type(code_typet &type);
262263
virtual void typecheck_typedef_type(typet &type);
263264
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
265+
virtual void typecheck_map_type(mathematical_function_typet &);
264266
virtual void typecheck_typeof_type(typet &type);
265267
virtual void typecheck_array_type(array_typet &type);
266268
virtual void typecheck_vector_type(typet &type);

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2534,6 +2534,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
25342534
function_application_exprt function_application(f_op, expr.arguments());
25352535

25362536
function_application.add_source_location() = expr.source_location();
2537+
function_application.type() = mathematical_function_type.codomain();
25372538

25382539
expr.swap(function_application);
25392540
return;

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -111,6 +111,10 @@ void c_typecheck_baset::typecheck_type(typet &type)
111111
{
112112
typecheck_vector_type(type);
113113
}
114+
else if(type.id() == ID_mathematical_function)
115+
{
116+
typecheck_map_type(to_mathematical_function_type(type));
117+
}
114118
else if(type.id()==ID_custom_unsignedbv ||
115119
type.id()==ID_custom_signedbv ||
116120
type.id()==ID_custom_floatbv ||
@@ -726,6 +730,14 @@ void c_typecheck_baset::typecheck_vector_type(typet &type)
726730
type = new_type.with_source_location(source_location);
727731
}
728732

733+
void c_typecheck_baset::typecheck_map_type(mathematical_function_typet &type)
734+
{
735+
for(auto &t : type.domain())
736+
typecheck_type(t);
737+
738+
typecheck_type(type.codomain());
739+
}
740+
729741
void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
730742
{
731743
// These get replaced by symbol types later.

‎src/ansi-c/expr2c.cpp

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -612,6 +612,28 @@ std::string expr2ct::convert_rec(
612612

613613
return q+dest+d;
614614
}
615+
else if(src.id() == ID_mathematical_function)
616+
{
617+
const mathematical_function_typet &function_type =
618+
to_mathematical_function_type(src);
619+
std::string dest = CPROVER_PREFIX "map(";
620+
bool first = true;
621+
for(auto &t : function_type.domain())
622+
{
623+
if(first)
624+
first = false;
625+
else
626+
dest += ", ";
627+
628+
dest += convert(t);
629+
}
630+
631+
dest += ", ";
632+
dest += convert(function_type.codomain());
633+
dest += ")";
634+
635+
return q + dest + d;
636+
}
615637
else if(src.id()==ID_constructor ||
616638
src.id()==ID_destructor)
617639
{

‎src/ansi-c/parser.y

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -198,6 +198,7 @@ int yyansi_cerror(const std::string &error);
198198
%token TOK_CLRCALL "__clrcall"
199199
%token TOK_FORALL "forall"
200200
%token TOK_EXISTS "exists"
201+
%token TOK_LAMBDA "lambda"
201202
%token TOK_ACSL_FORALL "\\forall"
202203
%token TOK_ACSL_EXISTS "\\exists"
203204
%token TOK_ACSL_LAMBDA "\\lambda"
@@ -206,6 +207,7 @@ int yyansi_cerror(const std::string &error);
206207
%token TOK_CPROVER_BITVECTOR "__CPROVER_bitvector"
207208
%token TOK_CPROVER_FLOATBV "__CPROVER_floatbv"
208209
%token TOK_CPROVER_FIXEDBV "__CPROVER_fixedbv"
210+
%token TOK_CPROVER_MAP "__CPROVER_map"
209211
%token TOK_CPROVER_ATOMIC "__CPROVER_atomic"
210212
%token TOK_CPROVER_BOOL "__CPROVER_bool"
211213
%token TOK_CPROVER_THROW "__CPROVER_throw"
@@ -506,6 +508,14 @@ quantifier_expression:
506508
mto($$, $5);
507509
PARSER.pop_scope();
508510
}
511+
| TOK_LAMBDA compound_scope '{' declaration comma_expression '}'
512+
{
513+
$$=$1;
514+
set($$, ID_lambda);
515+
parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($4)) } ));
516+
mto($$, $5);
517+
PARSER.pop_scope();
518+
}
509519
;
510520

511521
cprover_contract_loop_invariant:
@@ -1111,6 +1121,7 @@ type_specifier:
11111121
| typedef_type_specifier
11121122
| typeof_type_specifier
11131123
| atomic_type_specifier
1124+
| map_type_specifier
11141125
;
11151126

11161127
declaration_qualifier_list:
@@ -1554,6 +1565,18 @@ array_of_construct:
15541565
{ $$=$1; stack_type($$).add_subtype().swap(parser_stack($2)); }
15551566
;
15561567

1568+
map_type_specifier:
1569+
TOK_CPROVER_MAP '(' type_specifier ',' type_specifier ')'
1570+
{
1571+
$$=$1;
1572+
parser_stack($$).id(ID_mathematical_function);
1573+
irept domain{ID_tuple};
1574+
domain.move_to_sub(parser_stack($3));
1575+
parser_stack($$).move_to_sub(domain);
1576+
mts($$, $5);
1577+
}
1578+
;
1579+
15571580
pragma_packed:
15581581
{
15591582
init($$);

‎src/ansi-c/scanner.l

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1319,11 +1319,13 @@ __decltype { if(PARSER.cpp98 &&
13191319
{CPROVER_PREFIX}"atomic" { loc(); return TOK_CPROVER_ATOMIC; }
13201320
{CPROVER_PREFIX}"forall" { loc(); return TOK_FORALL; }
13211321
{CPROVER_PREFIX}"exists" { loc(); return TOK_EXISTS; }
1322+
{CPROVER_PREFIX}"lambda" { loc(); return TOK_LAMBDA; }
13221323
{CPROVER_PREFIX}"array_of" { loc(); return TOK_ARRAY_OF; }
13231324
{CPROVER_PREFIX}"thread_local" { loc(); return TOK_THREAD_LOCAL; }
13241325
{CPROVER_PREFIX}"bitvector" { loc(); return TOK_CPROVER_BITVECTOR; }
13251326
{CPROVER_PREFIX}"floatbv" { loc(); return TOK_CPROVER_FLOATBV; }
13261327
{CPROVER_PREFIX}"fixedbv" { loc(); return TOK_CPROVER_FIXEDBV; }
1328+
{CPROVER_PREFIX}"map" { loc(); return TOK_CPROVER_MAP; }
13271329
{CPROVER_PREFIX}"bool" { loc(); return TOK_CPROVER_BOOL; }
13281330
{CPROVER_PREFIX}"throw" { loc(); return TOK_CPROVER_THROW; }
13291331
{CPROVER_PREFIX}"catch" { loc(); return TOK_CPROVER_CATCH; }

‎src/goto-symex/build_goto_trace.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ static void set_internal_dynamic_object(
124124
if(expr.id()==ID_symbol)
125125
{
126126
const auto &type = expr.type();
127-
if(type.id() != ID_code && type.id() != ID_mathematical_function)
127+
if(type.id() != ID_code)
128128
{
129129
const irep_idt &id = to_ssa_expr(expr).get_original_name();
130130
const symbolt *symbol;

‎src/goto-symex/goto_symex_state.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -234,7 +234,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
234234
const auto &type = as_const(expr).type();
235235

236236
// we never rename function symbols
237-
if(type.id() == ID_code || type.id() == ID_mathematical_function)
237+
if(type.id() == ID_code)
238238
{
239239
rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
240240
return renamedt<exprt, level>{std::move(expr)};

‎src/goto-symex/renaming_level.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -221,7 +221,7 @@ bool check_renaming_l1(const exprt &expr)
221221
{
222222
const auto &type = expr.type();
223223
if(!expr.get_bool(ID_C_SSA_symbol))
224-
return type.id() != ID_code && type.id() != ID_mathematical_function;
224+
return type.id() != ID_code;
225225
if(!to_ssa_expr(expr).get_level_2().empty())
226226
return true;
227227
if(to_ssa_expr(expr).get_original_expr().type() != type)
@@ -262,7 +262,7 @@ bool check_renaming(const exprt &expr)
262262
{
263263
const auto &type = expr.type();
264264
if(!expr.get_bool(ID_C_SSA_symbol))
265-
return type.id() != ID_code && type.id() != ID_mathematical_function;
265+
return type.id() != ID_code;
266266
if(to_ssa_expr(expr).get_level_2().empty())
267267
return true;
268268
if(to_ssa_expr(expr).get_original_expr().type() != type)

‎src/solvers/flattening/boolbv.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -506,6 +506,10 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
506506
if(is_unbounded_array(type))
507507
return true;
508508

509+
// see if it's a function
510+
if(type.id() == ID_mathematical_function)
511+
return true;
512+
509513
const bvt &bv1=convert_bv(expr.rhs());
510514

511515
const irep_idt &identifier=

‎src/solvers/flattening/boolbv_equality.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,13 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
3535
return record_array_equality(expr);
3636
}
3737

38+
// see if it is a function
39+
if(expr.lhs().type().id() == ID_mathematical_function)
40+
{
41+
functions.record(expr);
42+
return prop.new_variable();
43+
}
44+
3845
const bvt &lhs_bv = convert_bv(expr.lhs());
3946
const bvt &rhs_bv = convert_bv(expr.rhs());
4047

‎src/solvers/lowering/functions.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,10 @@ void functionst::record(const function_application_exprt &function_application)
1818
function_application);
1919
}
2020

21+
void functionst::record(const equal_exprt &function_equality)
22+
{
23+
}
24+
2125
void functionst::add_function_constraints()
2226
{
2327
for(const auto &function : function_map)

‎src/solvers/lowering/functions.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,8 @@ class functionst
3131
{
3232
}
3333

34-
void record(const function_application_exprt &function_application);
34+
void record(const function_application_exprt &);
35+
void record(const equal_exprt &);
3536

3637
virtual void finish_eager_conversion()
3738
{

‎src/util/mathematical_types.h

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -73,13 +73,21 @@ class mathematical_function_typet : public type_with_subtypest
7373
{
7474
public:
7575
// the domain of the function is composed of zero, one, or
76-
// many variables, given by their type
76+
// many arguments, given by their type
7777
using domaint = std::vector<typet>;
7878

7979
mathematical_function_typet(const domaint &_domain, const typet &_codomain)
8080
: type_with_subtypest(
8181
ID_mathematical_function,
82-
{type_with_subtypest(irep_idt(), _domain), _codomain})
82+
{type_with_subtypest(irep_idt{ID_tuple}, _domain), _codomain})
83+
{
84+
}
85+
86+
// short-hand for the 1-tuple domain
87+
mathematical_function_typet(const typet &_domain, const typet &_codomain)
88+
: type_with_subtypest(
89+
ID_mathematical_function,
90+
{type_with_subtypest(irep_idt{ID_tuple}, {_domain}), _codomain})
8391
{
8492
}
8593

0 commit comments

Comments
 (0)
Please sign in to comment.