lingua-franca 0.10.1
Lingua Franca code generator
Loading...
Searching...
No Matches
org.lflang.analyses.c.IfNormalFormAstVisitor Class Reference

An AST visitor that converts an original AST into the If Normal Form. More...

Inherits org.lflang.analyses.c.CBaseAstVisitor< Void >.

Public Member Functions

T visit (CAst.AstNode tree)
 Visit an AST, and return a user-defined result of the operation.
T visit (CAst.AstNode tree, List< CAst.AstNode > nodeList)
 Visit an AST with a list of other AST nodes holding some information, and return a user-defined result of the operation.
T visitAdditionNode (CAst.AdditionNode node)
 Arithmetic operators.
T visitAssignmentNode (CAst.AssignmentNode node)
Void visitAssignmentNode (CAst.AssignmentNode node, List< CAst.AstNode > conditions)
T visitAstNode (CAst.AstNode node)
 These default implementations are not meant to be used.
T visitAstNodeBinary (CAst.AstNodeBinary node)
T visitAstNodeDynamic (CAst.AstNodeDynamic node)
T visitAstNodeUnary (CAst.AstNodeUnary node)
T visitDivisionNode (CAst.DivisionNode node)
T visitEqualNode (CAst.EqualNode node)
 Comparison operators.
T visitGreaterEqualNode (CAst.GreaterEqualNode node)
T visitGreaterThanNode (CAst.GreaterThanNode node)
T visitIfBlockNode (CAst.IfBlockNode node)
Void visitIfBlockNode (CAst.IfBlockNode node, List< CAst.AstNode > conditions)
T visitIfBodyNode (CAst.IfBodyNode node)
T visitLessEqualNode (CAst.LessEqualNode node)
T visitLessThanNode (CAst.LessThanNode node)
T visitLiteralNode (CAst.LiteralNode node)
T visitLogicalAndNode (CAst.LogicalAndNode node)
T visitLogicalNotNode (CAst.LogicalNotNode node)
T visitLogicalOrNode (CAst.LogicalOrNode node)
T visitMultiplicationNode (CAst.MultiplicationNode node)
T visitNegativeNode (CAst.NegativeNode node)
T visitNotEqualNode (CAst.NotEqualNode node)
T visitOpaqueNode (CAst.OpaqueNode node)
T visitScheduleActionIntNode (CAst.ScheduleActionIntNode node)
Void visitScheduleActionIntNode (CAst.ScheduleActionIntNode node, List< CAst.AstNode > conditions)
T visitScheduleActionNode (CAst.ScheduleActionNode node)
Void visitScheduleActionNode (CAst.ScheduleActionNode node, List< CAst.AstNode > conditions)
T visitSetPortNode (CAst.SetPortNode node)
 LF built-in operations.
Void visitSetPortNode (CAst.SetPortNode node, List< CAst.AstNode > conditions)
T visitStatementSequenceNode (CAst.StatementSequenceNode node)
Void visitStatementSequenceNode (CAst.StatementSequenceNode node, List< CAst.AstNode > conditions)
T visitStateVarNode (CAst.StateVarNode node)
T visitSubtractionNode (CAst.SubtractionNode node)
T visitTriggerIsPresentNode (CAst.TriggerIsPresentNode node)
T visitTriggerValueNode (CAst.TriggerValueNode node)
T visitVariableNode (CAst.VariableNode node)

Public Attributes

CAst.StatementSequenceNode INF = new CAst.StatementSequenceNode()

Detailed Description

An AST visitor that converts an original AST into the If Normal Form.

See "Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers" for details about the If Normal Form (https://link.springer.com/chapter/10.1007/11691617_9).

There are several requirements for an AST to be in INF: 1. There should be a single StatementSequence (SS) root node; 2. Each child of the SS node should be an IfBlockNode; 3. Variables in a subsequent child should be marked as "primed" versions of those in the previous child.

Limitations: 1. The implementation does not take the scope into account. E.g. "int i = 0; { int j = 0; }" is treated the same as "int i = 0; int j = 0;". 2. Due to the above limitation, the implementation assumes that each variable has a unique name. E.g. "{ int i = 0; }{ int i = 0; }" is an ill-formed program.

In this program, visit() is the normalise() in the paper.

Member Function Documentation

◆ visit() [1/2]

T org.lflang.analyses.c.AbstractAstVisitor< T >.visit ( CAst.AstNode tree)
inherited

Visit an AST, and return a user-defined result of the operation.

Parameters
treeThe CAst.AstNode to visit.
Returns
The result of visiting the parse tree.

◆ visit() [2/2]

T org.lflang.analyses.c.AbstractAstVisitor< T >.visit ( CAst.AstNode tree,
List< CAst.AstNode > nodeList )
inherited

Visit an AST with a list of other AST nodes holding some information, and return a user-defined result of the operation.

Parameters
treeThe CAst.AstNode to visit.
nodeListA list of CAst.AstNode passed down the recursive call.
Returns
The result of visiting the parse tree.

◆ visitAdditionNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitAdditionNode ( CAst.AdditionNode node)
inherited

Arithmetic operators.

◆ visitAssignmentNode() [1/2]

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitAssignmentNode ( CAst.AssignmentNode node)
inherited

◆ visitAssignmentNode() [2/2]

Void org.lflang.analyses.c.IfNormalFormAstVisitor.visitAssignmentNode ( CAst.AssignmentNode node,
List< CAst.AstNode > conditions )

◆ visitAstNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitAstNode ( CAst.AstNode node)
inherited

These default implementations are not meant to be used.

They should be overriden by the child class. In theory, this base visitor can be deleted? Let's keep it here for now for consistency.

◆ visitAstNodeBinary()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitAstNodeBinary ( CAst.AstNodeBinary node)
inherited

◆ visitAstNodeDynamic()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitAstNodeDynamic ( CAst.AstNodeDynamic node)
inherited

◆ visitAstNodeUnary()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitAstNodeUnary ( CAst.AstNodeUnary node)
inherited

◆ visitDivisionNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitDivisionNode ( CAst.DivisionNode node)
inherited

◆ visitEqualNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitEqualNode ( CAst.EqualNode node)
inherited

Comparison operators.

◆ visitGreaterEqualNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitGreaterEqualNode ( CAst.GreaterEqualNode node)
inherited

◆ visitGreaterThanNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitGreaterThanNode ( CAst.GreaterThanNode node)
inherited

◆ visitIfBlockNode() [1/2]

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitIfBlockNode ( CAst.IfBlockNode node)
inherited

◆ visitIfBlockNode() [2/2]

Void org.lflang.analyses.c.IfNormalFormAstVisitor.visitIfBlockNode ( CAst.IfBlockNode node,
List< CAst.AstNode > conditions )

◆ visitIfBodyNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitIfBodyNode ( CAst.IfBodyNode node)
inherited

◆ visitLessEqualNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitLessEqualNode ( CAst.LessEqualNode node)
inherited

◆ visitLessThanNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitLessThanNode ( CAst.LessThanNode node)
inherited

◆ visitLiteralNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitLiteralNode ( CAst.LiteralNode node)
inherited

◆ visitLogicalAndNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitLogicalAndNode ( CAst.LogicalAndNode node)
inherited

◆ visitLogicalNotNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitLogicalNotNode ( CAst.LogicalNotNode node)
inherited

◆ visitLogicalOrNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitLogicalOrNode ( CAst.LogicalOrNode node)
inherited

◆ visitMultiplicationNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitMultiplicationNode ( CAst.MultiplicationNode node)
inherited

◆ visitNegativeNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitNegativeNode ( CAst.NegativeNode node)
inherited

◆ visitNotEqualNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitNotEqualNode ( CAst.NotEqualNode node)
inherited

◆ visitOpaqueNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitOpaqueNode ( CAst.OpaqueNode node)
inherited

◆ visitScheduleActionIntNode() [1/2]

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitScheduleActionIntNode ( CAst.ScheduleActionIntNode node)
inherited

◆ visitScheduleActionIntNode() [2/2]

Void org.lflang.analyses.c.IfNormalFormAstVisitor.visitScheduleActionIntNode ( CAst.ScheduleActionIntNode node,
List< CAst.AstNode > conditions )

◆ visitScheduleActionNode() [1/2]

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitScheduleActionNode ( CAst.ScheduleActionNode node)
inherited

◆ visitScheduleActionNode() [2/2]

Void org.lflang.analyses.c.IfNormalFormAstVisitor.visitScheduleActionNode ( CAst.ScheduleActionNode node,
List< CAst.AstNode > conditions )

◆ visitSetPortNode() [1/2]

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitSetPortNode ( CAst.SetPortNode node)
inherited

LF built-in operations.

◆ visitSetPortNode() [2/2]

Void org.lflang.analyses.c.IfNormalFormAstVisitor.visitSetPortNode ( CAst.SetPortNode node,
List< CAst.AstNode > conditions )

◆ visitStatementSequenceNode() [1/2]

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitStatementSequenceNode ( CAst.StatementSequenceNode node)
inherited

◆ visitStatementSequenceNode() [2/2]

Void org.lflang.analyses.c.IfNormalFormAstVisitor.visitStatementSequenceNode ( CAst.StatementSequenceNode node,
List< CAst.AstNode > conditions )

◆ visitStateVarNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitStateVarNode ( CAst.StateVarNode node)
inherited

◆ visitSubtractionNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitSubtractionNode ( CAst.SubtractionNode node)
inherited

◆ visitTriggerIsPresentNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitTriggerIsPresentNode ( CAst.TriggerIsPresentNode node)
inherited

◆ visitTriggerValueNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitTriggerValueNode ( CAst.TriggerValueNode node)
inherited

◆ visitVariableNode()

T org.lflang.analyses.c.CBaseAstVisitor< T >.visitVariableNode ( CAst.VariableNode node)
inherited

Member Data Documentation

◆ INF

CAst.StatementSequenceNode org.lflang.analyses.c.IfNormalFormAstVisitor.INF = new CAst.StatementSequenceNode()
The documentation for this class was generated from the following file:
  • /Users/runner/work/lingua-franca/lingua-franca/core/src/main/java/org/lflang/analyses/c/IfNormalFormAstVisitor.java