Source and Sink Specifications for Impact Analysis in Polyspace Code Prover

You can use Polyspace^® Code Prover™ to prove that two objects in your C/C++ program do not impact each other. If you designate the two objects as a source and a sink, a Code Prover analysis can detect if the source values impact the sink values or can prove the absence of impact. An impact occurs if there is an uninterrupted data flow from the source to the sink (or if the value of the source variable determines if the sink variable acquires a specific value).

This topic shows how to define sources and sinks in an impact specification file for impact analysis in Polyspace Code Prover. For more information on the impact analysis workflow, see Prove Absence of Impact Between Objects in C/C++ Program.

XML Structure of Impact Specification File

The XML format for specifying sources and sinks follows this structure:

<?xml version="1.0" encoding="UTF-8"?>
<impact-specifications xmlns="http://www.mathworks.com/PolyspaceImpactSpecifications">
  <!-- Define variables that can act as source or sink>
  <variables>
      <!--Define each variable inside a 'variable' element, assign id -->
        <variable>
        </variable>
  </variables>
  <!-- Define function arguments or return values that can act as source or sink -->
  <functions>
      <!--Define each function argument or return value inside a 'function' element, assign id -->
        <function>
        </function>
  </functions>
  <!-- Define expected impact or no-impact using pairs of source-sink id-s-->
  <expect>
       <impact source="someSourceId" sink="someSinkId"/>
       <no-impact source="otherSourceId" sink="otherSinkId"/>
  </expect>
</impact-specifications>

In the XML file, inside a variable or function element, you can define a single variable or function, or a class of variables or functions. You define each variable (or class of variables) and each function (or class of functions) inside a match element, and assign one or more id-s to this element.. For instance:

To specify that a variable airVolumicMassDensity acts as a source, you define the variable element as follows:

<variable>
  <match>
    <match-declaration>
      <match-qualified-name value="airVolumicMassDensity"/>
    </match-declaration>
  </match>
  <impact-source id="air density calibration" event="onRead"/>
</variable>

For more details, see Variable Specification.

To specify that arguments of the function writeToDisplay act as sinks, you define the function element as follows:

<function>
  <match>
    <match-declaration>
       <match-qualified-name value="writeToDisplay"/>
    </match-declaration>
  </match>
  <impact-sink id="display x pos" event="onCallEntry" memory="(Argument (Function) 0)"/>
  <impact-sink id="display y pos" event="onCallEntry" memory="(Argument (Function) 1)"/>
  <impact-sink id="display value" event="onCallEntry" memory="(Argument (Function) 2)"/>
</function>

For more details, see Function Argument Specification.

You later use these id-s to define source-sink pairs in one of these elements in the XML file:

impact elements, to trigger checks for Expected impact.
no-impact elements, to trigger checks for Expected absence of impact.

For example, if you expect that the variable airVolumicMassDensity has no impact on the first argument of the writeToDisplay function when the function is called, specify a no-impact element as follows:

<no-impact source="air density calibration" sink="display x pos" />

Variable Specification

You can specify a variable or a class of variables as an impact-source or impact-sink. You specify each variable (or class of variables) inside a variable element in the impact specification XML file.

To specify the variable meterReading as an impact source, specify the following in the XML file:

<variable>
  <match>
    <match-declaration>
      <match-qualified-name value="airVolumicMassDensity"/>
    </match-declaration>
  </match>
  <impact-source id="A specific meter reading" event="onRead"/>
</variable>

To specify all variables starting with meterReading_ as impact sources, specify the following in the XML file:

<variable>
  <match>
    <match-declaration>
      <match-qualified-name wildcard="meterReading_*"/>
    </match-declaration>
  </match>
  <impact-source id="Any meter reading" event="onRead"/>
</variable>

To specify all variables starting with meterReading_ and ending with WithinRange as impact sources, specify the following in the XML file:

<variable>
  <match>
    <match-declaration>
      <match-qualified-name regex="meterReading_.*WithinRange"/>
    </match-declaration>
  </match>
  <impact-source id="A class of meter readings" event="onRead"/>
</variable>

The regex attribute supports all regular expressions.

An impact-source or impact-sink specification supports attributes such as event and memory. These attributes allow you to fine-tune certain aspects of the source and sink. For more information on these attributes, see Event and Memory Zone Specifications for Impact Analysis in Polyspace Code Prover.

Function Argument Specification

You can specify the argument or return value of a function or a class of functions as an impact source or sink. You specify each function (or class of functions) inside a function element in the impact specification XML file.

To specify the first and second arguments of the function writeToDisplay as impact sinks, specify the following in the XML file:

<function>
  <match>
    <match-declaration>
       <match-qualified-name value="writeToDisplay"/>
    </match-declaration>
  </match>
  <impact-sink id="display x pos" event="onCallEntry" memory="(Argument (Function) 0)"/>
  <impact-sink id="display y pos" event="onCallEntry" memory="(Argument (Function) 1)"/>
</function>

To specify the first and second arguments of all functions starting with writeToDisplay_ as impact sinks, specify the following in the XML file:

<function>
  <match>
    <match-declaration>
       <match-qualified-name wildcard="writeToDisplay_*"/>
    </match-declaration>
  </match>
  <impact-sink id="display all x pos" event="onCallEntry" memory="(Argument (Function) 0)"/>
  <impact-sink id="display all y pos" event="onCallEntry" memory="(Argument (Function) 1)"/>
</function>

To specify the first and second arguments of all functions starting with writeToDisplay_ and ending with WithinRange as impact sinks, specify the following in the XML file:

<function>
  <match>
    <match-declaration>
       <match-qualified-name regex="writeToDisplay_.*WithinRange"/>
    </match-declaration>
  </match>
  <impact-sink id="display some x pos" event="onCallEntry" memory="(Argument (Function) 0)"/>
  <impact-sink id="display some y pos" event="onCallEntry" memory="(Argument (Function) 1)"/>
</function>

The regex attribute supports all regular expressions.

An impact-source or impact-sink specification supports attributes such as event and memory. These attributes allow you to fine-tune certain aspects of the source and sink.

For instance, the previous examples describe how to specify a function argument as an impact sink. In all these cases, you are verifying at the function call site whether a specific function argument is impacted by the impact sources. Instead, you might want to focus on the function definition. For instance, you might want to specify a function parameter as an impact source, and verify whether certain objects within the function definition are impacted by this source. To provide this specification, you have to change the event attribute of the impact-source or impact-sink element (compared to the previous examples). In other words, you have to specify a different point of the function that begins the impact flow. For example, to specify that the first parameter of the function writeToDisplay must act as a source, use the following specification:

<function>
  <match>
    <match-declaration>
       <match-qualified-name value="writeToDisplay"/>
    </match-declaration>
  </match>
  <impact-source id="x Position Display" event="onStart" memory="(Argument (Function) 0)"/>
</function>

Note that the event specification has changed from onCallEntry to onStart to refer to the start of the function definition.

For more information on these attributes, see Event and Memory Zone Specifications for Impact Analysis in Polyspace Code Prover.

Class Member Specification

You can specify C++ objects as impact sources and sinks, just like any other variable. For instance, to specify that an object objMeterReadings of class MeterReadings acts as an impact source, use the following specification:

<variable>
  <match>
    <match-declaration>
      <match-qualified-name value="objMeterReadings"/>
    </match-declaration>
  </match>
  <impact-source id="A set of meter readings" event="onRead"/>
</variable>

You can also specify class members as impact sources and sinks using a memory attribute of the impact-source or impact-sink element. For instance, in the previous example, suppose that the object objMeterReadings is instantiated from a class MeterReadings that has a data member m_data and a member function write(). If you want to specify:

The member m_data as an impact source, use the following specification:

<variable>
  <match>
    <match-declaration>
      <match-qualified-name value="objMeterReadings"/>
    </match-declaration>
  </match>
  <impact-source id="A specific meter reading" event="onRead" memory="(Field (Variable) m_data)/>
</variable>

The member m_data as an impact source only after the member function write() is invoked, use the following specification:

<function>                
    <match>
        <match-declaration>
            <match-qualified-name value="MeterReadings::write"/>
        </match-declaration>
    </match>
    <impact-source id="readThis" 
                   event="onCallReturn" 
                   memory="(Field (Indirect (This (Function))) m_data)"/>
</function>

For more information on the memory attribute, see Event and Memory Zone Specifications for Impact Analysis in Polyspace Code Prover.