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
Note that it works like this: the parser creates pairs of functions which then
get applied.
Below we give a clear explanation how the parsing is done for a specific
deconstructor string, with the FormatCil module.
"void (*)(int)" is parsed like this (reduced to):
- "void" gets tokenized as terminal VOID, which gets reduced to type_spec
nonterminal
- "(*)(int)" gets reduced to direct_decl:
LPAREN attributes decl RPAREN LPAREN parameters RPAREN
where
attributes was reduced to empty (Note tha an attribute can be a
CONST, RESTRICT, VOLATILE)
decl was reduced to:
STAR attributes decl
where
attributes is reduced to empty
decl is reduced to empty (or highly unlikely to IDENT
which does in the semantic action also unrollType)
and the semantic action is:
{ ((fun ts args ->
let al = (fst $2) args in
(fst $3) (TPtr(ts, al)) args), (* Note that: TPtr of
typ * attributes *)
(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))
}
so it constructs TPtr.
and the semantic action is:
{ ((fun ts args -> (* Alex: who passes ts and args?? *)
let al = (fst $2) args in
let pars, isva = (fst $6) args in
(* Note that: TFun of typ * (string * typ *
attributes) list option * bool * attributes *)
(fst $3) (TFun(ts, pars, isva, al)) args),
(fun (fn, ft) ->
match (snd $3) (fn, ft) with
Some (TFun(rt, args, isva, al), m1) -> begin
match (snd $2) al, (snd $6) (args, isva) with
Some m2, Some m6
-> Some (unrollType rt, m1 @ m2 @ m6)
| _ -> None
end
| _ -> None))
}
Note that this direct_decl gets reduced to decl:
| direct_decl { $1 }
- the above reduction type_spec and direct_decl gets reduced to one_formal:
/*(* Do not allow attributes for the name *)*/
| type_spec attributes decl
{ ((fun args ->
let tal = (fst $2) args in
let ts = (fst $1) tal args in
let (fn, ft, _) = (fst $3) ts args in
(fn, ft, [])),
(fun (fn, ft, fa) ->
match (snd $3) (fn, ft) with
Some (restt, m3) -> begin
match (snd $1) restt,
(snd $2) (typeAttrs restt)with
Some m1, Some m2 ->
Some (m1 @ m2 @ m3)
| _, _ -> None
end
| _ -> None))
}
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and
their applications. This 200-page book is written by three acclaimed
leaders in the field. The early access version is available now.
Download your free book today! http://p.sf.net/sfu/neotech_d2d_may
_______________________________________________
CIL-users mailing list
CIL-users@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/cil-users
