package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Iterators.Goto

Control flow abstraction for Goto statements.

Due to its design, MOPSA drives the analysis by iterating inductively on the syntax of the AST. This means that in order to analyze the sequencing of multiple statements, MOPSA analyzes each of them in order, using as precondition to one statement the postcondition of the preceding one.

For example, given a precondition `pre`, MOPSA computes the postcondition of the following program

``` S_1; S_2; S_3; ```

as `exec S_1 pre |> exec S_2 |> exec S_3`.

On the other hand, goto statements can be used to arbitrarily redirect the control flow to other program points, thus they do not fit well in this picture since when a label is reached arbitrary flows may be converging to it. For example in the following program

``` S_1; if (rand) then goto label; S_2; label: S_3; ```

the precondition for the statment S_3 is not just the one coming naturally from the syntax (i.e., the postcondition of S_2), but also the one coming from the goto statement.

To address this issue, MOPSA allows to store additional flows than just the natural one in the Flow structure: when a goto statement is encountered, the natural flow is saved in a new token corresponding to the goto's target and it is reset to ⊥. Later when the target label is reached, all the incoming goto flows are joined with the natural one. In the previous example, the execution of the goto stores in a new token the natural flow and sets it to ⊥. Then when `label` is reached, the natural flow (from S_2) is joined with the flow stored in the goto token. In addition, the goto flow is removed to save memory.

This approach works as long as the control flow graph contains only gotos targeting labels that occur later in the syntax. To see why this is the case, consider the following example:

``` S_1; hdr: if (b) then goto exit; S_body; goto hdr; exit: S_2; ```

In this case, the label `hdr` is executed before the goto, therefore the flow coming from the latter is not available when the former is executed. Notice also that the postconditon of the program contains not only the natural flow, but also a goto flow for the `hdr` label. This is the case as the goto flows are removed when the corresponding label are executed, but this happens before the goto.

To ensure the soundness of the analysis, we need to compute an over-approximation of the flows reaching `hdr`. This is done, by repeating the execution of the program using always the same preconditon, but, crucially, by joining the goto flows with the ones obtained in the previous iterations. This means that in the previous example, the second iteration would reuse the precondition of the first one, but in addition the goto flows from the postconditon of the first iteration are added. This procedure is iterated, possibly with widening, until the goto flows converge.

val name : string

Command line options

val opt_goto_down : bool ref

Enable down iterations for goto

Flow tokens

type MopsaLib.token +=
  1. | T_goto of string
    (*

    Goto environments

    *)

Abstract domain

module Domain : sig ... end

Domain identification

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct