Extending the Static Checker

From Event-B
Revision as of 15:08, 25 August 2010 by imported>Pascal (→‎Parent)
Jump to navigationJump to search

Introduction

The purpose of this page is to describe how to extend the static checker. It covers on the one hand, the definition of the extension, and on the other hand its implementation.

The useful extension points are listed below; they offer the possibility to contribute to the static checker:

  • org.rodinp.core.autoTools
  • org.eventb.core.configurations
  • org.rodinp.core.internalElementTypes
  • org.eventb.core.scModuleTypes
  • org.eventb.core.scStateTypes

Before Starting

It is necessary to define the static checked elements that are similar to the unchecked elements. We will use as an example the decompositionFile that is defined as follows:

  • decompositionFile
    • decompositionRoot
      • Component (machine to be decomposed)
      • Configuration (style: shared events/shared variables;newProjectOption: decompose in the same project/different projects;decomposeContextOption:no decomposition/minimal decomposition)
      • SubComponent (resulting decomposed parts)
        • SubComponentElement (elements used to decompose: variables for shared event decomposition and events for shared variable decomposition)

To extend the static checker, it is necessary to add a new content type (org.eclipse.core.contenttype.contentTypes) containing the checked version of the decompositionFile: 

     <content-type
          base-type="org.rodinp.core.rodin"
          file-extensions="dcc,dcc_tmp"
          id="scDcpFile"
          name="Event-B Statically Checked Decomposition File"
          priority="normal">
    </content-type>

and the respective file association (org.rodinp.core.fileAssociations): 

    <fileAssociation 
         content-type-id="ch.ethz.eventb.decomposition.core.scDcpFile" 
         root-element-type="ch.ethz.eventb.decomposition.core.scDcpFile">
   </fileAssociation>

The respective static checked elements must be added as internal elements using the extension org.rodinp.core.internalElementTypes: 

<extension
       point="org.rodinp.core.internalElementTypes">
    <internalElementType
          class="ch.ethz.eventb.decomposition.core.basis.DecompositionRoot"
          id="dcpFile"
          name="%eventBdcpFile">
    </internalElementType>
    <internalElementType
          class="ch.ethz.eventb.decomposition.core.basis.SCDecompositionRoot"
          id="scDcpFile"
          name="Event-B Statically Checked Decomposition Root">
    </internalElementType>
    <internalElementType
          class="ch.ethz.eventb.decomposition.core.basis.DecompositionConfiguration"
          id="configuration"
          name="%eventBDecompositionConfiguration">
    </internalElementType>
    <internalElementType
          class="ch.ethz.eventb.decomposition.core.basis.SCDecompositionConfiguration"
          id="scConfiguration"
          name="Event-B Statically Checked Decomposition Configuration">
    </internalElementType>
</extension>

In the above example, the first internal element type is the unckecked internal element, and the second is the same internal element but in the checked version. Having the checked elements defined, we can start to extend the static checker for our files and respective elements.

AutoTools

The static checker it is a tool that runs automatically. In order to implement the tool, it is necessary to define the following extension point org.rodinp.core.autoTools. This extension point allows tools to run automatically when changes to the Rodin database are committed. To implement the reactive model of Rodin, automatic tools run only when one of their input files has changed. As such, for each automatic tool, plugin developers must provide two kinds of contributions:

  • Some dependency extractors.
  • The tool itself.

Declaration

The autoTools extension-point allows tool writers to register their tool implementation under a symbolic name that is then used by the Rodin platform to find and run the tool. The symbolic name is the id of the tool extension. An example of the implementation of a static checker can be seen as follows: 

<extension
       point="org.rodinp.core.autoTools">
    <tool
          class="ch.ethz.eventb.decomposition.internal.core.sc.DecompositionStaticChecker"
          id="decompositionSC"
          name="Decomposition Static Checker">
       <extractor
             class="ch.ethz.eventb.decomposition.internal.core.sc.DecompositionStaticChecker"
             name="Decomposition Extractor of Static Checker">
          <inputType
                id="ch.ethz.eventb.decomposition.core.dcpFile">
          </inputType>
       </extractor>
    </tool>
 </extension>

We defined a static checking tool that will run for the defined input type (ch.ethz.eventb.decomposition.core.dcpFile). The class provided for extractors shall implement the org.rodinp.core.builder.IExtractor interface, while the class provided for tools themselves shall implement org.rodinp.core.builder.IAutomaticTool.

The Rodin platform (see plug-in org.eventb.core) provides a static checking automatic tool for context/machine files.

Programmatic usage

The class to be implemented usually extends the class org.eventb.core.sc.StaticChecker and needs to implement the abstract method extract from the interface org.rodinp.core.builder.IExtractor: 

    public void extract(IFile file, IGraph graph, IProgressMonitor monitor)throws CoreException {
        try {
              monitor.beginTask(Messages.bind(Messages.build_extracting, file.getName()), 1);
              IRodinFile source = RodinCore.valueOf(file);
              IDecompositionRoot root = (IDecompositionRoot) source.getRoot();
              IRodinFile target = root.getSCDecompositionRoot().getRodinFile();
              graph.addTarget(target.getResource());
              graph.addToolDependency(source.getResource(), target.getResource(),true);
           } finally {
              monitor.done();
           }
    }

The interface org.rodinp.core.builder.IGraph is used by the extractors registered with the builder to manipulate the dependency graph of all Rodin resources of a Rodin project. It is a façade to the more complicated ways of manipulating the dependency graph inside the builder. Some information is cached in the corresponding object, so the contents of the façade must be synchronised with the graph at the end of an extraction. Requests to add nodes to the graph must be made explicitly by calls to the method addNode. Dependencies are managed by the façade. It saves clients to have to compute dependency graph deltas themselves.

We have already defined the static checking tool and the target for which it will run. Now, we need to configure the static checker tool. It is necessary to define the checks that are required for each element and this is done by providing an extension to org.eventb.core.configurations.

Configuration

The configuration is used to define which modules are used by the static checker. Similarly, it can be used for the proof obligation generator (POG).

Declaration

<!ELEMENT configuration ((config | pogModule | scModule))+>
 <!ATTLIST configuration
 id   CDATA #REQUIRED
 name CDATA #REQUIRED
 >
 id - the identifier for this attribute type (simple id token, unique for attribute types within the extension namespace). The token cannot contain dot (.) or whitespace.
 name - the human-readable name of this attribute type

For static checks, we need scModule and config elements. Below we see on an example how to define the configuration: 

<extension
        point="org.eventb.core.configurations">
     <configuration
           id="dcmp"
           name="Decomposition Configuration">
        <config
              id="ch.ethz.eventb.decomposition.core.dcmpBaseSC">
        </config>
     </configuration>
     <configuration
           id="dcmpSC"
           name="Decomposition Static Checker Root Module">
        <scModule
              id="ch.ethz.eventb.decomposition.core.decompositionModule">
        </scModule>
     </configuration>
     <configuration
           id="dcmpBaseSC"
           name="Decomposition Static Checker Base Module">
        <config
              id="ch.ethz.eventb.decomposition.core.dcmpSC">
        </config>
        <scModule
              id="ch.ethz.eventb.decomposition.core.componentModule">
        </scModule>
        <scModule
           id="ch.ethz.eventb.decomposition.core.decompositionConfigurationModule">
        </scModule>
        <scModule
              id="ch.ethz.eventb.decomposition.core.subComponentModule">
        </scModule>
        <scModule
              id="ch.ethz.eventb.decomposition.core.subComponentElementModule">
        </scModule>
     </configuration>
  </extension>

We structure the configuration as follows (although it can be structured in a different way):

  • "Decomposition Configuration" (id=dcmp) is defined by a base static checker module that contains the configuration element "Decomposition Static Checker Base Module" (see "config" markup, id=ch.ethz.eventb.decomposition.core.dcmpBaseSC). This configuration element is a reference to the respective configuration.
  • "Decomposition Static Checker Root Module" (id=dcmpSC) defines the initial module for decomposition (initialisation of the static checker) as the Root Module.
  • "Decomposition Static Checker Base Module" (id =dcmpBaseSC) defines all other modules, for each element in the decompositionFile:
    • ch.ethz.eventb.decomposition.core.componentModule
    • ch.ethz.eventb.decomposition.core.decompositionConfigurationModule
    • ch.ethz.eventb.decomposition.core.subComponentModule
    • ch.ethz.eventb.decomposition.core.subComponentElementModule

Here we are just defining the configuration of the modules. These modules shall be defined separately using the extension point org.eventb.core.scModuleTypes. These are used to process the necessary operations for each element inside a statically checked file.

Programmatic usage

It is possible to get the current configuration by invoking the org.eventb.core.IConfigurationElement.getConfiguration dedicated method.

In the same manner, the configuration is programmatically set with the setConfiguration method. It is possible to set multiple configurations with the ";" separator. Note that it is generally preferable to add a new configuration to the existing ones (see example 1), instead of replacing the existing ones with a new one (see example 2). Only the first evolution is indeed backward compatible. The second case requires to have installed the plug-in defining the new configuration in order to be able to manage the elements associated with this configuration; these elements cannot be (partially) handled by the old configuration.

  • Example 1 (better)
String conf = root.getConfiguration();
root.setConfiguration(conf + ";" + NEW_CONF);
where root is a IConfigurationElement object.
and NEW_CONF is the name of the new configuration.
  • Example 2
root.setConfiguration(NEW_CONF);

Modules

Filter

Filters are used to validate inserted elements. After the successful validation of all elements, they can be processed and stored in the statically-checked file. In order to implement a filter, we use the following extension from the extension point org.eventb.core.scModuleTypes: 

<!ELEMENT filterType (prereq)*>
 <!ATTLIST filterType
 id     CDATA #REQUIRED
 name   CDATA #REQUIRED
 parent CDATA #REQUIRED
 class  CDATA #REQUIRED
 >
 id - the identifier for this filter type (simple id token, unique for (filter/processor/root) types within the extension namespace). 
 The token cannot contain dot (.) or whitespace.
 name - the human-readable name of this filter module
 parent - the optional parent (processor) module. Root modules must leave the attribute undefined. It is not allowed to choose a filter module as parent.
 class - the fully-qualified name of a subclass of org.eventb.core.sc.SCFilterModule

For the filter type, the classes usually extend the abstract class org.eventb.core.sc.SCFilterModule. It also contains three methods:

  • public abstract boolean accept(IRodinElement element, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException;: it runs the static checker module. It returns whether the element should be accepted or not. If an error marker is associated with the element, the returned value should usually be false. Exceptions from this rule are possible, in particular if the element has been already marked with an error.
  • public abstract void initModule(ISCStateRepository repository,IProgressMonitor monitor) throws CoreException;: Initialisation code for the module.
  • public abstract void endModule(ISCStateRepository repository,IProgressMonitor monitor) throws CoreException;: Termination code for the module.

Processor

Processors literally process the elements, storing them in the static checked file, running sub-processors and adding states to the repository if required. To implement a processor, it is required to use the following extension from the extension point org.eventb.core.scModuleTypes: 

 <!ELEMENT processorType (prereq)*>
 <!ATTLIST processorType
 id     CDATA #REQUIRED
 name   CDATA #REQUIRED
 parent CDATA #REQUIRED
 class  CDATA #REQUIRED
 >
 id - the identifier for this processor type (simple id token, unique for (filter/processor/root) types within the extension namespace). 
 The token cannot contain dot (.) or whitespace.
 name - the human-readable name of this processor module
 parent - the optional parent (processor) module. Root modules must leave the attribute undefined. It is not allowed to choose a filter module as parent.
 class - the fully-qualified name of a subclass of org.eventb.core.sc.SCProcessorModule

The classes that implement the root type and processor type usually extend the abstract class org.eventb.core.sc.SCProcessorModule. They contain a constant called MODULE_TYPE that identifies the scModule element. An example is: 

public static final IModuleType<DecompositionModule> MODULE_TYPE = SCCore.getModuleType(DecompositionCorePlugin.PLUGIN_ID + ".decompositionModule");

that identifies the decomposition root module. Moreover, this classes should implement the three methods that are defined in the interface org.eventb.internal.core.tool.types.ISCProcessorModule:

  • public abstract void initModule(IRodinElement element,ISCStateRepository repository,IProgressMonitor monitor) throws CoreException: Initialisation code for the module. Used to initialise the global variables of the class.
  • public abstract void process(IRodinElement element,IInternalElement target, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException: Runs the static checker module. It processes the element. The element itself has already been accepted. If this element has children, then the children modules should be called here (see for example ch.ethz.eventb.decomposition.core.sc.modules.DecompositionSubComponentModule).
  • public abstract void endModule(IRodinElement element,ISCStateRepository repository,IProgressMonitor monitor) throws CoreException: Termination code for the module. It is used to clean up memory (global variables) before finishing the module call.

Root

Similar to a processor, but applied to the root of the file. The extension that needs to be implemented is defined below: 

<!ELEMENT rootType EMPTY>
 <!ATTLIST rootType
 id    CDATA #REQUIRED
 name  CDATA #REQUIRED
 input CDATA #REQUIRED
 class CDATA #REQUIRED
 >
 id - the identifier for this root type (simple id token, unique for (filter/processor/root) types within the extension namespace). The token cannot contain dot (.) or whitespace.
 name - the human-readable name of this root module
 input - identifier of the input file element type for this root module.
 class - the fully-qualified name of a subclass of org.eventb.core.sc.SCProcessorModule

Sequencing

Parent

A module may be linked to a parent module. The parent module shall be a processor module.

Prerequisite

Some static checks rely on already done static checks so they work as pre-requirements. For instance, if a concrete event is refined, it is necessary to know the abstract machine defined in the refine machine section. So the refine machine is a static check pre-requirement for the refinement an event. To implement a pre-requirement, it is necessary to use the following extension point: 

<!ELEMENT prereq EMPTY>
 <!ATTLIST prereq
 id CDATA #REQUIRED
 >
 id - the full ids of all (filter and processor) modules that must be run before this module

A pre-required module may be a filter module or a processor module.

Example

An example of module declaration is given below: 

 <extension
          point="org.eventb.core.scModuleTypes">
       <rootType
             class="ch.ethz.eventb.decomposition.core.sc.modules.DecompositionModule"
             id="decompositionModule"
             input="ch.ethz.eventb.decomposition.core.dcpFile"
             name="Decomposition SC Root Module">
       </rootType>
       <processorType
             class="ch.ethz.eventb.decomposition.core.sc.modules.DecompositionComponentModule"
             id="decompositionComponentModule"
             name="Decomposition SC Component Module"
             parent="ch.ethz.eventb.decomposition.core.decompositionModule">
       </processorType>
       .
       .
       .
       <filterType
             class="ch.ethz.eventb.decomposition.core.sc.modules.DecompositionSubComponentElementFilterModule"
             id="decompositionSubComponentElementFilterModule"
             name="Decomposition SC SubComponentElement Filter Module"
             parent="ch.ethz.eventb.decomposition.core.decompositionCommitSubComponentElementModule">
          <prereq
                id="ch.ethz.eventb.decomposition.core.decompositionConfigurationModule">
          </prereq>
          <prereq
                id="ch.ethz.eventb.decomposition.core.decompositionComponentModule">
          </prereq>
       </filterType>
    </extension>

Below is an example of the call of the three processor/root methods in the class ch.ethz.eventb.decomposition.core.sc.modules.DecompositionModule: 

       @Override
       public void initModule(IRodinElement element,ISCStateRepository repository,  IProgressMonitor monitor) throws CoreException {
               accuracyInfo = new DecompositionAccuracyInfo();
               final IDecompositionLabelSymbolTable labelSymbolTable = new DecompositionLabelSymbolTable(LABEL_SYMTAB_SIZE);
               repository.setState(labelSymbolTable);
               repository.setState(accuracyInfo);
               initProcessorModules(element, repository, monitor);
       }

       public void process(IRodinElement element, IInternalElement target,ISCStateRepository repository, IProgressMonitor monitor)throws CoreException {
               scRoot = (ISCDecompositionRoot) target;
              processModules(element, target, repository, monitor);
       }

       @Override
       public void endModule(IRodinElement element,ISCStateRepository repository, IProgressMonitor monitor) throws CoreException {
               scRoot.setAccuracy(accuracyInfo.isAccurate(), monitor);
              endProcessorModules(element, repository, monitor);
       }

Whenever a problem is encountered by the static checker, it is possible to raise a warning or an error, highlighting the associated element, using the method org.eventb.core.sc.SCModule#createProblemMarker. An example can be seen below: 

       public void process(IRodinElement element, IInternalElement target,ISCStateRepository repository, IProgressMonitor monitor)throws CoreException {
               monitor.subTask(Messages.bind(Messages.progress_DecompositionComponent));
               IComponent[] decompositionComponents = decompositionFile.getDecompositionComponents();
               if (decompositionComponents.length > 1) {
                       for (int k = 1; k < decompositionComponents.length; k++) {
                               createProblemMarker(decompositionComponents[k], DecompositionConfigurationAttributes.TARGET_ATTRIBUTE,
                                                             DecompositionGraphProblem.TooManyComponentsError);
                       }
              }
              ...
              repository.setState(new ComponentMachineInfo(scComponentMachineRoot,component));
              ...
             monitor.worked(1);
      }

In this particular case, if the number of IComponent elements is greater than 1, then an error is generated for the related IComponent element:

States

The static check of the elements in a file are independent of each other (different and independent modules). Nevertheless, some information depends on other elements. For instance, for label elements, it is necessary to know which labels have been previously used before checking the elements. Since the elements checks are independent, the solution is to ‘share data‘ through states implemented using the extension point org.eventb.core.scStateTypes. They are used to dynamically store data that will be used by dependencies. The data are stored in the SCStateRepository base, which contains a key and respective contents.

Declaration

<!ELEMENT stateType EMPTY>
 <!ATTLIST stateType
 id    CDATA #REQUIRED
 name  CDATA #REQUIRED
 class CDATA #REQUIRED
 >
 id - the identifier for this attribute type (simple id token, unique for attribute types within the extension namespace). The token cannot contain dot (.) or whitespace.
 name - the human-readable name of this attribute type
 class - the fully-qualified name of a subclass of org.eventb.core.sc.state.ISCState

Programmatic Usage

To store data, we need to call the method 

void setState(I state) [I extends IState]

defined in the interface org.eventb.core.tool.IStateRepository (See method initModule above).

To retrieve date, we call the method: 

I getState(IStateType<? extends I> stateType) throws CoreException

In order to use the stored state, it is necessary to define the ‘key‘ in the extension point stateType.

Example

An example of usage can be seen below: 

<extension
          point="org.eventb.core.scStateTypes">
       <stateType
             class="ch.ethz.eventb.decomposition.core.sc.state.IDecompositionAccuracyInfo"
             id="decompositionAccuracyInfo"
             name="Decomposition Accuracy Info">
       </stateType>
       <stateType
             class="ch.ethz.eventb.decomposition.core.sc.state.IDecompositionLabelSymbolTable"
             id="decompositionLabelSymbolTable"
             name="Decomposition Label-Symbol Table">
       </stateType>
       <stateType
             class="ch.ethz.eventb.decomposition.core.sc.state.IComponentAccuracyInfo"
             id="componentDecompositionInfo"
             name="Decomposition Component Machine Information">
       </stateType>
       <stateType
             class="ch.ethz.eventb.decomposition.core.sc.state.IDecompositionStyle"
             id="style"
             name="Decomposition Style">
       </stateType>
   </extension>

For instance, the last stateType element defined above is Decomposition Style. It is required to check which kind of subComponentElements are expected:

  • if style= shared event => subComponentElement expected type is variables.
  • if style= shared variable => subComponentElement expected type is events.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Extending_the_Static_Checker&oldid=5019’