Skip to content

Commit 23d948c

Browse files
Apply miscellaneous refactoring and fixes to goto-harness.
Add error checking (check that the entry function is in the symbol table before the code generation, and make sure that it's present correctly) make sure that doc comments are capitalised, change the signatures of functions to make them stricter in the arguments they accept.
1 parent 2400d10 commit 23d948c

File tree

3 files changed

+48
-23
lines changed

3 files changed

+48
-23
lines changed

src/goto-harness/function_call_harness_generator.cpp

Lines changed: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -72,10 +72,10 @@ struct function_call_harness_generatort::implt
7272
void ensure_harness_does_not_already_exist();
7373
/// Update the goto-model with the new harness function.
7474
void add_harness_function_to_goto_model(code_blockt function_body);
75-
/// declare local variables for each of the parameters of the entry function
75+
/// Declare local variables for each of the parameters of the entry function
7676
/// and return them
7777
code_function_callt::argumentst declare_arguments(code_blockt &function_body);
78-
/// write initialisation code for each of the arguments into function_body,
78+
/// Write initialisation code for each of the arguments into function_body,
7979
/// then insert a call to the entry function with the arguments
8080
void call_function(
8181
const code_function_callt::argumentst &arguments,
@@ -269,7 +269,7 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for(
269269
void function_call_harness_generatort::validate_options(
270270
const goto_modelt &goto_model)
271271
{
272-
if(p_impl->function == ID_empty)
272+
if(p_impl->function == ID_empty_string)
273273
throw invalid_command_line_argument_exceptiont{
274274
"required parameter entry function not set",
275275
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
@@ -283,8 +283,17 @@ void function_call_harness_generatort::validate_options(
283283
" --" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
284284
}
285285

286-
auto function_to_call = goto_model.symbol_table.lookup_ref(p_impl->function);
287-
auto ftype = to_code_type(function_to_call.type);
286+
const auto function_to_call_pointer =
287+
goto_model.symbol_table.lookup(p_impl->function);
288+
if(function_to_call_pointer == nullptr)
289+
{
290+
throw invalid_command_line_argument_exceptiont{
291+
"entry function `" + id2string(p_impl->function) +
292+
"' does not exist in the symbol table",
293+
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
294+
}
295+
const auto &function_to_call = *function_to_call_pointer;
296+
const auto &ftype = to_code_type(function_to_call.type);
288297
for(auto const &equal_cluster : p_impl->function_parameters_to_treat_equal)
289298
{
290299
for(auto const &pointer_id : equal_cluster)

src/goto-harness/recursive_initialization.cpp

Lines changed: 24 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,7 @@ void recursive_initializationt::initialize(
185185

186186
code_blockt recursive_initializationt::build_constructor_body(
187187
const exprt &depth_symbol,
188-
const exprt &result_symbol,
188+
const symbol_exprt &result_symbol,
189189
const optionalt<exprt> &size_symbol,
190190
const optionalt<irep_idt> &lhs_name)
191191
{
@@ -220,7 +220,7 @@ code_blockt recursive_initializationt::build_constructor_body(
220220
}
221221
}
222222

223-
const irep_idt &recursive_initializationt::build_constructor(const exprt &expr)
223+
irep_idt recursive_initializationt::build_constructor(const exprt &expr)
224224
{
225225
// for `expr` of type T builds a declaration of a function:
226226
//
@@ -235,7 +235,9 @@ const irep_idt &recursive_initializationt::build_constructor(const exprt &expr)
235235
{
236236
expr_name = to_symbol_expr(expr).get_identifier();
237237
if(should_be_treated_as_array(*expr_name))
238+
{
238239
size_var = get_associated_size_variable(*expr_name);
240+
}
239241
}
240242
const typet &type = expr.type();
241243
if(type_constructor_names.find(type) != type_constructor_names.end())
@@ -554,7 +556,7 @@ symbol_exprt recursive_initializationt::get_free_function()
554556

555557
code_blockt recursive_initializationt::build_pointer_constructor(
556558
const exprt &depth,
557-
const exprt &result)
559+
const symbol_exprt &result)
558560
{
559561
PRECONDITION(result.type().id() == ID_pointer);
560562
const typet &type = result.type().subtype();
@@ -639,7 +641,7 @@ code_blockt recursive_initializationt::build_pointer_constructor(
639641
}
640642

641643
code_blockt recursive_initializationt::build_array_string_constructor(
642-
const exprt &result) const
644+
const symbol_exprt &result) const
643645
{
644646
PRECONDITION(result.type().id() == ID_pointer);
645647
const typet &type = result.type().subtype();
@@ -668,7 +670,7 @@ code_blockt recursive_initializationt::build_array_string_constructor(
668670

669671
code_blockt recursive_initializationt::build_array_constructor(
670672
const exprt &depth,
671-
const exprt &result)
673+
const symbol_exprt &result)
672674
{
673675
PRECONDITION(result.type().id() == ID_pointer);
674676
const typet &type = result.type().subtype();
@@ -690,7 +692,7 @@ code_blockt recursive_initializationt::build_array_constructor(
690692

691693
code_blockt recursive_initializationt::build_struct_constructor(
692694
const exprt &depth,
693-
const exprt &result)
695+
const symbol_exprt &result)
694696
{
695697
PRECONDITION(result.type().id() == ID_pointer);
696698
const typet &struct_type = result.type().subtype();
@@ -705,8 +707,8 @@ code_blockt recursive_initializationt::build_struct_constructor(
705707
return body;
706708
}
707709

708-
code_blockt
709-
recursive_initializationt::build_nondet_constructor(const exprt &result) const
710+
code_blockt recursive_initializationt::build_nondet_constructor(
711+
const symbol_exprt &result) const
710712
{
711713
PRECONDITION(result.type().id() == ID_pointer);
712714
code_blockt body{};
@@ -718,7 +720,7 @@ recursive_initializationt::build_nondet_constructor(const exprt &result) const
718720

719721
code_blockt recursive_initializationt::build_dynamic_array_constructor(
720722
const exprt &depth,
721-
const exprt &result,
723+
const symbol_exprt &result,
722724
const exprt &size,
723725
const optionalt<irep_idt> &lhs_name)
724726
{
@@ -820,7 +822,19 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
820822

821823
bool recursive_initializationt::needs_freeing(const exprt &expr) const
822824
{
823-
return expr.type().id() == ID_pointer && expr.type().id() != ID_code;
825+
if(expr.type().id() != ID_pointer || expr.type().subtype().id() == ID_code)
826+
return false;
827+
for(auto const &common_arguments_origin : common_arguments_origins)
828+
{
829+
if(common_arguments_origin.has_value() && expr.id() == ID_symbol)
830+
{
831+
auto origin_name =
832+
to_symbol_expr(*common_arguments_origin).get_identifier();
833+
auto expr_name = to_symbol_expr(expr).get_identifier();
834+
return origin_name == expr_name;
835+
}
836+
}
837+
return true;
824838
}
825839

826840
void recursive_initializationt::free_if_possible(

src/goto-harness/recursive_initialization.h

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -173,15 +173,15 @@ class recursive_initializationt
173173
/// \return the body of the constructor
174174
code_blockt build_constructor_body(
175175
const exprt &depth_symbol,
176-
const exprt &result_symbol,
176+
const symbol_exprt &result_symbol,
177177
const optionalt<exprt> &size_symbol,
178178
const optionalt<irep_idt> &lhs_name);
179179

180180
/// Check if a constructor for the type of \p expr already exists and create
181181
/// it if not.
182182
/// \param expr: the expression to be constructed
183183
/// \return name of the constructor function
184-
const irep_idt &build_constructor(const exprt &expr);
184+
irep_idt build_constructor(const exprt &expr);
185185

186186
/// Generic constructor for all pointers: only builds one pointee (not an
187187
/// array) but may recourse in case the pointee contains more pointers, e.g.
@@ -190,26 +190,28 @@ class recursive_initializationt
190190
/// \param result: symbol of the result parameter
191191
/// \return the body of the constructor
192192
code_blockt
193-
build_pointer_constructor(const exprt &depth, const exprt &result);
193+
build_pointer_constructor(const exprt &depth, const symbol_exprt &result);
194194

195195
/// Constructor for structures: simply iterates over members and initialise
196196
/// each one.
197197
/// \param depth: symbol of the depth parameter
198198
/// \param result: symbol of the result parameter
199199
/// \return the body of the constructor
200-
code_blockt build_struct_constructor(const exprt &depth, const exprt &result);
200+
code_blockt
201+
build_struct_constructor(const exprt &depth, const symbol_exprt &result);
201202

202203
/// Default constructor: assigns non-deterministic value of the right type.
203204
/// \param result: symbol of the result parameter
204205
/// \return the body of the constructor
205-
code_blockt build_nondet_constructor(const exprt &result) const;
206+
code_blockt build_nondet_constructor(const symbol_exprt &result) const;
206207

207208
/// Constructor for arrays: simply iterates over elements and initialise
208209
/// each one.
209210
/// \param depth: symbol of the depth parameter
210211
/// \param result: symbol of the result parameter
211212
/// \return the body of the constructor
212-
code_blockt build_array_constructor(const exprt &depth, const exprt &result);
213+
code_blockt
214+
build_array_constructor(const exprt &depth, const symbol_exprt &result);
213215

214216
/// Constructor for dynamic arrays: allocate memory for `n` elements (`n` is
215217
/// random but bounded) and initialise each one.
@@ -220,14 +222,14 @@ class recursive_initializationt
220222
/// \return the body of the constructor
221223
code_blockt build_dynamic_array_constructor(
222224
const exprt &depth,
223-
const exprt &result,
225+
const symbol_exprt &result,
224226
const exprt &size,
225227
const optionalt<irep_idt> &lhs_name);
226228

227229
/// Constructor for strings: as array but the last element is zero.
228230
/// \param result: symbol of the result parameter
229231
/// \return the body of the constructor
230-
code_blockt build_array_string_constructor(const exprt &result) const;
232+
code_blockt build_array_string_constructor(const symbol_exprt &result) const;
231233
};
232234

233235
#endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H

0 commit comments

Comments
 (0)