Install DySy

  1. Download Pex. DySy uses Pex, a powerful symbolic execution and simplification engine.
    1. Installing Pex is easy, it comes with a very convenient click-through installer.
    2. You do not need Visual Studio or any other for-pay software, except a recent 32-bit version of Windows (Vista or XP).
    3. DySy does not require any of the Pex extensions (such as Visual Studio integration). So any Pex installation option (including "Typical") should work for DySy.
  2. Download DySy. Extract the DySy.dll file from the downloaded zip file and place the DySy.dll file in a directory of your choice, such as f:\dot-net\DySy-prebuilt
Advanced option: The basic option above just uses the default pre-packaged distribution straight out of the box. Alternatively, you may want more control and the DySy source code, to build DySy yourself.

Use DySy

  1. Add the [DySyAnalysis] attribute to the class you want to analyze with DySy.
    1. Make sure your project has a reference to the DySy.dll assembly.
    2. This is in addition to the [PexClass|http://research.microsoft.com/Pex/wiki/PexClassAttribute.html] and [PexMethod|http://research.microsoft.com/Pex/wiki/PexMethodAttribute.html] attributes you would normally use for Pex.
  2. DySy is currently limited to analyze only single test executions. I.e., only a single method should have a [PexMethod] attribute and that method should not take any parameters. In the examples below, this single point of entry method is Entry().
  3. Build your project and explore it with Pex. Enjoy ;-)

Example

  1. The DySy.Examples project contains a minimal usage scenario. I.e., see our Program class.
  2. Build DySy.Examples.
  3. Run pex from the command line, e.g.: pex DySy.Examples.dll
  4. Pex should generate html files and open them in a browser window.
  5. Click on log, inferred spec of Program.Foo(Int32). You should see something like the following.
=== Purity
pure; // on all observed paths
=== Precondition
return 0 < a;

=== Result 
if (0 < a)
  return 6 + 2 * a;

More examples

  1. The DySy.Examples project contains more simple examples for using DySy. I.e., ICSE08 contains some examples from the ICSE 2008 DySy paper.
  2. The DySy.StackAr project contains our C# version of Daikon's StackAr subject program, which we used for our evaluation in the ICSE 2008 DySy paper.

Options

The [DySyAnalysis] attribute supports the following options.
  1. bool Arrays, false by default, enables or disables the reporting of updates to array elements. For example, DySy.StackAr has it enabled via [DySyAnalysis(Arrays=true)].
  2. int MaxStackDepth, 32 by default, sets the maximum method call stack height explored by DySy.

Limitations and known bugs

  1. DySy inherits any limitation Pex may have. In particular, DySy is very resource-hungry.
  2. DySy currently only works with the command line version of Pex.
  3. Loop abstraction seems currently broken.
  4. If you encounter a mysterious !error! [reflection] System.NullReferenceException, try to apply the following before running Pex/DySy: set pex_dont_gc_terms=1

Last edited Dec 4, 2008 at 3:46 PM by csallner, version 39

Comments

No comments yet.