<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffff" text="#000000">
On 08/27/2013 03:31 PM, Mikhail Mandrykin wrote:
<blockquote cite="mid:13274836.kEaEmKnbkt@molnar" type="cite">
<blockquote type="cite">
<pre wrap="">Did you have
cfa.simplifyPointerExpressions = true
here (as in config/predicateAnaylsis-bitprecise.properties)?
</pre>
</blockquote>
<pre wrap="">
</pre>
<blockquote type="cite">
<pre wrap="">That would be explainable if the option
cfa.simplifyPointerExpressions was not set to true.
</pre>
</blockquote>
<pre wrap="">
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@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@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.
</pre>
<blockquote type="cite">
<pre wrap="">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)?
</pre>
</blockquote>
<pre wrap="">
I think transformPointerArithmetic, transformArrows, transformStarAmper,
ignoreConst and ignoreVolatile can be easily moved to the analysis itself.
</pre>
<blockquote type="cite">
<pre wrap="">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).
</pre>
</blockquote>
<pre wrap="">
The current CFA transformations change the type in all references as well, so
I'll then look at doing the same in the ASTConverter.
</pre>
</blockquote>
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. <br>
<blockquote cite="mid:13274836.kEaEmKnbkt@molnar" type="cite">
<pre wrap=""></pre>
<blockquote type="cite">
<pre wrap="">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.
</pre>
</blockquote>
<pre wrap="">
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).
</pre>
</blockquote>
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. <br>
<blockquote cite="mid:13274836.kEaEmKnbkt@molnar" type="cite">
<pre wrap="">Regards, Mikhail
</pre>
<pre wrap="">
<fieldset class="mimeAttachmentHeader"></fieldset>
_______________________________________________
ldv-project mailing list
<a class="moz-txt-link-abbreviated" href="mailto:ldv-project@linuxtesting.org">ldv-project@linuxtesting.org</a>
<a class="moz-txt-link-freetext" href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a>
</pre>
</blockquote>
<br>
<br>
<pre class="moz-signature" cols="72">--
Best regards, Evgeny Novikov.
Linux Verification Center, ISPRAS
web: <a class="moz-txt-link-freetext" href="http://linuxtesting.org">http://linuxtesting.org</a>
e-mail: <a class="moz-txt-link-abbreviated" href="mailto:novikov@ispras.ru">novikov@ispras.ru</a></pre>
</body>
</html>