[ldv-project] Benchmarking new predicate analysis with UFs

[Evgeny Novikov]

On 08/27/2013 03:31 PM, Mikhail Mandrykin wrote:
>> Did you have
>> cfa.simplifyPointerExpressions = true
>> here (as in config/predicateAnaylsis-bitprecise.properties)?
>> That would be explainable if the option
>> cfa.simplifyPointerExpressions was not set to true.
> No, so I've re-run the benchmark with this option. But it seems it won't
> influence the results greatly, because when I manually re-run the failed
> benchmarks with the option (used options attached in
> UsedConfiguration.properties), at least 9 out of 12 failures persisted. The
> exceptions are basically typing errors like these ones:
>
> 6x 			java.lang.IllegalArgumentException: A symbol with name `action at 4'
> already exists, with type:<BitVec, 64,>
> 2x			 java.lang.IllegalArgumentException: bv extraction of an empty range:
> [22671:22672]
> 1x			type error. term eeprom_wait_ready::status at 3 has type<BitVec, 64,>,
> but<BitVec, 48,>  was expected. (make_equal)
>
> Also there are 6 Out of Memory results (9GB of heap and 12 GB total limit is
> used) on the tests where three other configurations completed successfully.
>
>> However, the options that you present look much simpler to me, couldn't
>> these simplifications be implemented directly in the analysis itself
>> (where C asts are transformed to formulas)?
> I think transformPointerArithmetic, transformArrows, transformStarAmper,
> ignoreConst and ignoreVolatile can be easily moved to the analysis itself.
>
>> Options that do not have any disadvantages and just simplify the AST
>> could be implemented in the ASTConverter itself (without being
>> user-configurable). transformUnsizedArrays could be such an option
>> (although we would need to make sure that all references to that
>> variable also have pointer type instead of array type because analyses
>> expect that the type of variables does not change).
> The current CFA transformations change the type in all references as well, so
> I'll then look at doing the same in the ASTConverter.
>
I suggest to discuss all further questions about integration of the new 
Mikhail's analysis during his visit to Passau. This will be more 
efficiently. You will try different changes together and after all you 
will have a consensus.
>> For transformFunctionPointers, I wonder why you need this.
>> We actually added code to CPAchecker to make the reverse transformation
>> (adding * to a function pointer when it is called; adding&  to a
>> function when it is converted to a function pointer) to be able to
>> easily detect these cases in the AST and not confuse them with regular
>> function calls or variable accesses, and this helped to make the code of
>> the analysis easier and give less false answers.
> As I remember I had problems with typing here. In the CFA (especially in case
> of funciton pointer call handling with assume edges) there were comparisons of
> the form *f == *g where for instance f is a function and g  is a function
> pointer variable. Here my transformation only removes the star from *f. But
> maybe that's the only case when it's needed and that should be fixed somewhere
> else (in the CFA creation or in the analysis itself).
>
For me it looks like there shouldn't be a "*" before function "f" in 
this case after default transformations since "f" isn't a function 
pointer and, even more, "f" isn't called here. I assume there either "&" 
or nothing. But the latter will likely confuse some analysis if it will 
not see that function "f" isn't actually called there.
> Regards, Mikhail
>
>
> _______________________________________________
> ldv-project mailing list
> ldv-project at linuxtesting.org
> http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project


-- 
Best regards, Evgeny Novikov.
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: novikov at ispras.ru

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130828/78ad822d/attachment.html>