Module dev.civl.mc
Package dev.civl.mc.dynamic.IF

Interface DynamicMemoryLocationSet

public interface DynamicMemoryLocationSet

This class is a immutable data structure that stores a set of memory locations. See also DynamicMemoryLocationSetFactory

Relation to the symbolic value of CIVLMemType: 1. an instance of this class can be converted to a symbolic value of mem type by calling getMemValue(). 2. a symbolic value of mem type can be union-ed with an instance of this class with the method DynamicMemoryLocationSetFactory.addReference(DynamicMemoryLocationSet, SymbolicExpression).

Instances of this class are used to dynamically keep track of read/write sets. Here we just take a note for where in the CIVL code base, write/read operation will be recorded: Where write sets are collected:

  • The private methods in CommonExecutor, there are two of them: assignCore and assignLHS
  • invalid reference 
    ImmutableStateFactory#deallocate(dev.civl.mc.state.IF.State, SymbolicExpression, int, int, int)
  • executeMalloc and malloc in CommonExecutor

    • TODO: can all the following go through the executor's assign() ?
  • LibmpiExecutor.executeNewGcomm(dev.civl.mc.state.IF.State, int, java.lang.String, dev.civl.mc.model.IF.expression.Expression[], dev.civl.sarl.IF.expr.SymbolicExpression[], dev.civl.mc.model.IF.CIVLSource) (TODO: is this needed to be recorded ?)
  • LibtimeExecutor.executeLocalTime(dev.civl.mc.state.IF.State, int, dev.civl.mc.model.IF.expression.Expression[], dev.civl.sarl.IF.expr.SymbolicExpression[])
  • CommonExecutor.executeNextInDomain(dev.civl.mc.state.IF.State, int, dev.civl.mc.model.IF.statement.DomainIteratorStatement) (TODO: this one needs some special non-concretet handling)
  • LibcivlcExecutor.executeNextTimeCount(dev.civl.mc.state.IF.State, int, java.lang.String, dev.civl.mc.model.IF.expression.Expression[], dev.civl.sarl.IF.expr.SymbolicExpression[])
Where read sets are collected: at CommonExecutor.executeStatement(dev.civl.mc.state.IF.State, int, dev.civl.mc.model.IF.statement.Statement) method; Note also, read sets always contains write sets.

  • Method Summary

    Modifier and Type
    Method
    Description
    DynamicMemoryLocationSet
    apply(dev.civl.sarl.IF.UnaryOperator<dev.civl.sarl.IF.expr.SymbolicExpression> operator)
    Apply an UnaryOperator on the set of memory location references.
    dev.civl.sarl.IF.expr.SymbolicExpression
    getMemValue()
     

  • Method Details

    • getMemValue

      dev.civl.sarl.IF.expr.SymbolicExpression getMemValue()
      Returns:
      a symbolic expression of CIVLType.getDynamicType(dev.civl.sarl.IF.SymbolicUniverse) which contains all the references to objects that are stored in this write set.

    • apply

      DynamicMemoryLocationSet apply(dev.civl.sarl.IF.UnaryOperator<dev.civl.sarl.IF.expr.SymbolicExpression> operator)

      Apply an UnaryOperator on the set of memory location references. If the operator changes nothing, return this instance.

      Parameters:
      operator -
      Returns:
      An instance whose references are obtained by applying the operator on ones of this