Skip to content

Commit 7c2e774

Browse files
Petr BauchPetr Bauch
Petr Bauch
authored and
Petr Bauch
committed
Fix based on comments
1 parent 4a740c1 commit 7c2e774

11 files changed

+94
-103
lines changed

‎src/goto-programs/goto_function.h

+2-3
Original file line numberDiff line numberDiff line change
@@ -115,10 +115,9 @@ class goto_functiont
115115
///
116116
/// The validation mode indicates whether well-formedness check failures are
117117
/// reported via DATA_INVARIANT violations or exceptions.
118-
void validate(const symbol_tablet &table, const validation_modet vm) const
118+
void validate(const namespacet &ns, const validation_modet vm) const
119119
{
120-
body.validate(table, vm);
121-
namespacet ns(table);
120+
body.validate(ns, vm);
122121
validate_type_full_pick(type, ns, vm);
123122
}
124123
};

‎src/goto-programs/goto_functions.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -123,12 +123,12 @@ class goto_functionst
123123
///
124124
/// The validation mode indicates whether well-formedness check failures are
125125
/// reported via DATA_INVARIANT violations or exceptions.
126-
void validate(const symbol_tablet &table, const validation_modet vm) const
126+
void validate(const namespacet &ns, const validation_modet vm) const
127127
{
128128
for(const auto &entry : function_map)
129129
{
130130
const goto_functiont &goto_function = entry.second;
131-
goto_function.validate(table, vm);
131+
goto_function.validate(ns, vm);
132132
}
133133
}
134134
};

‎src/goto-programs/goto_model.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ class goto_modelt : public abstract_goto_modelt
102102
/// reported via DATA_INVARIANT violations or exceptions.
103103
void validate(const namespacet &ns, const validation_modet vm) const
104104
{
105-
goto_functions.validate(symbol_table, vm);
105+
goto_functions.validate(ns, vm);
106106
symbol_table.validate();
107107
}
108108
};

‎src/goto-programs/goto_program.cpp

+21-73
Original file line numberDiff line numberDiff line change
@@ -669,57 +669,12 @@ bool goto_programt::instructiont::equals(const instructiont &other) const
669669
}
670670

671671
void goto_programt::instructiont::validate(
672-
const symbol_tablet &table,
672+
const namespacet &ns,
673673
const validation_modet vm) const
674674
{
675-
namespacet ns(table);
676675
validate_code_full_pick(code, ns, vm);
677676
validate_expr_full_pick(guard, ns, vm);
678677

679-
auto evaluates_to_boolean = [](const exprt &e) -> bool {
680-
if(e.type().id() != ID_bool)
681-
return false;
682-
683-
if(e.id() == ID_typecast)
684-
return e.type().id() == ID_bool;
685-
686-
//Boolean constants
687-
if(e.id() == ID_true || e.id() == ID_false)
688-
return true;
689-
if(e.id() == ID_constant)
690-
return true;
691-
692-
//Symbols
693-
if(e.id() == ID_symbol)
694-
return true;
695-
696-
//arithmetic relations
697-
if(e.id() == ID_equal || e.id() == ID_notequal)
698-
return true;
699-
if(e.id() == ID_ieee_float_equal || e.id() == ID_ieee_float_notequal)
700-
return true;
701-
if(e.id() == ID_ge || e.id() == ID_gt)
702-
return true;
703-
if(e.id() == ID_le || e.id() == ID_lt)
704-
return true;
705-
706-
//propositional operators
707-
if(
708-
e.id() == ID_not || e.id() == ID_and || e.id() == ID_or ||
709-
e.id() == ID_implies)
710-
return true;
711-
if(e.id() == ID_exists || e.id() == ID_forall)
712-
return true;
713-
714-
//weird
715-
if(
716-
e.id() == ID_isfinite || e.id() == ID_isnormal || e.id() == ID_isinf ||
717-
e.id() == ID_isnan)
718-
return true;
719-
720-
return false;
721-
};
722-
723678
switch(type)
724679
{
725680
case ASSIGN:
@@ -733,36 +688,22 @@ void goto_programt::instructiont::validate(
733688
targets.empty(),
734689
"assume instruction should not have a target",
735690
source_location);
736-
DATA_CHECK_WITH_DIAGNOSTICS(
737-
evaluates_to_boolean(guard),
738-
"assuming non-boolean condition\n" + guard.pretty(),
739-
source_location);
740691
break;
741692
case ASSERT:
742693
DATA_CHECK_WITH_DIAGNOSTICS(
743694
targets.empty(),
744695
"assert instruction should not have a target",
745696
source_location);
746-
DATA_CHECK_WITH_DIAGNOSTICS(
747-
evaluates_to_boolean(guard),
748-
"asserting non-boolean condition\n" + guard.pretty(),
749-
source_location);
750697
break;
751698
case GOTO:
752699
DATA_CHECK_WITH_DIAGNOSTICS(
753700
has_target(),
754701
"goto instruction expects at least one target",
755702
source_location);
756-
for(const auto &t : targets)
757-
{
758-
DATA_CHECK_WITH_DIAGNOSTICS(
759-
t->is_target() && t->target_number != 0,
760-
"goto target has to be a target",
761-
source_location);
762-
}
703+
//get_target checks that targets.size()==1
763704
DATA_CHECK_WITH_DIAGNOSTICS(
764-
evaluates_to_boolean(guard),
765-
"goto with non-boolean condition\n" + guard.pretty(),
705+
get_target()->is_target() && get_target()->target_number != 0,
706+
"goto target has to be a target",
766707
source_location);
767708
break;
768709
case FUNCTION_CALL:
@@ -782,22 +723,29 @@ void goto_programt::instructiont::validate(
782723
code.get_statement() == ID_dead,
783724
"dead instructions should contain a dead statement",
784725
source_location);
785-
DATA_CHECK_WITH_DIAGNOSTICS(
786-
table.has_symbol(to_code_dead(code).get_identifier()),
787-
"removing unknown symbol: " +
788-
id2string(to_code_dead(code).get_identifier()) + " from scope",
789-
source_location);
726+
{
727+
const symbolt *symbol;
728+
DATA_CHECK_WITH_DIAGNOSTICS(
729+
!ns.lookup(to_code_dead(code).get_identifier(), symbol),
730+
"removing unknown symbol: " +
731+
id2string(to_code_dead(code).get_identifier()) + " from scope",
732+
source_location);
733+
}
790734
break;
791735
case DECL:
792736
DATA_CHECK_WITH_DIAGNOSTICS(
793737
code.get_statement() == ID_decl,
794738
"declaration instructions should contain a declaration statement",
795739
source_location);
796-
DATA_CHECK_WITH_DIAGNOSTICS(
797-
table.has_symbol(to_code_decl(code).get_identifier()),
798-
"declaring unknown symbol: " +
799-
id2string(to_code_decl(code).get_identifier()),
800-
source_location);
740+
{
741+
const symbolt *symbol;
742+
DATA_CHECK_WITH_DIAGNOSTICS(
743+
!ns.lookup(to_code_decl(code).get_identifier(), symbol),
744+
"declaring unknown symbol: " +
745+
id2string(to_code_decl(code).get_identifier()),
746+
source_location);
747+
}
748+
break;
801749
default:
802750
break;
803751
}

‎src/goto-programs/goto_program.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -404,7 +404,7 @@ class goto_programt
404404
///
405405
/// The validation mode indicates whether well-formedness check failures are
406406
/// reported via DATA_INVARIANT violations or exceptions.
407-
void validate(const symbol_tablet &table, const validation_modet vm) const;
407+
void validate(const namespacet &ns, const validation_modet vm) const;
408408
};
409409

410410
// Never try to change this to vector-we mutate the list while iterating
@@ -689,11 +689,11 @@ class goto_programt
689689
///
690690
/// The validation mode indicates whether well-formedness check failures are
691691
/// reported via DATA_INVARIANT violations or exceptions.
692-
void validate(const symbol_tablet &table, const validation_modet vm) const
692+
void validate(const namespacet &ns, const validation_modet vm) const
693693
{
694694
for(const instructiont &ins : instructions)
695695
{
696-
ins.validate(table, vm);
696+
ins.validate(ns, vm);
697697
}
698698
}
699699
};

‎src/util/std_code.h

+4-1
Original file line numberDiff line numberDiff line change
@@ -1106,7 +1106,10 @@ class code_function_callt:public codet
11061106
void check(const validation_modet vm = validation_modet::INVARIANT) const
11071107
{
11081108
DATA_CHECK(
1109-
operands().size() == 3, "function calls must have three operands");
1109+
operands().size() == 3,
1110+
"function calls must have three operands:\n1) expression to store the "
1111+
"returned values\n2) the function being called\n3) the vector of "
1112+
"arguments");
11101113
}
11111114

11121115
void validate(

‎src/util/std_expr.cpp

+45
Original file line numberDiff line numberDiff line change
@@ -211,3 +211,48 @@ const exprt &object_descriptor_exprt::root_object() const
211211

212212
return *p;
213213
}
214+
215+
bool evaluates_to_boolean(const exprt &e)
216+
{
217+
if(e.type().id() != ID_bool)
218+
return false;
219+
220+
if(e.id() == ID_typecast)
221+
return e.type().id() == ID_bool;
222+
223+
//Boolean constants
224+
if(e.id() == ID_true || e.id() == ID_false)
225+
return true;
226+
if(e.id() == ID_constant)
227+
return true;
228+
229+
//Symbols
230+
if(e.id() == ID_symbol)
231+
return true;
232+
233+
//arithmetic relations
234+
if(e.id() == ID_equal || e.id() == ID_notequal)
235+
return true;
236+
if(e.id() == ID_ieee_float_equal || e.id() == ID_ieee_float_notequal)
237+
return true;
238+
if(e.id() == ID_ge || e.id() == ID_gt)
239+
return true;
240+
if(e.id() == ID_le || e.id() == ID_lt)
241+
return true;
242+
243+
//propositional operators
244+
if(
245+
e.id() == ID_not || e.id() == ID_and || e.id() == ID_or ||
246+
e.id() == ID_implies)
247+
return true;
248+
if(e.id() == ID_exists || e.id() == ID_forall)
249+
return true;
250+
251+
//weird
252+
if(
253+
e.id() == ID_isfinite || e.id() == ID_isnormal || e.id() == ID_isinf ||
254+
e.id() == ID_isnan)
255+
return true;
256+
257+
return false;
258+
}

‎unit/goto-programs/goto_program_assume.cpp

+8-11
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ SCENARIO(
1414
"Validation of well-formed assert/assume codes",
1515
"[core][goto-programs][validate]")
1616
{
17-
GIVEN("A program with one assertion")
17+
GIVEN("A program with one assumption")
1818
{
1919
symbol_tablet symbol_table;
2020
const typet type1 = signedbv_typet(32);
@@ -23,38 +23,35 @@ SCENARIO(
2323
symbol.name = symbol_name;
2424
symbol_exprt varx(symbol_name, type1);
2525
exprt val10 = from_integer(10, type1);
26-
plus_exprt x_plus_10(varx, val10);
2726
binary_relation_exprt x_le_10(varx, ID_le, val10);
2827

2928
goto_functiont goto_function;
3029
auto &instructions = goto_function.body.instructions;
31-
instructions.emplace_back(goto_program_instruction_typet::ASSERT);
30+
instructions.emplace_back(goto_program_instruction_typet::ASSUME);
3231

3332
symbol.type = type1;
3433
symbol_table.insert(symbol);
3534
namespacet ns(symbol_table);
35+
instructions.back().make_assertion(x_le_10);
3636

37-
WHEN("Condition evaluates to a Boolean")
37+
WHEN("Instruction has not targets")
3838
{
39-
instructions.back().make_assertion(x_le_10);
4039
THEN("The consistency check succeeds")
4140
{
42-
goto_function.body.validate(symbol_table, validation_modet::INVARIANT);
41+
goto_function.body.validate(ns, validation_modet::INVARIANT);
4342
REQUIRE(true);
4443
}
4544
}
4645

47-
WHEN("Condition does not evaluate to a Boolean")
46+
WHEN("Instruction has a target")
4847
{
49-
instructions.back().make_assertion(x_plus_10);
50-
48+
instructions.back().targets.push_back(instructions.begin());
5149
THEN("The consistency check fails")
5250
{
5351
bool caught = false;
5452
try
5553
{
56-
goto_function.body.validate(
57-
symbol_table, validation_modet::EXCEPTION);
54+
goto_function.body.validate(ns, validation_modet::EXCEPTION);
5855
}
5956
catch(incorrect_goto_program_exceptiont &e)
6057
{

‎unit/goto-programs/goto_program_declaration.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -38,20 +38,21 @@ SCENARIO(
3838

3939
THEN("The consistency check succeeds")
4040
{
41-
goto_function.body.validate(symbol_table, validation_modet::INVARIANT);
41+
goto_function.body.validate(ns, validation_modet::INVARIANT);
4242
REQUIRE(true);
4343
}
4444
}
4545

4646
WHEN("Declaring unknown symbol")
4747
{
48+
namespacet ns(symbol_table);
49+
4850
THEN("The consistency check fails")
4951
{
5052
bool caught = false;
5153
try
5254
{
53-
goto_function.body.validate(
54-
symbol_table, validation_modet::EXCEPTION);
55+
goto_function.body.validate(ns, validation_modet::EXCEPTION);
5556
}
5657
catch(incorrect_goto_program_exceptiont &e)
5758
{

‎unit/goto-programs/goto_program_function_call.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ SCENARIO(
5555

5656
THEN("The consistency check succeeds")
5757
{
58-
goto_function.body.validate(symbol_table, validation_modet::INVARIANT);
58+
goto_function.body.validate(ns, validation_modet::INVARIANT);
5959
REQUIRE(true);
6060
}
6161
}
@@ -70,8 +70,7 @@ SCENARIO(
7070
bool caught = false;
7171
try
7272
{
73-
goto_function.body.validate(
74-
symbol_table, validation_modet::EXCEPTION);
73+
goto_function.body.validate(ns, validation_modet::EXCEPTION);
7574
}
7675
catch(incorrect_goto_program_exceptiont &e)
7776
{

‎unit/goto-programs/goto_program_goto_target.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ SCENARIO(
4242
instructions.front().target_number = 1;
4343
THEN("The consistency check succeeds")
4444
{
45-
goto_function.body.validate(symbol_table, validation_modet::INVARIANT);
45+
goto_function.body.validate(ns, validation_modet::INVARIANT);
4646
REQUIRE(true);
4747
}
4848
}
@@ -54,8 +54,7 @@ SCENARIO(
5454
bool caught = false;
5555
try
5656
{
57-
goto_function.body.validate(
58-
symbol_table, validation_modet::EXCEPTION);
57+
goto_function.body.validate(ns, validation_modet::EXCEPTION);
5958
}
6059
catch(incorrect_goto_program_exceptiont &e)
6160
{

0 commit comments

Comments
 (0)