Re: [csmith-dev] Generating ACSL \assigns clauses with programs

[Xuejun Yang <xuyang@microsoft.com>]

Sorry Robert, I missed your questions. See my answers inline.

> -----Original Message-----
> From: csmith-dev-bounces@flux.utah.edu [mailto:csmith-dev-
> bounces@flux.utah.edu] On Behalf Of Robert Clausecker
> Sent: Friday, November 27, 2015 9:07 AM
> To: csmith-dev@flux.utah.edu
> Subject: Re: [csmith-dev] Generating ACSL \assigns clauses with programs
> 
> Hello Xueyun,
> 
> > Take a look of FactMgr::map_stm_effect. I think it has the info you
> needed.
> 
> I tried to use map_stm_effect to get the desired information, but it doesn't
> seem to contain the information I need either. For example, for a statement
> 
>     *param = expression;
> 
> where param is parameter to the current function, map_stm_effect contains
> the object pointed to by param (as far as I understand). It seems to not
> contain information of the form “pointee of param is modified.”
> 


XY: map_stm_effect is a hash table, with key being a statement, and value being an effect. An Effect object contains 3 lists: read_vars, write_vars, and lhs_write_vars. If you find objects pointed to by param in the write_vars and/or lhs_write_vars lists, which means the pointees are written in this statement, it means the effect analysis is correct.

> > Csmith performs path-sensitive inter-procedural analysis. It is realized with
> the following steps:
> >
> > 1) Caller (foo) to callee (bar) handover, where foo passes the
> > knowledge, e.g., y is pointing to x, to bar;
> > 2) Effect analysis in bar;
> > 3) Callee (bar) to caller (foo) handover, where bar tells foo that x is
> modified.
> >
> > For details, check FunctionInvocationUser::revisit.
> 
> I have tried to understand how this mechanism works and I feel like I haven't
> understood it well enough to be able to make my own modifications to the
> code.
> 
> For my application, I believe I need the exact opposite (i.e.
> intra-functional path-insensitive analysis) of what the csmith code does.
> While it seems like the information I need is available during the analysis, it
> seems to be erased (i.e. replaced by contextual
> information) by the time meta-data about the function is printed out.
> 
> How would you implement tracking context-insensitive data about functions
> (i.e. data that is oblivious about where the function is called)? Where would
> you add the corresponding code and what modules have to be modified in
> order to get the desired result?
> 

XY: first of all, current implementation of Csmith can "see through" a pointer while performing effect analysis. You have to block that capability when the pointer is a function parameter. So if *param is on LHS, the analysis should conclude "param's pointees are written" instead of "{pointee1, pointee2, ....} are written". Same thing if *param is read. The key function you should modify is FactPointTo::merge_pointees_of_pointers. For pointers of parameters, the return list should be the pointer itself.

Secondly, you should use Function::feffect for a context-insensitive summary of the effects achieved by all invocations of the function. Once you take care the first issue, the read_vars and write_vars in this variable should tell you which parameter pointers are read or written.

-Xuejun