Basic reductions

Universal reductions (both for CFA declaration and instance)

RemoveLocationsWithNoIncomingTransition

Removes the locations with no incoming transition.

Pattern to match

G loc loc temp1->loc none loc->temp2 loc->temp2 loc->temp2

  • location loc
    • no incoming transition
    • not frozen, nor initial or end location
    • has no frozen outgoing transition
Modification
  • all outgoing transitions of loc are deleted
  • location loc is deleted

OverlapVarAssignments

CFA instance and CFA declaration (latter with name OverlapAssignments) reduction. This reduction tries to merge consecutive transitions by moving the variable assignments of the second transition to the first one.

Pattern to match

G loc1 loc1 loc2 loc2 loc1->loc2 tA [c] /VA1:=EA1;  VA2:=EA2;  ... loc3 loc3 loc2->loc3 tB [TRUE] /VB1:=EB1;  VB2:=EB2;  ... loc2->l1 no l0->loc2 no

  • assignment transition tA
    • may have a guard (c)
    • source=loc1, target=loc2
    • has variable assignments VA1:=EA1; VA2:=EA2; ...
    • not frozen
  • assignment transition tB
    • no guard (TRUE literal)
    • source=loc2, target=loc3
    • has variable assignments VB1:=EB1; VB2:=EB2; ...
    • not frozen
  • location loc2
    • 1 incoming transition (t1)
    • 1 outgoing transition (t2)
    • not frozen, not initial location, not end location
  • no conflict between the variable assignments, i.e.,
    • Vars(VA)Vars(EB)=Vars(VA) \cap Vars(EB) = \emptyset (the variables assigned in tA are not read in tB)
    • Vars(VB)Vars(EA)=Vars(VB) \cap Vars(EA) = \emptyset (the variables assigned in tB are not read in tA)
    • Vars(VA)Vars(VB)=Vars(VA) \cap Vars(VB) = \emptyset (the variables assigned in tA are not assigned in tB)
    • Note: VA=iVAiVA = \bigcup_{i}{VA_i}, VB=iVBiVB = \bigcup_{i}{VB_i}, EA=iEAiEA = \bigcup_{i}{EA_i}, EB=iEBiEB = \bigcup_{i}{EB_i}.
Modification
  • all assignments of tB (VB1:=EB1; VB2:=EB2; ...) are moved to tA
  • target of transition tA is modified to loc3 (instead of loc2)
  • location loc2 is deleted
  • transition tB deleted
Result

G loc1 loc1 loc3 loc3 loc1->loc3 tA [c] /VA1:=EA1;  VA2:=EA2;  ...  VB1:=EB1;  VB2:=EB2;  ...

RemoveEmptyTransitions

Merges the two ends of the transitions where the guard is a constant true literal and there is no variable assignment.

Pattern to match

G loc2 loc2 temp3->loc2 none loc1 loc1 loc1->temp1 none loc1->loc2 t [TRUE] /--- loc2->temp2 loc2->temp2 loc2->temp2

  • assignment transition t
    • guard: 'TRUE'
    • not frozen
    • source: loc1, target: loc2
    • has no assignments
  • location loc1
    • not frozen, not initial location, not end location
    • 1 outgoing transition (t)
  • location loc2
    • not frozen, not initial location, not end location
    • 1 incoming transition (t)
Modification
  • transition t is deleted
  • all outgoing transitions of loc2 are moved to loc1
  • location loc2 is deleted
  • The CFD reduction will move the annotations of loc2 to loc1. The CFI reduction assumes that there are no annotations.
Result

G loc1 loc1 loc1->temp2 loc1->temp2 loc1->temp2

CFA instance reductions

ConditionPushDown

It aims to push guard conditions deeper, essentially merging nested conditional branches and to reduce the number of locations.

Pattern to match

G loc2 loc2 dummy4->loc2 none loc1 loc1 loc1->loc2 t [c] loc2->dummy1 t1 [c1] loc2->dummy2 t2 [c2] loc2->dummy3 ...

  • assignment transition t
    • has no variable assignment
    • has guard (c)
    • source=loc1, target=loc2
    • not frozen
  • location loc1
    • has 0..* (any) incoming transition
    • has 1..* (at least one) outgoing transition (including t)
    • not frozen
  • location loc2
    • exactly 1 incoming transition (t)
    • 2.. outgoing assignment* transitions (with guards c1, c2, ...)
    • not frozen
Modification
  • all outgoing transitions of loc2 will be extended with "c AND" and their source changed do loc1
  • location loc2 deleted
  • transition t deleted
Result

G loc1 loc1 loc1->dummy1 t1 [c AND c1] loc1->dummy2 t2 [c AND c2] loc1->dummy3 ...

RemoveEmptyConditionalBranch

Removes unnecessary parallel empty transitions.

Pattern to match

G loc1 loc1 loc_invis1->loc1 loc_invis2->loc1 loc_invis3->loc1 loc2 loc2 loc1->loc2 t1 [c1] /--- loc1->loc2 t2 [c2 == not c1]    /---

  • location loc1

    • has exactly 2 outgoing transitions (t1, t2) and they both lead to the same location (loc2)
  • assignment transition t1

    • has a guard c1
    • does not have any variable assignments
    • may be frozen
  • assignment transition t2

    • has a guard c2 which equals to NOT c1
    • does not have any variable assignments
    • not frozen
Modification
  • t1's guard changed to 'TRUE'
  • t2 deleted Note that if t1 is frozen, t2 will still be merged into t1 by modifying its guard.
Result

G loc1 loc1 loc_invis1->loc1 loc_invis2->loc1 loc_invis3->loc1 loc2 loc2 loc1->loc2 t1 [TRUE] /---

RemoveFalseTransitions

CFI reduction. Removes the transitions where the guard is a constant false literal.

Pattern to match

G loc0->loc1 t [FALSE]

  • assignment transition t
    • guard is 'FALSE'
    • not frozen
Modification
  • transition t is deleted

RemoveIdentityAssignments

Removes the variable assignments where the left and right values equal.

Pattern to match

G loc0->loc1 t [c] /...  α := α; (amt)  ...

  • assignment amt
    • not frozen
    • its left and right value equal (α := α)
Modification
  • variable assignment amt is deleted
Result

G loc0->loc1 t [c] /...  ...

RemoveUnreadAssignments

Removes the variable assignments which are not read. I.e., if between the assignment v1 := <Expr1>; and v1 := <Expr2>; there is no reference to variable v1, then the first assignment. The reduction will keep track of assignments of variables while traversing the CFA. If another assignment is found for a variable in a way that:

  • There was no convergence or divergence in the CFA (each location inbetween had exactly 1 incoming and 1 outgoing transition),
  • There was no call transition since the last assignment,
  • There was no reference to the variable since the last assignment,
  • The last assignment is not frozen,

then the previous assignment will be removed.

RemoveUnreadVariables

Reduction that removes the unread variables of the given CFA. A variable will be removed if it is never read (and not frozen), independently from how many times it is assigned (zero, one or several times). If the variable is assigned and none of its assignments are frozen, the assignments are also removed. If any of the assignments of the variable is frozen, the variable will not be removed.

It is assumed that the variables in the requirement are frozen, thus they cannot be removed.

SimplifyTrivialConditionalBranches/1

It translates the trivial conditional branches assigning Boolean variables into (more complex) variable assignments by including the guard directly in the assignment.

Pattern to match

G loc1 loc1 loc_invis1->loc1 loc_invis1->loc1 loc_invis1->loc1 loc2 loc2 loc1->loc2 tA [c1] /boolVar:=α; VA1 loc3 loc3 loc1->loc3 tB [c2 == NOT c1]    /boolVar:=β; VA2

  • location loc1

    • has two outgoing transitions (tA, tB), both assignment transitions
    • not frozen, not initial location, not end location
  • assignment transition tA

    • has a guard c1
    • assigns the expression α to variable boolVar (which has a type BoolType)
      • this assignment is not frozen
    • may have additional variable assignments (VA1)
  • assignment transition tB

    • has a guard c2 which equals to NOT c1
    • assigns the expression β to variable boolVar (which has a type BoolType)
      • this assignment is not frozen
    • may have additional variable assignments (VA2)
  • The boolVar variable cannot be used in c1 or c2. (In this case the extraction of the assignment would alter the satisfaction of the guard c1 and/or c2.)
Modification
  • creates a new location loc0
  • creates a new assignment transition t0 from loc0 to loc1
  • creates a new assignment boolVar := (c1 AND α) OR (NOT c1 AND β) attached to t0
  • removes the assignments of boolVar from tA and tB
Result

G loc0 loc0 loc_invis1->loc0 loc_invis1->loc0 loc_invis1->loc0 loc1 loc1 loc0->loc1 t0 [TRUE] /boolVar:=(c1 AND α) OR (NOT c1 AND β); loc2 loc2 loc1->loc2 tA [c1] /VA1 loc3 loc3 loc1->loc3 tB [c2 == not c1] /VA2

SimplifyTrivialConditionalBranches/2

It translates the trivial conditional branches assigning Boolean variables into (more complex) variable assignments by including the guard directly in the assignment.

Pattern to match

G loc1 loc1 loc_invis1->loc1 loc_invis1->loc1 loc_invis1->loc1 loc2 loc2 loc1->loc2 tA [c1] /boolVar:=α; VA1 loc3 loc3 loc1->loc3 tB [c2 == not c1]    /VA2

  • location loc1

    • has two outgoing transitions (tA, tB), both assignment transitions
    • not frozen, not initial location, not end location
  • assignment transition tA

    • has a guard c1
    • assigns the expression α to variable boolVar (which has a type BoolType)
      • this assignment is not frozen
    • may have additional variable assignments (VA1)
  • assignment transition tB

    • has a guard c2 which equals to NOT c1
    • DOES NOT assign the variable boolVar
    • may have variable assignments (VA2)
Modification
  • creates a new location loc0
  • creates a new assignment transition t0 from loc0 to loc1
  • creates a new assignment boolVar := (c1 AND α) OR (NOT c1 AND boolVar) attached to t0
  • removes the assignment of boolVar from tA
Result

G loc0 loc0 loc_invis1->loc0 loc_invis1->loc0 loc_invis1->loc0 loc1 loc1 loc0->loc1 t0 [TRUE] /boolVar:=(c1 AND α) OR (NOT c1 AND boolVar);             loc2 loc2 loc1->loc2 tA [c1] /VA1 loc3 loc3 loc1->loc3 tB [c2 == not c1] /VA2

ExpressionSimplification

Simplifies logic and arithmetic expressions.

  • Negation expressions (UnaryLogicExpression with operator=NEG):
    • !(FALSE) --> TRUE
    • !(TRUE) --> FALSE
  • AND expressions (BinaryLogicExpression with operator=AND):
    • TRUE AND right --> right
    • left AND TRUE --> left
    • left AND FALSE --> FALSE
    • FALSE AND right --> FALSE
    • left AND left --> left
    • left AND (NOT left) --> FALSE
    • (NOT right) AND right --> FALSE
    • (a OR b) AND (a OR c) --> a AND (b OR c) (in all 4 combinations)
    • (a AND b) AND (a AND c) --> (a AND b) ANDc (in all 4 combinations)
  • OR expressions (BinaryLogicExpression with operator=OR):
    • FALSE OR right --> right
    • left OR FALSE --> left
    • left OR TRUE --> TRUE
    • TRUE OR right --> TRUE
    • left OR left --> left
    • left OR (NOT left) --> TRUE
    • (NOT right) OR right --> TRUE
    • (a OR b) OR (a OR c) --> (a OR b) OR c (in all 4 combinations)
  • IMPLIES expressions (BinaryLogicExpression with operator=IMPLIES):
    • FALSE IMPLIES right --> TRUE
    • TRUE IMPLIES right --> right
  • equality expressions (ComparisonExpression with operator=EQUALS):
    • alpha == alpha --> TRUE
    • alpha == TRUE --> alpha
  • non-equality expressions (ComparisonExpression with operator=NOT_EQUALS):
    • alpha != alpha --> FALSE
  • binary arithmetic expressions and comparisons: replaces computable subtrees with the computed literals (e.g. 120 / 5 --> 24; TRUE == FALSE --> FALSE, 2 > 1 --> TRUE).

ExpressionPropagation

Replaces the references to variables in guards and variable assignment right values to the definition of the referred variable, if possible. E.g. the sequence v1 := TRUE; v2 := v1; can be simplified to v1 := TRUE; v2 := TRUE;. If it is instantiated with constantPropagationOnly=true, only constants (literals) can be substituted. If constantPropagationOnly=false, expressions can also be propagated, i.e., v1 := a OR b; v2 := v1; can be reduced to v1 := a OR b; v2 := a OR b;.

The reduction infers for each transition the values of variables at the end of the transition based on the guards and variable assignments. For example, based on a transition with guard [a = TRUE AND b = FALSE] and assignment c := a AND d it can be inferred that a = TRUE; b = FALSE; c = TRUE and d. This information (held by a propagation table) is propagated throughout the whole CFA and updated at each transition accordingly. In case of forks (i.e., a location has multiple outgoing transitions), the same propagation table is propagated to all outgoing transitions. In case of merges (i.e., a location has multiple incoming transitions), the propagation tables computed for each incoming transitions are combined (intersected), i.e., their conflicting values are removed. For instance, the combination of a=1; b=2; c=3 and a=2; c=3 is c=3. In case it is not possible to calculate the propagation tables for each incoming transition (e.g., in case there is a loop in the CFA), the propagation is continued with an empty propagation table from that location.

Whenever an expression is recorded in the propagation table, it is simplified using the ExpressionSimplification.trySimplifySubtree() method. When the expression propagation replaces a variable with a propagated value, the whole expression subtree where the replacement happened will be simplified using the ExpressionSimplification.trySimplifySubtree() method.

Currently, the following information is used for the expression propagation reduction:

  • Variable assignments, if they are deterministic
  • Guards, if they are in one of the following forms: [<variable> = <expr>], [<expr> = <variable>], [<boolean_variable>], [NOT <boolean_variable>], or the AND connection of any of these.

The expression propagation shall never create conflicts. For instance, if the propagation table contains [a = c] and a transition has the variable assignments b := a and c := d, the a shall not be replaced by c, as it would cause conflicting variable assignments: b := c; c := d; which is forbidden.

Example.

Take the following SCL code as example. (Assume that b1, b2, b3 are BOOL variables, i1, i2, i3 are INT variables.)

b1 := TRUE;
b2 := b1 AND I0.0;
b3 := b1 AND b2;

i1 := 5;
i2 := i2 * 3;
i3 := i1 + i2;

If it is translated into CFA and then expression propagation is used with constantPropagationOnly=true, the result will be equivalent to having the following code translated into CFA:

b1 := TRUE;
b2 := TRUE; // simplified from 'TRUE AND I0.0'
b3 := TRUE; // simplified from 'TRUE AND TRUE'

i1 := 5;
i2 := 15; // simplified from '5 * 3'
i3 := 20; // simplified from '5 + 15'

Notice that even if only the propagation of constants (literals) was permitted, due to the automated expression simplification it was able to propagate values for variables whose definition originally contained non-literals (e.g., b2 := b1 AND I0.0; was possible to be propagated even though I0.0 is not a literal).

Example: propagation of guard values. Not only variable assignments can be the source of information for expression propagation. Take the following SCL code as example:

IF I0.0 = TRUE AND I0.1 = FALSE THEN
        b1 := I0.0;
      b2 := I0.1;
END_IF;
b3 := b1;

If it is translated into CFA and then expression propagation is used, the result will be equivalent to having the following code translated into CFA:

IF I0.0 = TRUE AND I0.1 = FALSE THEN
        b1 := TRUE;
      b2 := FALSE;
END_IF;
b3 := b1;

Example: propagation over conditional locations. Expressions can be propagated over forks and merges too.

Take the following SCL code as example:

a := 1;
IF b > 2 THEN
  c := b;
ELSE
  d := b - 1;
END_IF;
e := a;

If it is translated into CFA and then expression propagation is used, the result will be equivalent to having e := 1; in the last line of the example code.

CoiReduction

The cone of influence (COI) reduction explores the dependencies between variables, then removes the variables which the requirement does not depend on. For this, two kinds of dependencies are defined.

  • There is an assignment dependency between the variables a and b if a has an assignment which refers to the value of b (e.g., a := 2 * b;). In this case a is a dependent variable which depends on b.
  • There is a control dependency between the variables a and b if a has an assignment which is conditional, depending on the value of b. For example, if there is an assignment a := c + d; on a transition which includes b in its guard. Note that a variable v can have control dependency on variables which are not present in the guard of the transition assigning v. To determine the control dependencies an over-approximating heuristic is used. For this first the unconditional locations are identified. A location is unconditional if every path from the initial location will go through the given location. The control dependencies for a given assignment of a variable are determined based on the guards between the nearest unconditional location before the place of assignment and the transition of assignment.

The main steps of the algorithm are the following:

  1. First, the reduction will find all frozen variables. The variables present in frozen assignments will be made frozen too.
  2. Then, it will collect the variable dependencies using VariableDependencies.collect(). For diagnostic purposes, the variable dependency graph created this way can be visualized using PrintVarDepGraph.print().
  3. Next, it will collect the needed variables. A variable is needed if it is frozen, or if there is an already needed variable which depends on it (either through an assignment or a control dependency). Here, a fixed point is computed.
  4. The unnecessary variables are removed:
    • The assignments assigning unnecessary variables are removed.
    • Guards containing unnecessary variables are replaced with [TRUE].
    • The last step may have lead to parallel transitions having [TRUE] guards and no assignments. They will be removed.
    • If there are any more uses of the unnecessary variables (which is unexpected), they are removed and logged (with Warning severity).
    • Finally, the unnecessary variables are removed.

Example. Take the following SCL code as example:

FUNCTION coi_func1 : INT
    VAR
        b, c, d : INT;
        x, y, z : INT;
    END_VAR

    IF x > 0 THEN
        y := z;
    END_IF;

    IF b > 0 THEN
        d := c;
    END_IF;

    //#ASSERT d > 0
END_FUNCTION

If it is translated into CFA and then expression propagation is used, the result will be equivalent to having the following code translated into CFA:

FUNCTION coi_func1 : INT
    VAR
        b, c, d : INT;
    END_VAR

   // 'x', 'y' and 'z' are not needed

    IF b > 0 THEN
        // 'b' is needed because it is a control dependency of 'd'
        // 'c' is needed because it is an assignment dependency of 'd'
        d := c;
    END_IF;

    //#ASSERT d > 0
    // 'd' is needed because of the requirement
END_FUNCTION

results matching ""

    No results matching ""