View source for CITADEL

[[Category:Assertion checking]]

==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==
===Unfolded 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 unfolding depth were set to 2, then `c.unfolded' would be a 
  set of variables: {$c, c.x, c.y, $c.twin, c.twin.x, c.twin.y}.
  
  Containers need special kind of unfolding. 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.

====Functions in unfolded form====
 Ilinca: I'm not sure about the idea of including argument-less functions in 
  this unfolded form. What if the precondition of the function doesn't 
  hold or we run into some kind of trouble when executing the function 
  body (trouble such as the contracts of a sub-call made by this 
  function not holding or other bugs)? On the other hand, including 
  functions would bring significantly more information about the state 
  of the object... Does the Daikon frontend for Java, for instance, by 
  default evaluate functions too as part of the unfolded form of the 
  objects?

 Nadia: Well, this idea is disputable, of cause.
  In Java considering argument-less functions as variables is more 
  dangerous, because Java, like all C-family languages, encourages 
  side-effects in functions. However, in Daikon front-end for Java there 
  exists an option that allows using functions as variables. Together with 
  enabling this option user has to provide a special "purity" file that 
  lists those functions from the system, that are side-effect free. This 
  feature is described in Daikon User Manual, page 82.
  Considering functions as variables is even more relevant in Eiffel 
  context by two main reasons. Firstly, Eiffel encourages absence of 
  abstract side-effects in functions (and, I believe, most Eiffel 
  functions indeed do not have abstract side-effect, am I right?). For 
  those cases, when some functions in system are known to have 
  side-effect, we can allow user to specify an "impurity" file, that would 
  list those functions. I think that these cases would be rare.
  
    Ilinca: Indeed, I also think these cases would be rare, but, depending on the 
    size of the system, it might be very cumbersome for users to determine 
    these functions.

        Nadia: Well, a parameter may be introduced that will turn this facility on 
        and off. So, if a user knows that there are many impure functions in system, 
        he/she will just turn it off. I think, that its enough for the first version.
        In future some additional functionality may be introduced. In fact, a user may 
        not know about all impure functions in system (especially in code that was written 
        by someone else). The tool can help user to determine, did anything go wrong with 
        using functions in unfolding. For example, it may do instrumentation twice: first 
        time using only attributes and second time using functions also. As a result two 
        trace files are produces. Then the tool can compare attributes values in two files. 
        If they are the same, then with certain degree of confidence we can say, that called 
        functions had no abstract side effect.
        As I understand, precise analysis of abstract side-effect presence or absence in beyond 
        the state of the art. However, some methods which perform approximate analysis may be 
        introduced.
        Another interesting solution that came to mind is to store object's state each time before 
        calling a function and then recover object after the call. In this case we don't care about 
        function purity, we just get a result that this function might have had, if it was called at 
        this point :)
        Anyway, different partial solutions to this problem may be implemented and user may combine 
        different strategies to get a desired result with a desired degree of confidence.
        Conceptually, my point here is: why an "honest" Eiffel programmer, who never writes impure 
        functions, has to suffer (get less expressive contracts) because of other programmers, who 
        sometimes write impure functions?:)

            Ilinca: :) Indeed, the honest Eiffel programmer shouldn't suffer. So in conclusion, I 
            think we should go for the solution with the file containing the names of impure functions, 
            as Daikon does it. Adding the switch which turns it on and off is also a good idea. 

    Ilinca: Something else: what Daikon calls "purity" is actually 
    weak purity, isn't it? (Weak purity means that creations of local 
    variables are allowed in the body of a pure function. Strong purity 
    disallows this.)

        Nadia: Chicory (Java front end) doesn't check purity of functions that are listed in a purity 
        file. User is totally responsible for what he/she writes in this file. So, I would say that, what 
        Chicory calls purity isn't actually any special kind of purity. It only means that user allowed 
        Chicory to call this functions anywhere in the system, and if something goes wrong, it's user's 
        fault
  
  Nadia: Secondly, Eiffel advocates uniform access principle. Routine's clients 
  don't have to know, which queries, used in precondition, are attributes 
  and which are functions. If inferred preconditions contained only 
  attributes, it would be inconsistent with uniform access principle, I 
  think...

  Nadia: As for troubles that may arise when calling functions... As I 
  understand, exception in a function, called when its precondition holds, 
  is a bug. So, if it happens, we can just tell user that we found a bug 
  in certain function and that before inferring contracts the bug should 
  be fixed.

====Checking preconditions (static vs. dynamic)====  
  The issue with functions' preconditions that you've mentioned isn't a 
  big problem. If after unfolding we got a variable of the form, e.g., 
  `x.f1.f2', where `f1' and `f2' are functions, printing instructions for 
  this variable can be like this:
    if x.f1_precondition_holds and then x.f1.f2_precondition_holds
    then
       print (x.f1.f2)
    else
       print (Nonsensical)
    end
  "Nonsensical" is a special Daikon value that indicates that variable 
  cannot be evaluated.
  Function preconditions are known after parsing. To be able to evaluate 
  them separately, we may, for example, wrap them into functions. 
  `f1_precondition_holds' in the above code is an example of such a 
  function, that was introduced by instrumenter and added to x's 
  generating class.
  
    Ilinca: I don't think it's that easy, mainly because of polymorphism. Statically 
    you can't determine the type that x will be a direct instance of at 
    runtime. Hence, you don't know which preconditions to wrap. Of course, 
    since redefined routines can keep or weaken the preconditions of the 
    original routines, you can take the pessimistic approach of wrapping 
    only the precondition of the function from the static type of x, but 
    then you might miss cases in which the weakened version of the 
    precondition does hold. Do you understand my point?

        Nadia: Yeah, I see...
        I think that the main question here is: should we check "static" or "dynamic" 
        preconditions when calling a function?
        On the one hand, in Eiffel we can write something like:
        class A
           ...
           sqrt (x: REAL): REAL
               require
                   x >= 0.0
               do ... end
        end

        class B
           inherit A
              redefine sqrt end
           ...
           sqrt (x: REAL): REAL
               require else
                 True
               do ... end
        end

        class TEST
            ...
            an_a: A

            make is
               do
                    create {B} an_a
                    print (an_a.sqrt (-1.0))
               end
        end

        It works, and assertion checking mechanism doesn't indicate any error.
        But, on the other hand, is it legal? Am I allowed to call a function if it's 
        static precondition doesn't hold?
        As I understand, if I want to make sure that it's legal to call a routine at some 
        program point, I have to check it's static precondition. Even if today I'm sure that 
        dynamic type of `an_a' is always `B', this needn't remain the same tomorrow...

            Ilinca: That's correct. If the "static" precondition of a routine holds, this 
            implies of course that the preconditions of all its redefinitions will also hold. 
            But I was calling this approach "pessimistic" because the precondition of a redefined 
            version of a routine may hold even though the "static" precondition doesn't.

        So, if a programmer wanted to know function value at a program point, he/she would check 
        its static precondition. Then why instrumenter should act differently? Well, actually 
        there is a difference:  instrumenter not only avoids function call when precondition 
        doesn't hold, but also claims that function value is nonsensical. From one point of view, 
        such behavior is incorrect, because function actually could be called and a sensible value 
        could be received. From the other point, since it was illegal to call the function this time, 
        it makes sense to declare function value nonsensical.
        To sum up, I think that it is rather a philosophical then a technical problem, but, as for me, 
        checking static preconditions is more appropriate.
        However, if we wanted to check a dynamic precondition, it's also possible. We can wrap function's 
        precondition into a special function and redefine that special function any time the original 
        function is redefined. It is possible since instrumenter has access to the whole system.

            Ilinca: Well, this would definitely be the more... correct solution, but it's also a lot more 
            work. Couldn't this also be done by not wrapping the function, but simply calling it and adding 
            some exception handling code to the unfolder? I mean, the unfolder would try to call all 
            argument-less functions of a class on an object, and, if it gets a precondition violation, 
            it catches the exception and it declares that particular function as nonsensical?

 Nadia: I would like to return to the subject of checking "static" or "dynamic" preconditions 
 before function calls in unfolding. I think that this problem arises because the semantics 
 of special variable value "nonsensical" in Daikon is ambiguous.
 In Java and C there are no preconditions, so this value is originally used in Daikon for the 
 only purpose: if a pointer of reference is null, then the dereferenced value (and its attributes, 
 if the value is not of primitive type) is declared "nonsensical". In Eiffel we will use 
 "nonsensical" for this purpose too: if a reference entity is void, then its queries will be output 
 as "nonsensical".
 However, in Eiffel we have one more source of problems with evaluating variables: if a variable is 
 a result of a function call, then function precondition may not hold, so we won't be able to 
 evaluate its result. In this case the variable value should also be declared "nonsensical", because 
 this is the only special value in Daikon, which denotes that variable can't be evaluated. However, 
 in this case there appears a question: what does it mean that the variable can't be evaluated? Does 
 it mean that something terrible will happen (e.g., exception), if we try to evaluate it? Or does 
 it mean that it isn't legal to evaluate this variable in this program state?
 If we take the first point, then we should check dynamic precondition, because if static precondition 
 doesn't hold, but dynamic does, nothing terrible will happen during function call.
 If we take the second point, we should check static precondition, because if it doesn't hold then 
 it's illegal to call this function, even if dynamic precondition holds. This point seems more 
 correct to me, and here is an example that illustrates the situation.
 Consider class `INT_LIST' (with feature `item' that has a precondition `not off') and it's heir - 
 class EXTRAPOLATED_INT_LIST (that weakens precondition of `item'):

 class INT_LIST
 ...
 feature
    item: INTEGER is
       require
          not off
       ...
       end
 end

 class EXTRAPOLATED_INT_LIST
 inherit
    INT_LIST
    redefine
       item
    end
 ...
 feature
    item: INTEGER is
       require else True
       do
          if not off then
             Result := Precursor
          else
             Result := 0
          end
       end
 end

 Consider also class CLIENT, which is a client of INT_LIST:

 class CLIENT
 ...
 feature
    test (a_list: INT_LIST) is
       do ... end
 end

 Imagine that during system execution, when contracts were inferred, actual argument of `test' was 
 always a direct instance of EXTRAPOLATED_INT_LIST,  and in addition it was always passed to this 
 procedure in such a state that cursor was before the first element (`off' was true). If we check 
 dynamic preconditions for functions in unfolding, than a precondition, inferred for `test', will 
 be something like this:

 require
   a_list /= Void
   a_list.off
   a_list.item = 0

 But this contract isn't correct (as for me), although it is, certainly, true for a specific system 
 execution. It becomes a little more correct, if we infer:

 require
   a_list /= Void
   a_list.off
   a_list.generator = "EXTRAPOLATED_INT_LIST"
   a_list.item = 0

 However, such contracts (connected with dynamic type of variable) seem useless to me. One of the 
 goals of dynamic contract inference is to eliminate those properties that happened by chance and 
 are not intended properties of the code. Properties that are connected with dynamic types definitely 
 happen by chance: they can't be intended properties, because if programmer wanted his software to 
 have such a property, he would change static entity type to a more specific (based on descendant).
 Such properties may be useful only if we treat them not as contracts but rather as some kind of 
 runtime statistics. Programmer may be interested in information that is true for a specific system 
 execution, e.g. for debug purposes. It might be useful to add such a feature (inference of dynamic 
 type information and properties, connected with dynamic types) in future, but it isn't "classic" 
 contract inference, as for me, so I don't think that we need it in the first version. And if we 
 don't want to know anything about dynamic types, then we should check static preconditions of 
 functions during unfolding.

====Checking hand-written contracts====
    Ilinca: There's one further problem with this approach: when a function 
    is called as part of the evaluation of a contract, this function's 
    contracts are not checked. The reason for this is to avoid infinite 
    loops. If you wrap your precondition into a function, the contracts of 
    any routines it calls will be evaluated, and thus the system can 
    actually behave differently.
    Should we check at all the hand-written contracts of a system for which CITADEL  
    is trying to infer contracts? We could also start from the assumption that Daikon 
    uses: the tool is given a set of passing test cases and from those it has to infer 
    contracts. If the inferred contracts somehow contradict the hand-written ones, then 
    there's a problem in the system, and the source of the  problem may be that the 
    hand-written contracts are faulty. What do you think?
    
        Nadia: I think that it makes sense to turn assertion checking off when running 
        instrumented system. This will solve the problem with functions inside wrapped 
        preconditions, which you've mentioned.
        In current version instrumented system is supposed to behave exactly the same way 
        as the original system did (except for creating a trace file). So, if a user was 
        sure about the original, hand-written contracts and wanted to check the system against 
        them, he/she could run the original system with assertion checking on, make sure that 
        everything is ok and after that perform contract inference.
        On the other hand, returning to using functions in unfolding: for these calls we have to 
        check hand-written preconditions, because they were introduced by instrumenter, so they are 
        not parts of "passing test cases". Fortunately, as you said before, erroneous preconditions 
        are very rare.

====Checking preconditions (wrapping vs. qualification)====
 Nadia: I started implementing function preconditions checks in unfolding recently and realized 
 that my first idea (to wrap these preconditions into functions) has an important disadvantage. 
 Without creating new functions for preconditions if we instrument a class, then only the source 
 code of that very class changes. However, if during class instrumentation we add functions to 
 its clients, then the source code of those clients also changes. It isn't a disaster, of cause, 
 but it's an unpleasant property, as for me. It would be nice, if class instrumentation affected 
 only the class itself.
 The other solution is not to wrap preconditions into functions, but to "qualify" them: if we want 
 to check precondition before calling a function `x.f', we should take f's precondition and 
 replaced all unqualified calls in it by qualified calls with target `x' and all occurrences of 
 `Current' by `x'. This replacement is not difficult conceptually, but its implementation is quite 
 voluminous (during this operation we have to replace some identifiers in an expression with function 
 calls, so we need to redefine all `process_<something>' procedures of ET_AST_ITERATOR, where 
 <something> can appear in expression and can contain identifiers).
 What do you think about these two solutions ("wrapping into functions" and "qualification")?

    Ilinca: I think the best way to go is to wrap the precondition in a function in the class that 
    it belongs to. Wrapping it in a function in clients would break encapsulation: you would only 
    be allowed to access the exported features. I don't see any advantages of qualification over 
    function-wrapping, so I think it makes sense to choose the least-work solution

        Nadia: My previous explanation of the problem with "wrapping" was a little bit confused 
        (I wrote that functions have to be added to clients of instrumented class, but actually 
        I meant quite the opposite: that they should be added to suppliers:) )
        Wrapping a precondition in a function in the class that it belongs to is exactly what I 
        wanted to do firstly. The reason for it was that, if we instrument a class `C' and it has, 
        say, an attribute `x: LIST[INTEGER]', then unfolded form of `Current' variable will include 
        a variable `x.first'. Precondition of function `first' in class LIST is `not empty'. However, 
        we need to check this precondition not inside LIST, but inside routines of class `C'. In fact, 
        printing instruction for variable `x.first' should be guarded by condition like this:
        if x /= Void and then not x.empty then
           print (x.first)
        end
        We can't just take a precondition from `first' and insert it into the guarding condition as is, 
        instead we should "qualify" the call to `empty' with target `x'.
        Firstly qualification seemed too complex to me, so I decided to wrap `not empty' into function, say,
        `first_precondition: BOOLEAN' and add it to class `LIST', so that inside `C' I can check simpler 
        condition before printing x.first:
        if x /= Void and then x.first_precondition then
            print (x.first)
        end.
        However, as you can see, it involves modifying class `LIST' (and possibly any other supplier of 
        `C') while instrumenting `C'. If only `C' changed, then we could print only its source code after 
        instrumentation, we could compile only `C' (if incremental compilation is used) and don't recompile 
        base library, we would have no problems with tracking added functions (the problems are like this: 
        if we instrument class `LIST' after `C', we probably don't want neither to instrument added functions, 
        nor to see them in unfolded form of `Current' variable of class `LIST'). As for me, wrapping adds 
        surplus dependencies into the system, and software never benefits from dependencies :)
        That is why later I inclined to "qualification" solution. Actually, I have already mostly implemented 
        it:) Current implementation might be incomplete, there are several syntactic constructs that it doesn't 
        handle, because I'm not sure that they can appear in preconditions, but I'll check it and fix the problem.

            Ilinca: Ok, so what I was thinking about was that you wanted to wrap the whole precondition of 
            `first' into a function in class C. So, in class C you would have a routine
            precondition_first (l: LIST[G]): BOOLEAN
                 require
                      l_not_void: l /= Void
                 do
                      Result := not l.empty
                 end
            Then the guard for printing x.first would be
                 if x /= Void and then precondition_first (x) then
                      print (x.first)
                 end
            But of course whether or not you wrap the precondition in a function or just quote it in the if 
            statement does not make a big difference.

 One more question: should the tool allow instrumenting library classes? If a library was precompiled, 
 then instrumenting any of its classes will result in recompiling the whole library, am I right? Are 
 precompiled libraries anyway recompiled during system finalization or not? (It matters for choosing 
 between "wrapping into functions" and "qualification" solutions, because "wrapping into functions" can 
 change library classes, even if user wants to implement only classes from his own clusters).

===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.

===Inferring contracts for generic classes===
 Nadia: there are actually two different cases.
  1. Contracts inside generic classes. This is not really a problem. 
  Entities, which have parameter type, can be treated as if their 
  generator is constraining class (ANY, if genericity is unconstrained).
  
  2. Contracts in clients of generic classes. Here some problems arise. If 
  we have an entity `x: ARRAYED_LIST[INTEGER]', its unfolding involves 
  processing the `item' query. `item' is declared to be of type `G' in 
  ARRAYED_LIST and, as I understand, parsing is not enough (some type 
  analysis is needed) to infer that `G' means `INTEGER' in current 
  context. Two approaches to this problem, that I see at present, are: 
  perform such a type analysis in compile time (with the help of gobo 
  compilation facilities) or leave some unfolding work until runtime, 
  when reflections may be used to determine variable's generating class.