Module dev.civl.mc
Package dev.civl.mc.model.IF

Interface ModelFactory

public interface ModelFactory
The factory to create all model components. Usually this is the only way model components will be created.

A model consists of a set of functions, including a designated "system" function which is where the execution of the program begins. To create a model, first create the system function using

invalid reference 
#function(CIVLSource, Identifier, List, CIVLType, Scope, Location)
. A function has a name, parameters, a return type, a containing scope (which is null only in the case of the system function), and a start location. The start location is a location that serves as the beginning of the function's body, and will have one or more outgoing statements.

All methods to create statements have a parameter for the location that is the origin location for that statement. Before the new statement is returned, it will be added as an outgoing statement to the specified location. Thus, to add the first statement to a function, call the method to create the new statement and pass the function's start location as a parameter.

After constructing the system function, use model(CIVLSource, CIVLFunction, Program) to create the model. Additional functions can then be created in the same manner and added to the model with Model.addFunction(CIVLFunction).

  • Method Details

    • addressOfExpression

      AddressOfExpression addressOfExpression(CIVLSource source, LHSExpression operand)
      Returns a new address-of expression (invalid input: '&e') with given operand.
      Parameters:
      source - The CIVL source of the expression
      operand - the operand of the address-of operator
      Returns:
      the address-of expression with given operand

    • binaryExpression

      BinaryExpression binaryExpression(CIVLSource source, BinaryExpression.BINARY_OPERATOR operator, Expression left, Expression right)
      A binary expression. One of {+,-,*,\,invalid input: '<',invalid input: '<'=,==,!=,invalid input: '&'invalid input: '&',||,%}
      Parameters:
      source - The CIVL source
      operator - The binary operator.
      left - The left operand.
      right - The right operand.
      Returns:
      The binary expression.

    • booleanExpression

      Expression booleanExpression(Expression expression) throws dev.civl.mc.model.common.ModelFactoryException
      Convert an expression to be of boolean-type. The resulting expression will always be boolean-valued. If the expression evaluates to a numeric type, the result will be the equivalent of expression!=0. Used for evaluating expression in conditions.
      Parameters:
      expression - The expression to be translated.
      Returns:
      The boolean expression
      Throws:
      dev.civl.mc.model.common.ModelFactoryException - if the given expression doesn't have boolean type

    • numericExpression

      Expression numericExpression(Expression expression) throws dev.civl.mc.model.common.ModelFactoryException
      Translates an expression to be of numeric-type (i.e., int or real). Basically, if the given expression has boolean type, then it is converted to a cast expression ((int)expression). Otherwise, if it is not of numeric type, an exception will be thrown.
      Parameters:
      expression -
      Returns:
      the numeric representation of the given expression
      Throws:
      dev.civl.mc.model.common.ModelFactoryException - if the given expression doesn't have boolean or numeric type

    • arithmeticableExpression

      Expression arithmeticableExpression(Expression expression) throws dev.civl.mc.model.common.ModelFactoryException
      Translates an expression to be of the type for arithmetic operations i.e. either translate to a comparableExpression(Expression) or make sure the expression has one of the following types:
      • pointer
      • set of pointer
      • array
      Parameters:
      expression -
      Returns:
      the arithmeticable representation of the given expression
      Throws:
      dev.civl.mc.model.common.ModelFactoryException - if the given expression doesn't have boolean or arithmeticable type

    • comparableExpression

      Expression comparableExpression(Expression expression) throws dev.civl.mc.model.common.ModelFactoryException
      Translates an expression to be of the type for comparable operations i.e. either translate to a numericExpression(Expression) or make sure the expression has scope type.
      Parameters:
      expression -
      Returns:
      the comparable representation of the given expression
      Throws:
      dev.civl.mc.model.common.ModelFactoryException - if the given expression doesn't have boolean or comparable type

    • booleanLiteralExpression

      BooleanLiteralExpression booleanLiteralExpression(CIVLSource source, boolean value)
      A boolean literal expression.
      Parameters:
      source - The CIVL source
      value - True or false.
      Returns:
      The boolean literal expression.

    • boundVariableExpression

      BoundVariableExpression boundVariableExpression(CIVLSource source, Identifier name, CIVLType type)
      An expression for a bound variable.
      Parameters:
      source - The source file information for this expression.
      name - The name of the bound variable being referenced.
      type - The type of the bound variable being referenced.
      Returns:
      The new bound variable expression.

    • charLiteralExpression

      CharLiteralExpression charLiteralExpression(CIVLSource sourceOf, char value)
      Creates a character literal expression with the given character value.
      Parameters:
      sourceOf - The source of the new expression
      value - The character value of the expression
      Returns:
      a new character literal expression with the given character value.

    • conditionalExpression

      ConditionalExpression conditionalExpression(CIVLSource source, Expression condition, Expression trueBranch, Expression falseBranch)
      The ternary conditional expression ("?" in C).
      Parameters:
      source - The CIVL source
      condition - The condition being evaluated in this conditional.
      trueBranch - The expression returned if the condition evaluates to true.
      falseBranch - The expression returned if the condition evaluates to false.
      Returns:
      The conditional expression.

    • castExpression

      CastExpression castExpression(CIVLSource source, CIVLType type, Expression expression)
      Create a cast expression
      Parameters:
      source - The CIVL source information of the cast expression
      type - The type to which the expression is cast.
      expression - The expression being cast to a new type.
      Returns:
      The cast expression created by this method

    • dereferenceExpression

      DereferenceExpression dereferenceExpression(CIVLSource source, Expression pointer)
      Returns a new dereference expression (*p) with operand pointer.
      Parameters:
      source - The CIVL source
      pointer - The operand of the dereference operator, an expression with pointer type
      Returns:
      The dereference expression with given operand

    • dotExpression

      DotExpression dotExpression(CIVLSource source, Expression struct, int fieldIndex)
      A dot expression is a reference to a struct field.
      Parameters:
      source - The CIVL source
      struct - The struct being referenced.
      fieldIndex - The field index (indexed from 0).
      Returns:
      The dot expression.

    • dynamicTypeOfExpression

      DynamicTypeOfExpression dynamicTypeOfExpression(CIVLSource source, CIVLType type)
      Returns a "DynamicTypeOf" expression with the given type argument. When evaluated in a state s, it returns an symbolic expression wrapping a symbolic type which is the type determined by the static type in the given state.
      Parameters:
      source - source code reference
      type - static type argument
      Returns:
      the DynamicTypeOf expression with given argument

    • functionIdentifierExpression

      FunctionIdentifierExpression functionIdentifierExpression(CIVLSource source, CIVLFunction function)
      creates a function identifier expression.
      Parameters:
      source -
      function -
      Returns:
      the new function identifier expression of the given function

    • hereOrRootExpression

      HereOrRootExpression hereOrRootExpression(CIVLSource source, boolean isRoot)
      Parameters:
      source -
      isRoot - true if the expression to be created is $root; otherwise, $here
      Returns:
      a new here or root expression

    • initialValueExpression

      InitialValueExpression initialValueExpression(CIVLSource source, Variable variable)
      Returns an "initial value" expression for the given variable. This is an expression which returns the initial value for the variable. It is used to initialize a variable by assigning it to the variable. The type of this expression is the type of the variable.
      Parameters:
      source -
      variable -
      Returns:
      The initial value expression

    • integerLiteralExpression

      IntegerLiteralExpression integerLiteralExpression(CIVLSource source, BigInteger value)
      An integer literal expression.
      Parameters:
      source - The CIVL source
      value - The (arbitrary precision) integer value.
      Returns:
      The integer literal expression.

    • nullPointerExpression

      Expression nullPointerExpression(CIVLPointerType pointerType, CIVLSource source)
      Generate a null pointer expression
      Parameters:
      pointerType - The type of the pointer
      source - The CIVL source of the expression
      Returns:
      The null pointer expression

    • procnullExpression

      ProcnullExpression procnullExpression(CIVLSource source)
      Creates a $proc_null constant expression.
      Parameters:
      source - The source of the $proc_null
      Returns:
      the new $proc_null constant expression

    • quantifiedExpression

      QuantifiedExpression quantifiedExpression(CIVLSource source, QuantifiedExpression.Quantifier quantifier, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)
      Creates a new quantified expression.
      Parameters:
      source - The source file information for this expression.
      quantifier - The quantifier for this quantified expression. One of {FORALL, EXISTS, UNIFORM}.
      boundVariableList - the list of bound variables as long as their domains (optional)
      restriction - The boolean-valued expression involving the bound variable which is expected to be true
      expression - The body expression.
      Returns:
      The new quantified expression

    • arrayLambdaExpression

      ArrayLambdaExpression arrayLambdaExpression(CIVLSource source, CIVLArrayType arrayType, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)
      Creates a new array lambda expression.
      Parameters:
      source - the source file information for this expression.
      arrayType - the type of this array lambda, which should be some array type
      boundVariableList - the list of bound variables as long as their domains (optional)
      restriction - the boolean-valued expression involving the bound variable which is expected to be true
      expression - the body expression.
      Returns:
      the new array lambda expression

    • lambdaExpression

      LambdaExpression lambdaExpression(CIVLSource source, CIVLFunctionType functionType, Variable variable, Expression expression)
      Creates a new lambda expression.
      Parameters:
      source - the source file information for this expression.
      functionType - the type of this lambda, which should be some function type
      expression - the body expression.
      boundVariableList - the list of bound variables as long as their domains (optional)
      Returns:
      the new array lambda expression

    • extendedQuantifiedExpression

      ExtendedQuantifiedExpression extendedQuantifiedExpression(CIVLSource source, CIVLType type, dev.civl.abc.ast.node.IF.acsl.ExtendedQuantifiedExpressionNode.ExtendedQuantifier quant, Expression lo, Expression hi, Expression function)
      Parameters:
      source -
      type -
      quant -
      lo -
      hi -
      function -
      Returns:

    • realLiteralExpression

      RealLiteralExpression realLiteralExpression(CIVLSource source, BigDecimal value)
      A real literal expression.
      Parameters:
      source - The CIVL source
      value - The (arbitrary precision) real value.
      Returns:
      The real literal expression.

    • regularRangeExpression

      RegularRangeExpression regularRangeExpression(CIVLSource source, Expression low, Expression high, Expression step)
      Creates a regular range expression, which has the syntax low .. high # step. step should be non-zero, and (high-low)/step >= 0 .
      Parameters:
      source - the source code information of the regular range expression.
      low - the lower bound of the range
      high - the higher bound of the range
      step - the step of the range
      Returns:
      the new regular range expression with the given lower/upper bounds and step.

    • recDomainLiteralExpression

      RecDomainLiteralExpression recDomainLiteralExpression(CIVLSource source, List<Expression> ranges, CIVLType type)
      Create a rectangular domain expression, which has the form {r1, r2, ..., rm}, where m is the dimension of the domain, and ri (where 1 invalid input: '<'= i invalid input: '<'= m) is a range expression (either regular range or literal range).
      Parameters:
      source - the source code information of the domain expression
      ranges - the list of range expressions that will be used to compose the domain expression
      type - the type of the domain expression
      Returns:
      the new rectangular domain expression.

    • domainGuard

      DomainGuardExpression domainGuard(CIVLSource source, List<Variable> vars, Variable counter, Expression domain)
      Returns a domain guard expression which is boolean expression whose arguments consists of loop variables in a CIVL $for loop and the original domain associate to the loop. It evaluates it to true if and only if the values of those variables are such that at least one more iteration exists.
      Parameters:
      source - the source code information of the domain guard expression
      vars - the list of variables the value of which represent the current element of the domain
      counter - the counter variable for iterating the domain one by one
      domain - the domain
      Returns:
      the new domain guard expression.

    • scopeofExpression

      ScopeofExpression scopeofExpression(CIVLSource source, LHSExpression argument)
      Creates a new $scopeof expression using the given argument.
      Parameters:
      source - The source code element to be used for error report.
      argument - The argument of the scope of expression.
      Returns:
      The new $scopeof expression.

    • selfExpression

      SelfExpression selfExpression(CIVLSource source)
      A self expression. Used to referenced the current process.
      Parameters:
      source - The CIVL source
      Returns:
      A new self expression.

    • sizeofTypeExpression

      SizeofTypeExpression sizeofTypeExpression(CIVLSource source, CIVLType type)
      Returns a new "sizeof(t)" expression.
      Parameters:
      source - source code reference
      type - a CIVL type, the argument to "sizeof"
      Returns:
      the sizeof expression

    • sizeofExpressionExpression

      SizeofExpression sizeofExpressionExpression(CIVLSource source, Expression argument)
      Returns a new expression of the form "sizeof(e)" where is an expression.
      Parameters:
      source - source code reference
      argument - an expression
      Returns:
      a new sizeof expression

    • compoundLiteralExpression

      CompoundLiteralExpression compoundLiteralExpression(CIVLSource source, Scope exprScope, CIVLType type, boolean isStringLiteral)
      Creates a new instance of a compound literal expression.
      Parameters:
      source - the source of the literal expression
      exprScope - the scope of the literal expression
      type - the type of the literal expression
      isStringLiteral - true iff this expression represents a string literal
      Returns:
      the new compound literal expression

    • subscriptExpression

      SubscriptExpression subscriptExpression(CIVLSource source, LHSExpression array, Expression index)
      An expression for an array index operation. e.g. a[i]
      Parameters:
      source - The CIVL source
      array - An expression evaluating to an array.
      index - An expression evaluating to an integer.
      Returns:
      The array index expression.

    • functionCallExpression

      FunctionCallExpression functionCallExpression(CallOrSpawnStatement callStatement)
      creates a system function call expression
      Parameters:
      callStatement -
      Returns:
      the new expression which contains a call to a system function.

    • trueExpression

      Expression trueExpression(CIVLSource source)
      creates a new boolean expression which has the value $true
      Parameters:
      source - the source of the expression
      Returns:
      the new boolean expression which has the value $true

    • systemGuardExpression

      Expression systemGuardExpression(CallOrSpawnStatement sysCall)
      Creates the system guard expression for the given system call statement.

      Precondition: sysCall.isCall == true invalid input: '&'invalid input: '&' sysCall.isSystemCall() == true.

      Parameters:
      sysCall - The system call statement.
      Returns:
      the expression that represents the guard of a system function call

    • unaryExpression

      UnaryExpression unaryExpression(CIVLSource source, UnaryExpression.UNARY_OPERATOR operator, Expression operand)
      A unary expression. One of {-,!}.
      Parameters:
      source - The CIVL source of the expression
      operator - The unary operator.
      operand - The expression to which the operator is applied.
      Returns:
      The unary expression.

    • variableExpression

      VariableExpression variableExpression(CIVLSource source, Variable variable)
      A variable expression.
      Parameters:
      source - The CIVL source
      variable - The variable being referenced.
      Returns:
      The variable expression.

    • abstractFunctionCallExpression

      AbstractFunctionCallExpression abstractFunctionCallExpression(CIVLSource source, AbstractFunction function, List<Expression> arguments)
      An expression for a call to an abstract function.
      Parameters:
      source - The source file information for this expression.
      function - The abstract function being called.
      arguments - The arguments to the function call.
      Returns:
      The new abstract function call expression.

    • derivativeCallExpression

      DerivativeCallExpression derivativeCallExpression(CIVLSource source, AbstractFunction function, List<Pair<Variable,IntegerLiteralExpression>> partials, List<Expression> arguments)
      An expression for a call to the derivative of an abstract function.
      Parameters:
      source - The source file information for this expression.
      function - The abstract function being called.
      partials - The pairs representing which partial derivatives are taken. Each pair is comprised of the variable for the parameter in which the partial derivative is taken, and an integer indicating how many times that partial is taken.
      arguments - The arguments to the function call.
      Returns:
      The new derivative call expression.

    • differentiableExpression

      DifferentiableExpression differentiableExpression(CIVLSource source, AbstractFunction function, int degree, Expression[] lowerBounds, Expression[] upperBounds)
      An expression representing the claim that some function is differentiable. Specifically, the function has degree continuous derivatives on the Cartesian product of the closed intervals specified by the lower and upper bounds.
      Parameters:
      source -
      function -
      degree -
      lowerBounds -
      upperBounds -
      Returns:

    • arraySliceReference

      ArraySliceReference arraySliceReference(ArraySliceReference.ArraySliceKind sliceKind, Expression index)
      creates a new array slice reference.
      Parameters:
      sliceKind - the kind of the array slice
      index - the index expression for the slice, which could be of integer or domain type
      Returns:
      the new array slice reference

    • selfReference

      SelfReference selfReference()
      Returns:
      a self reference

    • structFieldReference

      StructOrUnionFieldReference structFieldReference(int fieldIndex)
      creates a reference to a certain field of a struct
      Parameters:
      fieldIndex - the index of the field referred to
      Returns:
      the new reference to the field at the specified index of a struct

    • memoryUnitExpression

      MemoryUnitExpression memoryUnitExpression(CIVLSource source, Variable variable, CIVLType objetType, MemoryUnitReference reference, boolean writable, boolean hasPinterRef)
      creates a memory unit expression.
      Parameters:
      source - the source of the expression
      variable - the variable that the memory unit corresponds to
      objetType - the type of the object that the memory unit references
      reference - the reference corresponds to the variable
      writable - the access status of the memory unit
      hasPinterRef - does the memory unit contains any pointer reference?
      Returns:
      the new memory unit expression

    • assignStatement

      AssignStatement assignStatement(CIVLSource civlSource, Location source, LHSExpression lhs, Expression rhs, boolean isInitializer)
      An assignment statement.
      Parameters:
      civlSource - The CIVL source
      source - The source location for this statement.
      lhs - The left hand side of the assignment.
      rhs - The right hand side of the assignment.
      isInitializer - True iff the assign statement to create is translated from a the initialization node of variable declaration node.
      Returns:
      A new assignment statement.

    • atomicFragment

      Fragment atomicFragment(Fragment fragment, Location start, Location end)
      Generate an atomic fragment based on a certain fragment, by adding one location at before and after the fragment to denote the boundary of the atomic block
      Parameters:
      fragment - The fragment representing the body of the atomic block
      start - The start location of the atomic node
      end - The end location of the atomic node
      Returns:
      The new fragment with atomic signs

    • atomicEnter

      Statement atomicEnter(Location loc)
      Generate an atomic enter statement
      Parameters:
      loc - the location that is associated with the generated statement
      Returns:
      the generated atomic enter statement

    • atomicExit

      Statement atomicExit(Location loc)
      Generate an atomic exit statement
      Parameters:
      loc - the location that is associated with the generated statement
      Returns:
      the generated atomic exit statement

    • callOrSpawnStatement

      CallOrSpawnStatement callOrSpawnStatement(CIVLSource sourceOf, Location location, boolean isCall, Expression function, List<Expression> arguments, Expression guard, boolean isInitializer)
      Creates a call or spawn statement. In the case of call, it could be a normal function call, or a system function call.
      Parameters:
      sourceOf - The CIVL source of the call or spawn statement
      location - The source location for the call or spawn statement.
      isCall - is this a call statement (not spawn statement)?
      function - The function identifier expression, null if the function is not a variable.
      arguments - The arguments to the function.
      guard - The guard of the statement
      isInitializer - A boolean value indicating that if the return value of the creating call statement will initialize a left-hand side expression
      Returns:
      the new call or spawn statement

    • civlParForEnterStatement

      CivlParForSpawnStatement civlParForEnterStatement(CIVLSource source, Location location, Expression domain, VariableExpression domSize, VariableExpression procsVar, CIVLFunction parProcFunc)
      creates a $parfor enter statement to start the execution of the $parfor.
      Parameters:
      source - the source of the $parfor enter statement
      location - the source location of the $parfor enter statement
      domain - the domain of the $parfor statement
      domSize -
      procsVar - the variable expression representing the array for the references of processes that are to be spawned by the $parfor
      parProcFunc - the function that represents the body of the $parfor
      Returns:
      the new $parfor enter statement

    • gotoBranchStatement

      NoopStatement gotoBranchStatement(CIVLSource civlSource, Location source, String label)
      A goto branch statement is of the form goto label; . When a goto branch statement is executed, no variables will be updated but only the location of the process will be updated to the target of the goto branch statement.
      Parameters:
      civlSource - The source of this goto statement.
      source - The source location of this goto statement.
      label - The label of the target of the goto statement.
      Returns:
      A new goto branch statement.

    • ifElseBranchStatement

      NoopStatement ifElseBranchStatement(CIVLSource civlSource, Location source, Expression guard, boolean isIf)
      An if-else branch statement is introduced to translate if-else statement. It could be either the if-branch statement or the else-branch statement.
      Parameters:
      civlSource - The source of this if-else branch statement.
      source - The source location of this if branch statement.
      guard - The guard of the if-else branch statement. Given an statement like if(c)a;else b; , the guard of the if branch is a, whereas the guard for the else branch is !a.
      isIf - True iff the branch is the if branch, otherwise, it is the else branch.
      Returns:

    • loopBranchStatement

      NoopStatement loopBranchStatement(CIVLSource civlSource, Location source, Expression guard, boolean isTrue, LoopContract loopContract)
      An loop branch statement is introduced when translating a loop. It could be the branch for the loop condition being either true or false.
      Parameters:
      civlSource - The CIVL source of the loop branch statement.
      source - The source location of the loop branch statement.
      guard - The guard of the loop branch statement. Given an statement like while(a)b; , the guard of the loop-true branch is a, whereas the guard for the loop-false branch is !a.
      isTrue - True if the statement is for the loop-true branch, otherwise for the loop-false branch.
      loopContract - The loop contracts attached with this loop. null if no loop contracts attached.
      Returns:

    • mallocStatement

      MallocStatement mallocStatement(CIVLSource civlSource, Location source, LHSExpression lhs, CIVLType staticElementType, Expression scopeExpression, Expression sizeExpression, int mallocId, Expression guard)
      Create a new malloc statement
      Parameters:
      civlSource - The CIVL source
      source - The source location of the malloc statement
      lhs - The left hand side of the malloc statement
      staticElementType - The static element type
      scopeExpression - The expression of the scope
      sizeExpression - The size argument of the malloc statement
      mallocId - The id of the malloc statement
      guard - The guard
      Returns:
      The new malloc statement

    • noopStatement

      NoopStatement noopStatement(CIVLSource civlSource, Location source, Expression expression)
      A noop statement with the default guard of true.
      Parameters:
      civlSource - The CIVL source of the no-op statement
      source - The source location for this noop statement.
      expression - The expression associates with this noop statement.
      Returns:
      A new noop statement with the default guard of true.

    • noopStatementTemporary

      NoopStatement noopStatementTemporary(CIVLSource civlSource, Location source)
      A temporary noop statement with the true guard
      Parameters:
      civlSource - The CIVL source of the no-op statement
      source - The source location for this noop statement.
      Returns:
      A new temporary noop statement with the true guard

    • noopStatementForVariableDeclaration

      NoopStatement noopStatementForVariableDeclaration(CIVLSource civlSource, Location source)
      A temporary noop statement with the true guard
      Parameters:
      civlSource - The CIVL source of the no-op statement
      source - The source location for this noop statement.
      Returns:
      A new temporary noop statement with the true guard

    • noopStatementWtGuard

      NoopStatement noopStatementWtGuard(CIVLSource civlSource, Location source, Expression guard)
      A noop statement with an explicit guard expression.
      Parameters:
      civlSource - The CIVL source of the no-op statement
      source - The source location for this noop statement.
      guard - The guard of the noop statement. Must be non-null. For the default guard of true, use
      invalid reference 
      #noopStatement(CIVLSource, Location)
      .
      Returns:
      A new noop statement.

    • returnFragment

      Fragment returnFragment(CIVLSource civlSource, Location source, Expression expression, CIVLFunction function)
      Create a one-statement fragment that contains the return statement.
      Parameters:
      civlSource - The CIVL source of the return statement
      source - The source location for this return statement.
      expression - The expression being returned. Null if non-existent.
      function - The CIVL function that this return statement belongs to.
      Returns:
      A new fragment.

    • switchBranchStatement

      NoopStatement switchBranchStatement(CIVLSource civlSource, Location source, Expression guard)
      Creates a switch branch statement for the default case, which is a subclass of no-op statement.
      Parameters:
      civlSource - The CIVL source of the default case
      source - The source location for this statement
      guard - The guard of the branch statement
      Returns:
      the new switch branch statement for the default case

    • switchBranchStatement

      NoopStatement switchBranchStatement(CIVLSource civlSource, Location source, Expression guard, Expression label)
      Creates a switch branch statement for a labeled case.
      Parameters:
      civlSource - The CIVL source of the default case
      source - The source location for this statement
      guard - The guard of the branch statement
      label - The label of the case
      Returns:
      the new switch branch statement for the specified case

    • updateStatement

      UpdateStatement updateStatement(CIVLSource source, Location srcLoc, Expression guard, Expression collator, CallOrSpawnStatement call)
      Creates an $update statement.
      Parameters:
      source - the source code information of the statement
      srcLoc - the source location of the $update statement
      guard - the guard of the $update statement.
      collator - the collator of the $update statement.
      call - the function call of the $update statement.
      Returns:
      the new $update statement.

    • updateStatement

      UpdateStatement updateStatement(CIVLSource source, Location srcLoc, Expression guard, Expression collator, CIVLFunction function, Expression[] arguments)

    • sourceOf

      CIVLSource sourceOf(dev.civl.abc.token.IF.Source abcSource)
      Translate ABC source into CIVL source
      Parameters:
      abcSource - The ABC source
      Returns:
      The CIVL source

    • sourceOfToken

      CIVLSource sourceOfToken(dev.civl.abc.token.IF.CivlcToken token)
      Get the CIVL source of a C token
      Parameters:
      token - The C token
      Returns:
      The CIVL source

    • sourceOf

      CIVLSource sourceOf(dev.civl.abc.ast.node.IF.ASTNode node)
      Get the CIVL source of an AST node
      Parameters:
      node - The AST node
      Returns:
      The CIVL source

    • sourceOfBeginning

      CIVLSource sourceOfBeginning(dev.civl.abc.ast.node.IF.ASTNode node)
      Get the CIVL source of the beginning of an AST node
      Parameters:
      node - The AST node
      Returns:
      The CIVL source

    • sourceOfEnd

      CIVLSource sourceOfEnd(dev.civl.abc.ast.node.IF.ASTNode node)
      Get the CIVL source of the end of an AST node
      Parameters:
      node - The AST node
      Returns:
      The CIVL source

    • sourceOfSpan

      CIVLSource sourceOfSpan(dev.civl.abc.token.IF.Source abcSource1, dev.civl.abc.token.IF.Source abcSource2)
      Translate the span of two ABC sources into CIVL source
      Parameters:
      abcSource1 - The first ABC source
      abcSource2 - The second ABC source
      Returns:
      The CIVL source

    • sourceOfSpan

      CIVLSource sourceOfSpan(dev.civl.abc.ast.node.IF.ASTNode node1, dev.civl.abc.ast.node.IF.ASTNode node2)
      Get the CIVL span source of two AST nodes
      Parameters:
      node1 - The first AST node
      node2 - The second AST node
      Returns:
      The CIVL source

    • sourceOfSpan

      CIVLSource sourceOfSpan(CIVLSource source1, CIVLSource source2)
      Get the span of two CIVL sources
      Parameters:
      source1 - The first CIVL source
      source2 - The second CIVL source
      Returns:
      The CIVL source

    • systemSource

      CIVLSource systemSource()
      Returns a source object representing a system-defined object with no link to actual source code. Used for built-in functions, types, etc.
      Returns:
      a system source object

    • atomicLockVariableExpression

      VariableExpression atomicLockVariableExpression()
      This method is used in Enabler when a process resumes from being blocked and wants to get the atomic lock
      Returns:
      The variable expression object of the atomic lock variable

    • abstractFunction

      AbstractFunction abstractFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, int continuity, String attribute)
      Generate an abstract function.
      Parameters:
      source - The CIVL source of the function.
      name - The function name.
      parameters - The parameters of the function.
      returnType - The CIVL return type
      containingScope - The scope that contains the function.
      continuity - The total number of partial derivatives of this function that may be taken.
      attribute - Nullable. The optional attribute attached to the function
      Returns:
      The abstract function.

    • function

      CIVLFunction function(CIVLSource source, boolean isAtomic, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, Location startLocation)
      Create a new function. When the function is constructed, its outermost scope will be created.
      Parameters:
      source - The CIVL source
      isAtomic - Is the function atomic (i.e., declared with $atomic_f)?
      name - The name of this function.
      parameters - The list of parameters.
      returnType - The return type of this function.
      containingScope - The scope containing this function.
      startLocation - The first location in the function.
      Returns:
      The new function.

    • logicFunction

      LogicFunction logicFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType outputType, int[] pointerToHeapMap, Scope containingScope, Expression definition)
      Create a new logic function (LogicFunction).
      Parameters:
      source - The CIVLSource related to this logic function
      name - The name of the logic function
      parameterScope - the scope of the logic function parameters
      parameters - a list of parameters of the logic function
      pointerToHeapMap - see LogicFunction.pointerToHeapVidMap()
      containingScope - the scope where the logic function is defined
      definition - the logic function definition which is an instance of Expression, can be null if it has no definition.
      Returns:
      a new instance of LogicFunction

    • nondetFunction

      CIVLFunction nondetFunction(CIVLSource source, Identifier name, CIVLType returnType, Scope containingScope)

    • identifier

      Identifier identifier(CIVLSource source, String name)
      Get an identifier with the given name.
      Parameters:
      source - The CIVL source of the identifier
      name - The name of this identifier.
      Returns:
      The new identifier

    • location

      Location location(CIVLSource source, Scope scope)
      Create a new location.
      Parameters:
      source - The CIVL source of the location
      scope - The scope containing this location.
      Returns:
      The new location.

    • model

      Model model(CIVLSource source, CIVLFunction system, dev.civl.abc.program.IF.Program program)
      Create a new model.
      Parameters:
      source - The CIVL source of the model
      system - The designated outermost function, called "System."
      Returns:
      A new model

    • scope

      Scope scope(CIVLSource source, Scope parent, List<Variable> variables, CIVLFunction function)
      Create a new scope. This is not used for the outermost scope of a function, because the outermost scope of a function is created when the function is constructed.
      Parameters:
      source - The source of the scope
      parent - The containing scope of this scope. Only null for the outermost scope of the designated "System" function.
      variables - The set of variables in this scope.
      function - The function containing this scope.
      Returns:
      A new scope

    • systemFunction

      SystemFunction systemFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, String libraryName)
      Generate the system function
      Parameters:
      source - The CIVL source of the function
      name - The function name
      parameters - The parameters of the function
      returnType - The CIVL return type
      containingScope - The scope that contains the function
      libraryName - The name of the library that defines the function
      Returns:
      The system function

    • variable

      Variable variable(CIVLSource source, CIVLType type, Identifier name, int vid)
      Create a new variable.
      Parameters:
      source - The CIVL source of the variable
      type - The type of this variable.
      name - The name of this variable.
      vid - The index of this variable in its scope.
      Returns:
      The variable

    • variableAsParameter

      Variable variableAsParameter(CIVLSource source, CIVLType type, Identifier name, int vid)
      Create a new variable which is also a parameter of some function.
      Parameters:
      source - The CIVL source of the variable
      type - The type of this variable.
      name - The name of this variable.
      vid - The index of this variable in its scope.
      Returns:
      The variable

    • model

      Model model()
      Returns the CIVL model built by this model factory.
      Returns:
      the CIVL model built by this model factory.

    • timeCountVariable

      Variable timeCountVariable()

    • brokenTimeVariable

      Variable brokenTimeVariable()

    • setTokenFactory

      void setTokenFactory(dev.civl.abc.token.IF.TokenFactory tokens)
      Set the token factory
      Parameters:
      tokens - The token factory

    • setScopes

      void setScopes(Scope scope)
      Set the system scope, which is the root (static) scope of the model.
      Parameters:
      scope - The system scope of the model

    • typeFactory

      CIVLTypeFactory typeFactory()
      Gets the CIVL type factory associates with this model factory.
      Returns:
      the CIVL type factory

    • universe

      dev.civl.sarl.IF.SymbolicUniverse universe()
      Returns:
      The symbolic universe

    • getProcessId

      int getProcessId(dev.civl.sarl.IF.expr.SymbolicExpression processValue)
      Translate a symbolic process id into an integer. A symbolic process id is a tuple with one element of integer type.
      Parameters:
      processValue - The symbolic object of the process id
      Returns:
      The integer of the process id

    • isProcNull

      boolean isProcNull(dev.civl.sarl.IF.expr.SymbolicExpression procValue)
      Checks if the given process value equals to the $proc_null constant. An error is reported if the given process value is not of $proc type.
      Parameters:
      procValue - The process value to be checked.
      source - The source code element for error report.
      Returns:
      True iff the given process value equals to the $proc_null constant.

    • nullProcessValue

      dev.civl.sarl.IF.expr.SymbolicExpression nullProcessValue()

    • isPocessIdDefined

      boolean isPocessIdDefined(int pid)

    • isProcessIdNull

      boolean isProcessIdNull(int pid)

    • undefinedValue

      dev.civl.sarl.IF.expr.SymbolicExpression undefinedValue(dev.civl.sarl.IF.type.SymbolicType type)
      generate undefined value of a certain type
      Parameters:
      type -
      Returns:

    • isTrue

      boolean isTrue(Expression expression)
      Check if a certain expression is TRUE.
      Parameters:
      expression - The expression to be checked
      Returns:
      True iff the expression is TRUE

    • computeImpactScopeOfLocation

      void computeImpactScopeOfLocation(Location location)
      Computes the impact scope of a location, which is the highest scope that the location accesses. This method has side effect on the location.
      Parameters:
      location - The location whose impact scope is to be computed.

    • newAnonymousVariableForArrayLiteral

      Variable newAnonymousVariableForArrayLiteral(CIVLSource sourceOf, Scope scope, CIVLArrayType type)
      Creates an anonymous variable of array type in a certain scope. An anonymous variable has the name "_anon_i", like "_anon_0", "_anon_1", etc.
      Parameters:
      sourceOf - The source of the variable
      scope - The scope of the new anonymous variable
      type - The type of the new anonymous variable
      Returns:
      the new anonymous variable

    • newAnonymousVariableForConstantArrayLiteral

      Variable newAnonymousVariableForConstantArrayLiteral(CIVLSource sourceOf, CIVLArrayType type, dev.civl.sarl.IF.expr.SymbolicExpression value)
      Creates an anonymous variable of array type in the static constant scope. An anonymous variable has the name "_anon_i", like "_anon_0", "_anon_1", etc.
      Parameters:
      sourceOf - The source of the variable
      type - The type of the new anonymous variable
      value - the value of the array literal
      Returns:
      the new anonymous variable

    • anonFragment

      Fragment anonFragment()
      Returns the current fragment of an assignment statement for an anonymous variable initialization. When translating a string literal or an array literal of characters, if it is used as the initializer of a variable of pointer type, then an anonymous (constant) variable of array of character is created in the top scope (i.e., system scope).
      Returns:

    • clearAnonFragment

      void clearAnonFragment()
      Clear the current anonymous fragment. See anonFragment() for more about anonymous fragments.

    • addAnonStatement

      void addAnonStatement(Statement statment)
      Add the given statement to the anonymous fragment.
      Parameters:
      statment - The statement to be added to the anonymous fragment.

    • functionGuardExpression

      Expression functionGuardExpression(CIVLSource source, Expression function, List<Expression> arguments)

    • civlForEnterFragment

      Fragment civlForEnterFragment(CIVLSource source, Location src, Expression dom, List<Variable> variables, Variable counter)
      Returns a new fragment containing a CivlForStatement.
      Parameters:
      source -
      src -
      dom -
      variables -
      Returns:

    • domSizeVariable

      VariableExpression domSizeVariable(CIVLSource source, Scope scope)

    • parProcsVariable

      VariableExpression parProcsVariable(CIVLSource source, CIVLType type, Scope scope)

    • elaborateDomainPointer

      FunctionIdentifierExpression elaborateDomainPointer()

    • getLiteralDomCounterIdentifier

      Identifier getLiteralDomCounterIdentifier(CIVLSource source, int count)
      Get the name of the counter variable for the for loop on a literal domain
      Returns:
      the identifier wrapping the name of the variable

    • getHideConstant

      dev.civl.sarl.IF.expr.SymbolicConstant getHideConstant()

    • newAnonymousVariable

      Variable newAnonymousVariable(CIVLSource sourceOf, Scope scope, CIVLType type)
      Create a variable of the given type and add it to the given scope.
      Parameters:
      sourceOf -
      scope -
      type -
      Returns:

    • codeAnalyzers

      List<CodeAnalyzer> codeAnalyzers()
      The list of code analyzers associate with this model.
      Returns:

    • setCodeAnalyzers

      void setCodeAnalyzers(List<CodeAnalyzer> analyzers)

    • inputVariables

      List<Variable> inputVariables()

    • addInputVariable

      void addInputVariable(Variable variable)

    • wildcardExpression

      WildcardExpression wildcardExpression(CIVLSource source, CIVLType type)
      Creates a wildcard expression ..., which is only used in contract.
      Parameters:
      source -
      type -
      Returns:

    • loopContract

      LoopContract loopContract(CIVLSource civlSource, Location loopLocation, List<Expression> loopInvariants, List<LHSExpression> loopAssigns, List<Expression> loopVariants)
      Creates a LoopContract instance
      Parameters:
      civlSource - The CIVLSource of the loop contract.
      loopLocation - The Location which identifies the corresponding loop.
      loopInvariants - A set of loop invairant expressions.
      loopAssigns - A set of loop assign expressions.
      loopVariants - A set of loop vairant expressions.
      Returns:

    • leastCommonAncestor

      Scope leastCommonAncestor(Scope s0, Scope s1)

    • nothing

      Nothing nothing(CIVLSource source)

    • staticConstantScope

      Scope staticConstantScope()
      returns the static scope for constants
      Returns:

    • parallelAssignStatement

      ParallelAssignStatement parallelAssignStatement(CIVLSource source, List<Pair<LHSExpression,Expression>> assignPairs)