Readme of ECC Fixer v0.1

Introduction

The ECC fixer is a research prototype showing how to use the new fix generation technique developed by Generative Software Development Lab, University of Waterloo to fix configuration errors in eCos/CDL configuration. Given an eCos configuration file (.ecc file), this tool automatically reports all errors in the configuration, and propose a list of fixes for each error. Alternatively, the user can specify an option name, and the tool will try to give a list of fixes for activating the option. This is a preliminary release mainly served as supplementary material for paper "Generating Range Fixes for Software Configuration".

Installation

Prerequisite

ECC fixer is developed in Scala using simple build tool. To successfully compile and run the code, you need the following tools.

Installation Steps

  1. Extract the zip file.
  2. Open "src\main\scala\Configuration.scala", and point "Z3_PATH" to the binary of Z3. Note there are four different binaries of Z3, designed respectively for x86/x64 and single-thread/multi-thread. All of them are supported, and we recommend to use the multi-thread version if you have a multi-core CPU. Please choose one that suits your computer.
  3. If you choose a multi-thread Z3 binary in the previous step, you may set the number of threads by changing "THREAD_NUMBER" in "src\main\scala\Configuration.scala".
  4. In the root of the extract files, type "tools\sbt" to start simple build tool
  5. Type "generate" to generate part of the source code.
  6. Type "compile" to compile the source code. There might be some warnings, but are safely
  7. Type "exit" to exit simple build tool.

Usage

There are two main uses of Ecc fixer. First, given an .ecc file saved by eCos Configuration Tool (configtool), Ecc fixer automatically reports all errors in the configuration, and propose a list of fixes for each error. Second, the user can specify an option name, and the tool will try to give a list of fixes for activating the option.

Check and fix configuration errors

Type "run [ecc_file_name]" to check and propose fixes for an ecc file.

The released package already contains a few (possibly faulty) ecc files under the directory "testfiles\realworld". For example, "Easy-3-redboot.ecc" contains one error. You may type "run testfiles\realworld\Easy-3-redboot.ecc" to get this error and three fixes for it.

[CYGBLD_REDBOOT_CMD_LINE_HISTORY_bool:=false]
[CYGNUM_REDBOOT_CMD_LINE_EDITING_data:(CYGNUM_REDBOOT_CMD_LINE_EDITING_data > 0)]
[CYGBLD_BUILD_REDBOOT_bool:=false]

When loading a new ecc file, the system will first try to deduce types for all options. It is possible that there are type conflicts or a unique type cannot be determined. In such cases, Ecc fixer uses annotations to overwrite faulty expressions or mark correct types for an option. To learn more about annotations, please refer to the introduction of annotation below.

Activate an option

Type "run -a [option_name] [ecc_file_name]" to generate fixes for activating an option. For example, typing "run -a CYGSEM_HAL_VIRTUAL_VECTOR_CLAIM_DEFAULT testfiles\realworld\Easy-3-redboot.ecc", we will get the following fix.

[CYGSEM_HAL_VIRTUAL_VECTOR_INIT_WHOLE_TABLE_bool:=false]

Measure fixing time

Use option "-t" to let Ecc fixer report the time used to generate the fixes. You may also use "-t [n]" to execute the generation n times and Ecc fixer will report the average time used for one generation.

Use annotation file to correct type errors

Ecc fixer assumes each option in a CDL model has one of the following types:

Ecc fixer will try to deduce one type for each option from the expressions referring to the options. If no unique type can be determined, either because an option can have multiple types or has no suitable type, an type error is reported. For example, if we remove the following lines in "realworld\allModels.annotation",

CYGNUM_HAL_ARM_LPC2XXX_CAN_CLK{
calculated [CYGNUM_HAL_ARM_LPC24XX_CLOCK_SPEED / toInt(CYGNUM_HAL_ARM_LPC24XX_CAN_CLK_DIV) ] replacing [CYGNUM_HAL_ARM_LPC24XX_CLOCK_SPEED / CYGNUM_HAL_ARM_LPC24XX_CAN_CLK_DIV]
}
we shall get the following type error:
ca.uwaterloo.gsd.rangeFix.TypeErrorsException: Type clash in CYGNUM_HAL_ARM_LPC2XXX_CAN_CLK:
T[CYGNUM_HAL_ARM_LPC24XX_CAN_CLK_DIV]=Number from Set(CYGNUM_HAL_ARM_LPC2XXX_CAN_CLK)
T[CYGNUM_HAL_ARM_LPC24XX_CAN_CLK_DIV]=Enum[1,2,4,0,6] from Set(CYGNUM_HAL_ARM_LPC24XX_CAN_CLK_DIV).

The error basically says that from "CYGNUM_HAL_ARM_LPC2XXX_CAN_CLK" we deduce that "CYGNUM_HAL_ARM_LPC24XX_CAN_CLK_DIV" should be of type number, and from "CYGNUM_HAL_ARM_LPC24XX_CAN_CLK_DIV" we deduce that "CYGNUM_HAL_ARM_LPC24XX_CAN_CLK_DIV" should be of type enumeration. However, their types clash in "CYGNUM_HAL_ARM_LPC2XXX_CAN_CLK".

To fix type errors, we use annotations specified in "realworld\allModels.annotation". To fix the above type error, we add the above code back into "realworld\allModels.annotation". The code basically says that in option "CYGNUM_HAL_ARM_LPC2XXX_CAN_CLK", if we find a calculated declaration matching "[CYGNUM_HAL_ARM_LPC24XX_CLOCK_SPEED / CYGNUM_HAL_ARM_LPC24XX_CAN_CLK_DIV]", we replace it with "[CYGNUM_HAL_ARM_LPC24XX_CLOCK_SPEED / toInt(CYGNUM_HAL_ARM_LPC24XX_CAN_CLK_DIV) ]". By adding the "toInt" function, we explicitly convert the type of the later expression to number.

This kind of annotation has the following general form:

header [expression1] replacing [expression2]

where "header" can be "default_value", "legal_values", "requires", "calculated", and "active_if". When we use "requires" or "active_if", we may also add a number as "requires(0)" or "active_if(1)" to specify the index of the declaration to be replaced. If the declared expression matches expression2, it will be replaced with expression1.

Besides this one, we also supports two other forms of annotation, as listed below.

Experiment

The files used in the experiments in the paper are stored under folder "experiment". To repeat the experiments, execute "runExperiment", files will be created recording the result of the experiments.

Licenses

Ecc fixer is published under MIT license. Please see "license.txt" file for more details. Some ecc files, libraries and tools are obtained from other projects, and they are released under their own licenses, specified by the "fileName-license.txt" or "directoryName-license.txt" in the respective directories.

Contributors

Contact

Please contact Yingfei Xiong for any question, suggestion, or if you would like to contribute to the code.