The WhyR API

WhyR exposes a C++ API for tool authors to use for their own purpose. Here is a brief overview of how WhyR works. For details, check out the documentation in the header files themselves.

How WhyR Works

WhyR loads LLVM modules from files using the function AnnotatedModule::moduleFromBitcode. This function returns an AnnotatedModule, which is WhyR's wrapper around an LLVM module (Use the method rawIR to get the underlying data).

Once a module is loaded, call the method annotate to parse annotations attached to the module. This method will throw whyr_exceptions if something goes wrong.

AnnotatedModules contain AnnotatedFunctions, which contain AnnotatedInstructions. All of these wrap their corresponding LLVM concepts. AnnotatedFunctions contain requires and ensures clauses. AnnotatedInstructions contain assert and assume clauses.

Clauses are stored as the class LogicExpression. LogicExpressions represent a portion of an annotation. All LogicExpressions have a LogicType, which includes ints, reals, and LLVM types. LogicExpressions are parsed from the LLVM metadata nodes using the function ExpressionParser::parseMetadata.

LogicExpressions have a method checkTypes. This invokes type checking, which throws whyr_exceptions on violations of the type system. Methods to assist in type checking include LogicType's commonType and equals.

All LogicExpressions and LogicTypes have a getSource method, which returns a NodeSource. This contains debug information, source information, and the logic-local variable state.

WAR

WAR is parsed by a flex/bison generated parser. To turn an arbitrary WAR string into a LogicExpression, call the function parseWarString.

Why3 Generation

The function generateWhy3 writes the modelling of a module to an output stream.

Before WhyR can generate output, it has to figure out what theories it needs to add. It uses TypeInfo's method getTypeInfo. The information concerning all types used is stored in the TypeInfo object.

Once it gathers type info, it begins adding theories. The add* family of functions all add a certain theory (or part of a theory).

The function getWhy3SafeName mangles LLVM names, such that they will be valid Why3 names. Other get* functions returns the Why3 name of a certain concept.

LogicExpressions are converted into Why3 via the toWhy3 method. It receives a Why3Data object, which holds all the relevant information the LogicExpression needs to convert to Why3. LogicType also has this method; it returns a Why3 type name. This method also receives a TypeInfo, which it will add to if it requires a certain type to be present in the theory.

Why3 Execution

WhyR includes a utility function, execWhy3, that executes Why3 on a generated Why3 file. It returns a string that can be passed into the constructor of Why3Output. From there, the output of the Why3 execution is parsed.

error will be true if there was a syntax error (and message will contain the message, in that case). goals is a list of all the goals, which are Why3Goals. Why3Goals have a theory, goal, and status.

RTE Assertion Generation

addRTE adds runtime error assertions to an existing module. It finds instructions like add, sdiv, or shl, and adds assertions to them in order to prevent the execution of undefined behavior. Call addRTE to add RTE assertions.

Extending WhyR

You can add new kinds of annotation to WhyR. Just extend LogicExpression and/or LogicType!

To allow users to use your new expression, you will have to add an entry to the metadata parser table. ExpressionParser::getExpressionParsers returns the map of expression names to parser functions. Extend ExpressionParser and add it to this map.