Difference between revisions of "CITADEL"

Revision as of 06:58, 14 December 2007

Overview

CITADEL (Contract-Inference Tool that Applies Daikon to the Eiffel Language) is a tool that provides an Eiffel front-end for the Daikon invariant detector. It is being implemented as a Master's project by Nadia Polikarpova supervised by Ilinca Ciupa (ETH).

Discussions

• Flattened variables

Nadia: Daikon can process values of only few types: five scalar types (boolean, 
 integer, double, string and hashcode) and five more types, which are 
 arrays of these scalars.
 So, if in Eiffel code we a have a variable of one of basic types 
 (BOOLEAN, NATURAL, INTEGER, REAL or STRING) we can print its value 
 directly as if it has one of Daikon's types.
 If, however, we have a variable of any other type, we have to collect 
 all the information about it that is of interest and is available at 
 certain program point, and present this information to Daikon as a set 
 of  variables, which have Daikon types. The information of interest 
 about a variable includes results of all queries that can be called on 
 this variable at this program point.  However, since queries results may 
 themselves be of non-basic types, we have to perform this operation 
 recursively (to a certain depth).
 For a reference variable information of interest includes also its 
 address (Daikon type "hashcode" is intended for representing object 
 addresses).
 For example, if we had a variable c: POINT, queries of class POINT 
 available at current program point were `x: REAL', `y: REAL' and `twin: 
 POINT' and flattening depth were set to 2, then `c.flattened' would be a 
 set of variables: {$c, c.x, c.y, $c.twin, c.twin.x, c.twin.y}.
 
 Containers need special kind of flattening. If we want Daikon to handle 
 them sensibly, they should be converted to arrays of scalars (to be more 
 precise, it should be done only if all container elements are observable 
 at current program point...). It isn't difficult for descendants of 
 CONTAINER class from standard library. Instrumenter may check, if a 
 variable is an indirect instance of CONTAINER, get its 
 `linear_representation', then traverse it and output as array. I think 
 that in the first version we may leave aside those containers, that 
 aren't inherited from CONTAINER.

• Support for loop invariants

Ilinca: Does the "classic" Daikon support loop invariants?

Nadia: Daikon uses standard program point 
 suffixes to infer more invariants. E.g., it understands that 
 some_routine:::ENTER and some_routine:::EXIT are entry and exit points 
 of the same routine. Thanks to this, it knows `old' values of variables 
 at exit and can infer invariants like "x = old x". As I understood, if 
 Daikon sees an unknown suffix, it treats corresponding program point as, 
 so to say, "standalone" and doesn't try to connect it with any other.
 We don't need any extra support from Daikon to handle loop invariants.

 If we want to infer loop invariants, we should introduce a separate 
 program point for each loop. So, we need a way to distinguish loops 
 within a routine. One way is to take its position in source code as 
 index. However, I thought, that position is too unstable to become loop 
 identifier, so I chose instruction number instead. These numbers are 
 unique numbers of instructions within surrounding routine, they may be 
 used not only for loops, but for arbitrary instructions. 
 CI_INSTRUCTION_COUNTER is responsible for counting instruction while 
 iterating through AST.