Skip to content

Idea : Documenting and checking the invariants on goto programs #751

Closed
@martin-cs

Description

@martin-cs

[ Documenting a TODO : Thanks to @thk123 for the prompt, @smowton and @jgwilson42 for previous discussions and @peterschrammel for ideas. ]

There are a number of obvious and less obvious invariants on goto-programs and what "well structured" means. At the moment these are at the stage of fokelore with scraps being documented, which is not exactly an ideal state of affairs. Maybe we could...

  1. Write an is_valid() method for goto_functionst and goto_programt which checks if it is well structured. As @peterschrammel observes, there are various, nested correct forms (have function pointers been removed, have throw/catch been removed, etc.) so it might be good to take parameters to denote which form it should be in.

  2. Add in assert(program.is_valid()) calls at key locations, including after the front-end / load from file, after instrumentation passes and before the back-end engines.

  3. If you want to assume something about the structure of a program, add to the validity check, get it merged and assume away.

@peterschrammel adds:

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions