From 76d5fe0e2afee8d6267ad0e79f5ce9050ef55d73 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 11 Jun 2022 12:00:17 +0100 Subject: [PATCH] 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. --- regression/cbmc/map-type/basic1.c | 19 ++++++++++++++++++ regression/cbmc/map-type/basic1.desc | 11 +++++++++++ regression/cbmc/map-type/basic2.c | 18 +++++++++++++++++ regression/cbmc/map-type/basic2.desc | 11 +++++++++++ src/ansi-c/c_typecheck_base.h | 2 ++ src/ansi-c/c_typecheck_expr.cpp | 1 + src/ansi-c/c_typecheck_type.cpp | 12 +++++++++++ src/ansi-c/expr2c.cpp | 22 +++++++++++++++++++++ src/ansi-c/parser.y | 23 ++++++++++++++++++++++ src/ansi-c/scanner.l | 2 ++ src/goto-symex/build_goto_trace.cpp | 2 +- src/goto-symex/goto_symex_state.cpp | 2 +- src/goto-symex/renaming_level.cpp | 4 ++-- src/solvers/flattening/boolbv.cpp | 4 ++++ src/solvers/flattening/boolbv_equality.cpp | 7 +++++++ src/solvers/lowering/functions.cpp | 4 ++++ src/solvers/lowering/functions.h | 3 ++- src/util/mathematical_types.h | 12 +++++++++-- 18 files changed, 152 insertions(+), 7 deletions(-) create mode 100644 regression/cbmc/map-type/basic1.c create mode 100644 regression/cbmc/map-type/basic1.desc create mode 100644 regression/cbmc/map-type/basic2.c create mode 100644 regression/cbmc/map-type/basic2.desc diff --git a/regression/cbmc/map-type/basic1.c b/regression/cbmc/map-type/basic1.c new file mode 100644 index 00000000000..d48a79f0b7a --- /dev/null +++ b/regression/cbmc/map-type/basic1.c @@ -0,0 +1,19 @@ +int main() +{ + __CPROVER_map(int, int) my_map; + + my_map = __CPROVER_lambda + { + int i; + i == 1 ? 10 : 20 + }; + + // should pass + __CPROVER_assert(my_map(1) == 10, "(1)"); + __CPROVER_assert(my_map(2) == 20, "(2)"); + + // should fail + __CPROVER_assert(my_map(0) == 10, "(0)"); + + return 0; +} diff --git a/regression/cbmc/map-type/basic1.desc b/regression/cbmc/map-type/basic1.desc new file mode 100644 index 00000000000..8818678b8c2 --- /dev/null +++ b/regression/cbmc/map-type/basic1.desc @@ -0,0 +1,11 @@ +CORE +basic1.c + +^\[.*\] line \d+ \(1\): FAILURE$ +^\[.*\] line \d+ \(2\): FAILURE$ +^\[.*\] line \d+ \(0\): FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc/map-type/basic2.c b/regression/cbmc/map-type/basic2.c new file mode 100644 index 00000000000..5042885db1c --- /dev/null +++ b/regression/cbmc/map-type/basic2.c @@ -0,0 +1,18 @@ +__CPROVER_map(int, int) nondet_map(); + +int main() +{ + __CPROVER_map(int, int) my_map = nondet_map(); + + __CPROVER_assume(my_map(1) == 10); + __CPROVER_assume(my_map(2) == 20); + + // should pass + __CPROVER_assert(my_map(1) == 10, "(1)"); + __CPROVER_assert(my_map(2) == 20, "(2)"); + + // should fail + __CPROVER_assert(my_map(0) == 10, "(0)"); + + return 0; +} diff --git a/regression/cbmc/map-type/basic2.desc b/regression/cbmc/map-type/basic2.desc new file mode 100644 index 00000000000..a42938569e2 --- /dev/null +++ b/regression/cbmc/map-type/basic2.desc @@ -0,0 +1,11 @@ +CORE +basic2.c + +^\[.*\] line \d+ \(1\): SUCCESS$ +^\[.*\] line \d+ \(2\): SUCCESS$ +^\[.*\] line \d+ \(0\): FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index dc0b11a209a..5d64a18f101 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com class ansi_c_declarationt; class c_bit_field_typet; +class mathematical_function_typet; class shift_exprt; class c_typecheck_baset: @@ -261,6 +262,7 @@ class c_typecheck_baset: virtual void typecheck_code_type(code_typet &type); virtual void typecheck_typedef_type(typet &type); virtual void typecheck_c_bit_field_type(c_bit_field_typet &type); + virtual void typecheck_map_type(mathematical_function_typet &); virtual void typecheck_typeof_type(typet &type); virtual void typecheck_array_type(array_typet &type); virtual void typecheck_vector_type(typet &type); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 35bc45cb257..828e20599d4 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2534,6 +2534,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call( function_application_exprt function_application(f_op, expr.arguments()); function_application.add_source_location() = expr.source_location(); + function_application.type() = mathematical_function_type.codomain(); expr.swap(function_application); return; diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 3e3121b0f40..a224fa97a43 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -111,6 +111,10 @@ void c_typecheck_baset::typecheck_type(typet &type) { typecheck_vector_type(type); } + else if(type.id() == ID_mathematical_function) + { + typecheck_map_type(to_mathematical_function_type(type)); + } else if(type.id()==ID_custom_unsignedbv || type.id()==ID_custom_signedbv || type.id()==ID_custom_floatbv || @@ -726,6 +730,14 @@ void c_typecheck_baset::typecheck_vector_type(typet &type) type = new_type.with_source_location(source_location); } +void c_typecheck_baset::typecheck_map_type(mathematical_function_typet &type) +{ + for(auto &t : type.domain()) + typecheck_type(t); + + typecheck_type(type.codomain()); +} + void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) { // These get replaced by symbol types later. diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 07003ead306..a2368c22450 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -612,6 +612,28 @@ std::string expr2ct::convert_rec( return q+dest+d; } + else if(src.id() == ID_mathematical_function) + { + const mathematical_function_typet &function_type = + to_mathematical_function_type(src); + std::string dest = CPROVER_PREFIX "map("; + bool first = true; + for(auto &t : function_type.domain()) + { + if(first) + first = false; + else + dest += ", "; + + dest += convert(t); + } + + dest += ", "; + dest += convert(function_type.codomain()); + dest += ")"; + + return q + dest + d; + } else if(src.id()==ID_constructor || src.id()==ID_destructor) { diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 59e320f7112..d02bf60741a 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -198,6 +198,7 @@ int yyansi_cerror(const std::string &error); %token TOK_CLRCALL "__clrcall" %token TOK_FORALL "forall" %token TOK_EXISTS "exists" +%token TOK_LAMBDA "lambda" %token TOK_ACSL_FORALL "\\forall" %token TOK_ACSL_EXISTS "\\exists" %token TOK_ACSL_LAMBDA "\\lambda" @@ -206,6 +207,7 @@ int yyansi_cerror(const std::string &error); %token TOK_CPROVER_BITVECTOR "__CPROVER_bitvector" %token TOK_CPROVER_FLOATBV "__CPROVER_floatbv" %token TOK_CPROVER_FIXEDBV "__CPROVER_fixedbv" +%token TOK_CPROVER_MAP "__CPROVER_map" %token TOK_CPROVER_ATOMIC "__CPROVER_atomic" %token TOK_CPROVER_BOOL "__CPROVER_bool" %token TOK_CPROVER_THROW "__CPROVER_throw" @@ -506,6 +508,14 @@ quantifier_expression: mto($$, $5); PARSER.pop_scope(); } + | TOK_LAMBDA compound_scope '{' declaration comma_expression '}' + { + $$=$1; + set($$, ID_lambda); + parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($4)) } )); + mto($$, $5); + PARSER.pop_scope(); + } ; cprover_contract_loop_invariant: @@ -1111,6 +1121,7 @@ type_specifier: | typedef_type_specifier | typeof_type_specifier | atomic_type_specifier + | map_type_specifier ; declaration_qualifier_list: @@ -1554,6 +1565,18 @@ array_of_construct: { $$=$1; stack_type($$).add_subtype().swap(parser_stack($2)); } ; +map_type_specifier: + TOK_CPROVER_MAP '(' type_specifier ',' type_specifier ')' + { + $$=$1; + parser_stack($$).id(ID_mathematical_function); + irept domain{ID_tuple}; + domain.move_to_sub(parser_stack($3)); + parser_stack($$).move_to_sub(domain); + mts($$, $5); + } + ; + pragma_packed: { init($$); diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index ad408dbeb31..19503f51b8f 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1319,11 +1319,13 @@ __decltype { if(PARSER.cpp98 && {CPROVER_PREFIX}"atomic" { loc(); return TOK_CPROVER_ATOMIC; } {CPROVER_PREFIX}"forall" { loc(); return TOK_FORALL; } {CPROVER_PREFIX}"exists" { loc(); return TOK_EXISTS; } +{CPROVER_PREFIX}"lambda" { loc(); return TOK_LAMBDA; } {CPROVER_PREFIX}"array_of" { loc(); return TOK_ARRAY_OF; } {CPROVER_PREFIX}"thread_local" { loc(); return TOK_THREAD_LOCAL; } {CPROVER_PREFIX}"bitvector" { loc(); return TOK_CPROVER_BITVECTOR; } {CPROVER_PREFIX}"floatbv" { loc(); return TOK_CPROVER_FLOATBV; } {CPROVER_PREFIX}"fixedbv" { loc(); return TOK_CPROVER_FIXEDBV; } +{CPROVER_PREFIX}"map" { loc(); return TOK_CPROVER_MAP; } {CPROVER_PREFIX}"bool" { loc(); return TOK_CPROVER_BOOL; } {CPROVER_PREFIX}"throw" { loc(); return TOK_CPROVER_THROW; } {CPROVER_PREFIX}"catch" { loc(); return TOK_CPROVER_CATCH; } diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 7e4013f5b6e..ab515bcee64 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -124,7 +124,7 @@ static void set_internal_dynamic_object( if(expr.id()==ID_symbol) { const auto &type = expr.type(); - if(type.id() != ID_code && type.id() != ID_mathematical_function) + if(type.id() != ID_code) { const irep_idt &id = to_ssa_expr(expr).get_original_name(); const symbolt *symbol; diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 9ac435c89a4..4f2819fc0ae 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -234,7 +234,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) const auto &type = as_const(expr).type(); // we never rename function symbols - if(type.id() == ID_code || type.id() == ID_mathematical_function) + if(type.id() == ID_code) { rename(expr.type(), to_symbol_expr(expr).get_identifier(), ns); return renamedt{std::move(expr)}; diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index 7109f4b0c09..37b6ee2b476 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -221,7 +221,7 @@ bool check_renaming_l1(const exprt &expr) { const auto &type = expr.type(); if(!expr.get_bool(ID_C_SSA_symbol)) - return type.id() != ID_code && type.id() != ID_mathematical_function; + return type.id() != ID_code; if(!to_ssa_expr(expr).get_level_2().empty()) return true; if(to_ssa_expr(expr).get_original_expr().type() != type) @@ -262,7 +262,7 @@ bool check_renaming(const exprt &expr) { const auto &type = expr.type(); if(!expr.get_bool(ID_C_SSA_symbol)) - return type.id() != ID_code && type.id() != ID_mathematical_function; + return type.id() != ID_code; if(to_ssa_expr(expr).get_level_2().empty()) return true; if(to_ssa_expr(expr).get_original_expr().type() != type) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 38f856898be..84c5a5b5515 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -506,6 +506,10 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr) if(is_unbounded_array(type)) return true; + // see if it's a function + if(type.id() == ID_mathematical_function) + return true; + const bvt &bv1=convert_bv(expr.rhs()); const irep_idt &identifier= diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index 8e604fe9ac1..9ab3b324bd9 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -35,6 +35,13 @@ literalt boolbvt::convert_equality(const equal_exprt &expr) return record_array_equality(expr); } + // see if it is a function + if(expr.lhs().type().id() == ID_mathematical_function) + { + functions.record(expr); + return prop.new_variable(); + } + const bvt &lhs_bv = convert_bv(expr.lhs()); const bvt &rhs_bv = convert_bv(expr.rhs()); diff --git a/src/solvers/lowering/functions.cpp b/src/solvers/lowering/functions.cpp index 152b223ad5a..ca226d8147f 100644 --- a/src/solvers/lowering/functions.cpp +++ b/src/solvers/lowering/functions.cpp @@ -18,6 +18,10 @@ void functionst::record(const function_application_exprt &function_application) function_application); } +void functionst::record(const equal_exprt &function_equality) +{ +} + void functionst::add_function_constraints() { for(const auto &function : function_map) diff --git a/src/solvers/lowering/functions.h b/src/solvers/lowering/functions.h index 1ee2e373767..5fbbb346b47 100644 --- a/src/solvers/lowering/functions.h +++ b/src/solvers/lowering/functions.h @@ -31,7 +31,8 @@ class functionst { } - void record(const function_application_exprt &function_application); + void record(const function_application_exprt &); + void record(const equal_exprt &); virtual void finish_eager_conversion() { diff --git a/src/util/mathematical_types.h b/src/util/mathematical_types.h index 48d4438b12e..ab680e2dd15 100644 --- a/src/util/mathematical_types.h +++ b/src/util/mathematical_types.h @@ -73,13 +73,21 @@ class mathematical_function_typet : public type_with_subtypest { public: // the domain of the function is composed of zero, one, or - // many variables, given by their type + // many arguments, given by their type using domaint = std::vector; mathematical_function_typet(const domaint &_domain, const typet &_codomain) : type_with_subtypest( ID_mathematical_function, - {type_with_subtypest(irep_idt(), _domain), _codomain}) + {type_with_subtypest(irep_idt{ID_tuple}, _domain), _codomain}) + { + } + + // short-hand for the 1-tuple domain + mathematical_function_typet(const typet &_domain, const typet &_codomain) + : type_with_subtypest( + ID_mathematical_function, + {type_with_subtypest(irep_idt{ID_tuple}, {_domain}), _codomain}) { }