Goto programs validation #3191

sonodtt · 2018-10-17T09:39:37Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

2019-03-01
NB Will squash prior to merge.
Fairly major changes after review by Kroening.

check for entry-point now disabled
checks for presence of sourcelocation and code.sourcelocation now disabled.
goto_modelt::validate now has default values for validation_mode and goto_model_validation_options

2019-02-27
There will be a follow up PR to this to re-enable the checks for an entry-point ("validate_goto_modelt::entry_point_exists()")
This is temporarily disabled as some (<6) regression tests have no entry point, and in some
cases this is intentional (e.g. testing json-ui warnings)

2018-12-21
The first two commits are not new. Changes to reviews have been put into separate commits - but the last commit is the most consequential as it deals with @daniel.poetzl’s request for a change of location and I break the source location tests out into a new unit test file.

• Relevant to this PR (the bigger picture) are also the remarks on
#751 & more recently on #3188
These are not addressed directly here as such, but I am flagging these as context/reminders for reviewers/ going forward.
In particular:
#3188 (comment)
There are several (hopefully nested but maybe not) ideas of what a "valid" goto-program is that are implicitly assumed by different parts of the code. Part of the point of all of this validity checking was to map out, clarify and correct these. Parts of the code assume that there are no RETURN instructions, parts assume that there are and things like the last instruction (apart from END_INSTRUCTION) should be return. I was asking how your validity checks will cope with this. It seems there are two options:

The caller specifies which kind of goto-program they want to check for.
The check reports some auxiliary flags and the caller then checks these separately.

@peterschrammel added:
There are several kinds of Goto program that (should) form a subset chain.
The transformations in process_Goto_program() go through this chain in several feature reduction passes.
Certain analyses may require a specific kind of Goto program.
So, 'valid' depends on the stage of processing. We should make this explicit.

xbauch · 2018-10-17T10:11:11Z

src/goto-programs/validate_goto_model.cpp

+        const irep_idt &identifier =
+          to_symbol_expr(function_call.function()).get_identifier();
+
+        DATA_CHECK(function_map.find(identifier) != function_map.end(), "");


Please fill the comment (also below).

Done. Thanks!

xbauch · 2018-10-17T10:12:12Z

src/goto-programs/validate_goto_model.cpp

+    DATA_CHECK(
+      fun.second.body.instructions.back().is_end_function(),
+      "last instruction should be of end function type");
+  };


Is the semicolon necessary?

erm..nope! Well spotted.

martin-cs

Right direction but not finished yet.

src/cbmc/cbmc_parse_options.cpp

src/goto-programs/goto_functions.h

src/goto-programs/validate_goto_model.cpp

martin-cs · 2018-10-17T13:58:59Z

src/goto-programs/validate_goto_model.cpp

+  class test_for_function_addresst : public const_expr_visitort
+  {
+  private:
+    const irep_idt match_id{ID_address_of};


??? Why not just use ID_address_of directly?

martin-cs · 2018-10-17T14:03:50Z

src/goto-programs/validate_goto_model.cpp

+      if(!test_for_function_address.identifiers.empty())
+      {
+        for(auto &identifier : test_for_function_address.identifiers)
+          DATA_CHECK(function_map.find(identifier) != function_map.end(),


Does this work for pre-linking goto-programs?

@martin-cs
That got us thinking... and I rewrote the following check (which now has the comments below)
/// Check that goto-programs that have a body end with an END_FUNCTION
/// instruction.
///
/// NB functions that are only declared, and not used will not appear in the
/// function map. Functions that are declared only and used to e.g.
/// initialise a function pointer will have no body.
void check_last_instruction();

karkhaz · 2018-11-07T14:38:43Z

@tautschnig suggested that I chime in here: instructionts have a source_location and also a code->source_location(), but these are often inconsistent (sometimes one of them is nil). I'm wondering whether it should be an invariant that those two fields are always identical. I've been using the below code in various places, but it would be nice if there were a consistency check for this sort of thing:

const source_locationt &sloc_of(const goto_programt::const_targett &ins) const
  {
    return ins->code.source_location().is_not_nil()
             ? ins->code.source_location()
             : ins->source_location;
  }

  source_locationt &sloc_of(const goto_programt::const_targett &ins)
  {
    return const_cast<source_locationt &>(
      static_cast<const dispatch_loop_detectort &>(*this).sloc_of(ins));
  }

  const source_locationt &sloc_of(const goto_programt::instructiont &ins) const
  {
    return ins.code.source_location().is_not_nil() ? ins.code.source_location()
                                                   : ins.source_location;
  }

  source_locationt &sloc_of(const goto_programt::instructiont &ins)
  {
    return const_cast<source_locationt &>(
      static_cast<const dispatch_loop_detectort &>(*this).sloc_of(ins));
  }

Skeleton for well-formedness checking of goto models [blocks: #3118, #3147, #3188, #3191, #3187, #3193]

sonodtt · 2018-11-21T10:48:47Z

@karkhaz Many thanks for bringing this up. A check is now in place - not currently active as the code needs patching to ensure both locations are set. I'll raise an issue for that.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 1fb1129).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102487466

kroening · 2019-02-27T15:46:33Z

src/cbmc/cbmc_parse_options.cpp

+    goto_model.validate(
+      validation_modet::INVARIANT,
+      goto_model_validation_optionst{
+        goto_model_validation_optionst::set_optionst::all_true});


Given how often that all_true option is used, simply make that the default?

Same for INVARIANT?

Done. Also for INVARIANT.

kroening · 2019-02-27T15:48:17Z

src/goto-programs/goto_program.cpp

+      vm,
+      code.source_location().is_not_nil(),
+      "each instruction code field, must have non nil source location");
+


Remove the comma

Note that not every instruction has a code member, so this will fail.

Action taken (after team chat). In commit message (reproduced here in case it helps):

Removed previously disabled checks :
Not every instruction has a code member - so removed checks that both
instruction sourcelocation and code sourcelocation are set and identical
Remove also remaining check that every instruction have a non-nil
sourcelocation as this would have to be optional (if enabled fails
many regression tests). This also simplifies considerably the overall
validation pass (removes much passing around of the options structure).

kroening · 2019-02-27T15:52:23Z

src/goto-programs/validate_goto_model.cpp

+  /// - lhs of every \ref code_function_callt instruction is nil
+  /// - all return types are void (of both calls and functions themselves)
+  void check_returns_removed();
+


Please note #4266 on the return type.

removed in validate_goto_model.cpp

DATA_CHECK( vm, goto_function.type.return_type().id() == ID_empty, "functions must have empty return type");

kroening · 2019-02-27T15:54:37Z

src/goto-programs/validate_goto_model.cpp

+      {
+        const code_function_callt &function_call =
+          to_code_function_call(instr.code);
+        DATA_CHECK(


Use instr.get_function_call().

kroening · 2019-02-27T15:55:09Z

src/goto-programs/validate_goto_model.cpp

+      if(instr.is_function_call())
+      {
+        const auto &function_call = to_code_function_call(instr.code);
+        DATA_CHECK(


kroening · 2019-02-27T15:55:36Z

src/goto-programs/validate_goto_model.cpp

+      // check functions that are called
+      if(instr.is_function_call())
+      {
+        const auto &function_call = to_code_function_call(instr.code);


kroening · 2019-02-27T15:57:15Z

unit/goto-programs/goto_program_instruction.cpp

+    auto &instructions = goto_function.body.instructions;
+
+    goto_programt::instructiont instruction;
+    instruction.make_end_function();


instructiont::make_end_function is deprecated -- use goto_programt::make_end_function

kroening · 2019-02-27T15:58:39Z

unit/goto-programs/goto_program_instruction.cpp

+    goto_programt::instructiont instruction;
+    instruction.make_end_function();
+    instructions.push_back(instruction);
+    instructions.back().source_location.id("id_any_valid_id");


The source_locationt ireps don't have an ID.

kroening · 2019-02-27T15:59:45Z

unit/goto-programs/goto_program_symbol_type_table_consistency.cpp

+    // required as goto_function.validate checks (if a function has a body) that
+    // the last instruction of a function body marks the function's end.
+    goto_programt::instructiont end_function_instruction;
+    end_function_instruction.make_end_function();


Removed previously disabled checks: Not every instruction has a code member - so removed checks that both instruction sourcelocation and code sourcelocation are set and identical Remove also remaining check that every instruction have a non-nil sourcelocation as this would have to be optional (if enabled fails many regression tests). This also simplifies considerably the overall validation pass (removes much passing around of the options structure). Removes check on function return type - this will be preserved (diffblue#4266) goto_model::validate now has default parameters. Minor fixes.

Although additional checks may hold, they have their own unit tests and it is these tests that should fail when these checks fail.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 6ba2cf4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102836757

martin-cs

As a start this is reasonable but there are many invariants it doesn't check (whether variables follow the DECL - use - DEAD cycle, scoping of variables, whether exprt's are well formed, etc.). I presume these will be in follow-up patches.

martin-cs · 2019-03-04T11:13:59Z

src/goto-programs/validate_goto_model.h

+  bool function_pointer_calls_removed = true;
+  bool check_returns_removed = true;
+  bool check_called_functions = true;
+


If this is intended to be comprehensive right now, it should also check for vector and complex. If this is intended to be a general framework then it's not super urgent.

Its a general framework right now - everyone is invited to fill in the additional checks :-)

sonodtt added the do not merge label Oct 17, 2018

sonodtt requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners October 17, 2018 09:39

sonodtt assigned danpoe and unassigned danpoe Oct 17, 2018

xbauch reviewed Oct 17, 2018

View reviewed changes

sonodtt force-pushed the goto_programs-validation branch from f3410eb to 81732d2 Compare October 17, 2018 11:54

sonodtt requested a review from danpoe October 17, 2018 13:09

sonodtt force-pushed the goto_programs-validation branch from 81732d2 to 1de2516 Compare October 17, 2018 13:46

martin-cs requested changes Oct 17, 2018

View reviewed changes

tautschnig added a commit that referenced this pull request Nov 9, 2018

Merge pull request #3123 from danpoe/feature/well-formedness-checking

f08e23b

Skeleton for well-formedness checking of goto models [blocks: #3118, #3147, #3188, #3191, #3187, #3193]

tautschnig assigned sonodtt Nov 10, 2018

sonodtt force-pushed the goto_programs-validation branch 4 times, most recently from 9ccd64d to 1cb3da1 Compare November 21, 2018 10:04

sonodtt removed the do not merge label Nov 21, 2018

sonodtt assigned martin-cs Nov 21, 2018

sonodtt force-pushed the goto_programs-validation branch 4 times, most recently from f56e3c5 to 91ace58 Compare November 21, 2018 14:56

sonodtt assigned martin-cs and unassigned martin-cs Feb 27, 2019

allredj reviewed Feb 27, 2019

View reviewed changes

kroening reviewed Feb 27, 2019

View reviewed changes

Sonny Martin added 4 commits March 1, 2019 14:05

Remove extraneous goto-program checks in unit tests.

a1de5dc

Although additional checks may hold, they have their own unit tests and it is these tests that should fail when these checks fail.

Reorder unit test headers for consistency.

6ba2cf4

sonodtt force-pushed the goto_programs-validation branch from 73e94b4 to 6ba2cf4 Compare March 1, 2019 14:50

allredj reviewed Mar 1, 2019

View reviewed changes

martin-cs approved these changes Mar 4, 2019

View reviewed changes

chrisr-diffblue approved these changes Mar 4, 2019

View reviewed changes

chrisr-diffblue assigned smowton and peterschrammel and unassigned martin-cs and chrisr-diffblue Mar 4, 2019

martin-cs mentioned this pull request Mar 4, 2019

What is a safe overapproximation of an OTHER instruction #4323

Open

peterschrammel approved these changes Mar 4, 2019

View reviewed changes

tautschnig merged commit 2bb84ad into diffblue:develop Mar 4, 2019

Goto programs validation #3191

Goto programs validation #3191

Conversation

sonodtt commented Oct 17, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sonodtt Oct 17, 2018 • edited Loading

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

karkhaz commented Nov 7, 2018

sonodtt commented Nov 21, 2018

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sonodtt Mar 1, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sonodtt commented Oct 17, 2018 •

edited

Loading

sonodtt Oct 17, 2018 •

edited

Loading

sonodtt Mar 1, 2019 •

edited

Loading