[CIL users] Searching with CIL interpreted deconstructors

[Alex S. <ale...@gm...>]

On 3/21/2013 10:56 PM, Gabriel Kerneis wrote:
> Hi Alex,
>
> On Tue, Mar 12, 2013 at 12:04:26PM +0200, Alex Susu wrote:
>> As far as I understand, interpreted constructors allow more general patterns
>> than deconstructors - see end of Section 6.2 for example of big constructor
>> pattern. On the other hand, I was able only to specify types for
>> deconstructors. I was thinking it might be somewhat useful to match a
>> function by giving to a deconstructor the prototype of the function but
>> maybe also some statements within the function.
>
> The reason what you are trying to do doesn't work is because the name of
> formal parameters is part of the type of the function, whereas it's name is
> not.  I'm not sure whether this is part of the C standard or an artifact of
> how CIL handles types, but it explains the limitation you have hit.
> Formatparse is not the culprit here: the identifier is parsed correctly (in
> the "decl" rule indeed), but ignored by dType because it does not belong to
> the type at all
> (see the definition of TFun in cil.mli).

   Thanks for pointing me out to this. Indeed TFun in cil.ml(i) doesn't contain the name 
of the function either.

 >> Given the above examples, I would like to have a few extensions to the CIL
 >> deconstructors:
 >> - specify names of functions - currently adding real function names to
 >> deconstructors gives parse error
 >
 > Agreed, it would be sensible and consistent with matching parameter names.

   I spent a bit of time to understand what are the semantic actions normally handling the 
deconstructor strings like: "void (*)(int)". You can find a sort of explanation on how 
such string is parsed by formatparse.mly in the attached text file.

   So the problem is:
     CIL currently can deconstruct the following strings:
       "void (*)(int)"
     but can't deconstruct (gives parser error because we specify the function name):
       "void MyFunctionName(int)"

       (OR "void MyFunctionName(int s)")


   The solution seems to be:
    To be able to manage this:
     STAR attributes decl
         should be replaced to IDENT? attributes decl (or maybe argv?? attributes decl):
         IDENT attributes decl
                     { ((fun ts args ->
                          let al = (fst $2) args in
                          (fst $3) (TPtr(ts, al)) args),

                        (fun (fn, ft) ->
                          match (snd $3) (fn, ft) with
                            Some (TPtr(bt, al), m2) -> begin
                              match (snd $2) al with
                                Some m1 -> Some (bt, m1 @ m2)
                              | _ -> None
                            end
                          | _ -> None))
                     }

         I guess that we need to process IDENT similar to this:
             |  DOT IDENT offset       { ((fun t args ->
                                             let fi = getField t $2 in
                                             Field (fi, (fst $3) fi.ftype args)),

                                         (fun off -> match off with
                                            Field (fi, off') when fi.fname = $2 ->
                                              (snd $3) off'
                                         | _ -> None))
                                       }

    I am starting now to experience with the grammar in formatparse.mly - will let you 
know of the outcome.



> On the other hand, you are not restricted to types for deconstructors: you can
> match expressions (dExp), lvalues (dLval) and instructions (dInstr).  A dStmt
> seems to be missing, however.  You would need to change the "stmt" rule of
> formatparse.mly, making a pair of constructor/deconstructor functions and
> using fst/snd for cStmt/dStmt in formatcil.ml, just like it is done for
> "instr". No idea how hard it would be to implement.

   Would there be an interest to add an dStmt deconstructor, as well?


   Regards,
     Alex