USI & SUPSI Source Code Management (SCM): Issueshttps://scm.ti-edu.ch/https://scm.ti-edu.ch/favicon.ico?15601711372019-10-06T22:15:21ZUSI & SUPSI Source Code Management (SCM)
Redmine hifrog - Bug #13577 (New): prop incorrect resulthttps://scm.ti-edu.ch/issues/135772019-10-06T22:15:21ZSepideh Asadisepideh.a65@gmail.com
<p>Benchmark: ex21-upg2.c (attached)</p>
<p>How to run:<br />./hifrog --logic prop ex21-upg2.</p>
<p>Error:<br />reported as Successful but I think a= 1 and b=1 is a CEX. Surprisingly CBMC also agrees as Successful!</p> hifrog - Bug #13356 (Resolved): Bug in Hifrog LRA encoding - resulting assertion violation for a ...https://scm.ti-edu.ch/issues/133562019-09-26T11:54:36ZSepideh Asadisepideh.a65@gmail.com
<p><strong>Benchmark</strong>: ex13-change-orig.c (attached)</p>
<p><strong>How to run:</strong><br />./hifrog --logic qflra ex13-change-orig.c</p>
<p><strong>Error:</strong><br />LRA reports the bench as unsafe, while prop reports it as safe. The result of dump-query is SAT in OpenSMT and Z3, so the bug is in the encoding.</p> cow - Feature #12972 (New): Implementazione header e footer del CERDDhttps://scm.ti-edu.ch/issues/129722019-08-21T15:17:23ZAndrea Massimini
<p>Per avere uno standard nei vari siti e una corporate identity si vuole implementare un header e un footer per tutti i siti che sia anche facilmente modificabile. <br />Questo è stato reso possibile tramite un implementazione in JS.</p>
<p>in allegato (codice.docx) ho evidenziato il codice necessario per il funzionamento.<br />Ho inserito già per il comando "createHeader" i colori per la vostra piattaforma.</p>
<p>Il risultato dovrebbe essere come allegato ("Pescu3-withCERDD.png" e "Pescu2-withCERDD_01.png" con il problema di conflitto di bootstrap e "Pescu3-withCERDD_02.png" senza)</p>
<p>questo crea un tempo di loading dato che deve scaricare i vari file come anche eseguire i comandi. Noi abbiamo internamente sviluppato dei semplici controlli per evitare una fase di caricamento che visualizza gli elementi che vengono disposti. Eventualmente si può discutere su come implementarlo ma richiede poche linee di codice quindi sarebbe interessante avere lo stesso sistema.</p> OpenSMT 2 - Bug #10647 (New): UF benchmark crashhttps://scm.ti-edu.ch/issues/106472019-04-11T09:18:00ZMartin Blichablicha@d3s.mff.cuni.czhifrog - To do #10434 (New): Automatically detect the bound in HiFrog for the sake of completenesshttps://scm.ti-edu.ch/issues/104342019-03-29T13:52:40ZSepideh Asadisepideh.a65@gmail.com
<p>Developing a preprocessing mechanism to detect the necessary depth of unrolling the program.(completeness threshold)<br />Then we can claim on verification of those instances, not just falsification.</p> hifrog - To do #9433 (New): strong itp-lra-algorithm generates redundant formulahttps://scm.ti-edu.ch/issues/94332018-11-28T21:43:13ZSepideh Asadisepideh.a65@gmail.com
<p>investigate LRA strong itp Alg and compare the result with weak one; it seems weak mode generates compact and good summary, the same as TACAS version, but STRONG mode contains some redundant parts in the formula.</p>
<p>------------------------------------------<br />example:<br />short get_nondet_short();</p>
<p>int abs(int x) {<br /> return x >= 0 ? x : -x;<br />}</p>
<p>int main() {<br /> int x = get_nondet_short();<br /> x = abs(x);<br /> int y = x + 2;<br /> assert(y >= 0);<br />}</p>
<p>------------------------------------------<br />How to run?</p>
<p>weak: <br />./hifrog --logic qflra --itp-lra-algorithm 2 example.c</p>
<p>strong:<br />./hifrog --logic qflra --itp-lra-algorithm 0 example.c</p> hifrog - To do #7864 (New): investigate the functionality of --no-assert-grouping https://scm.ti-edu.ch/issues/78642018-09-08T18:23:22ZSepideh Asadisepideh.a65@gmail.com
<p>2-Enable this functionality:<br />--no-assert-grouping : do not group checks for the same assertion with the different call stack.</p>
<p>This option when is enabled will increase the possibility of holding the assertion for a specific function.</p> hifrog - To do #7863 (New): report system in HiFroghttps://scm.ti-edu.ch/issues/78632018-09-08T18:19:17ZSepideh Asadisepideh.a65@gmail.com
<p>Design a separate class as a report class in HiFrog (storing in the Buffer beforehand) - (due to performance)</p> hifrog - To do #7862 (New): enable summary re-use in CUFhttps://scm.ti-edu.ch/issues/78622018-09-08T18:08:22ZSepideh Asadisepideh.a65@gmail.com
<p>CUF generates summary but does not reload(re-use) it.</p> hifrog - To do #7861 (New): A minimal necessary unwinding boundhttps://scm.ti-edu.ch/issues/78612018-09-07T20:19:13ZSepideh Asadisepideh.a65@gmail.com
<p>A minimal necessary unwinding bound<br />A lazy enumeration of unrollings, it is something that CBMC is doing in SVCOMP.</p> hifrog - To do #7860 (New): follow up in EUF summaries (Grisha's idea)https://scm.ti-edu.ch/issues/78602018-09-07T20:15:03ZSepideh Asadisepideh.a65@gmail.com
<p>The point is about the loop in function func which calculates a new value for variable b. This loop is not needed for verifying any of assertions. It cannot be removed by slicing because variable b is used later in the program. But it can be identified by our summarization procedure.</p>
<p>So idea is to 1) skip the loop at all, and thus treat b nondeterministically, 2) solve the whole BMC formula with EUF and get the UNSAT result, 3) interpolate and analyze the EUF summary for func. If variable b does not appear in the summary, then we can safely remove the loop and trust the summary. If b appears in the summary, then the result is not trustable, and we go back to the encoding of main program with loop, (unroll the loop perhaps, lazily?) and re-check. If the result is SAT, then of course we also need to go back to the unrolling.</p>
<p><strong>Note</strong>: <br />if you replace the assignment to b after the loop by nondet() and the formula is UNSAT, then you can trust the summary. But if you create an under-approximation of the loop (e.g., unroll it 1 / 2 / 5 / 10 times) and the formula is UNSAT then the summary is not trustable any more, and you may try the above trick.</p> hifrog - To do #7859 (New): checks for uninitialized locals in CBMChttps://scm.ti-edu.ch/issues/78592018-09-07T20:01:30ZSepideh Asadisepideh.a65@gmail.com
<p>CBMC in the goto-instrument program supports --uninitialized-check.<br />Since we updated cprover to version 5.10, it is well worth investigating.</p> hifrog - Bug #7805 (New): UFInterpolator.Chttps://scm.ti-edu.ch/issues/78052018-08-29T11:04:47ZSepideh Asadisepideh.a65@gmail.com
<p><strong>File</strong>: sumth60.c (attached)</p>
<p><strong>How to run:</strong><br />--logic qfuf --claim 2</p>
<p><strong>Error message:</strong><br />RESULT: UNSAT - it holds!<br />Start generating interpolants...<br />Assertion failed: (!sorted_edges.empty( ) || tmp.back( )->target == x), function getSortedEdges, file /Users/sepidehasadi/2phd/dev/opensmt2/src/tsolvers/egraph/UFInterpolator.C, line 2451.</p> hifrog - Bug #7795 (New): Type constraints option for LA theorieshttps://scm.ti-edu.ch/issues/77952018-08-29T08:08:26ZKarine Even Mendozakarine.even_mendoza@kcl.ac.uk
<p>Following Grigory answer, this code is a test for the assertion ordering than for the type constraints: assuming a >= 0 and b >= 0 we can easily derive that c >= 0.</p>
<p>The original code, suppose to run with type_constraints 1 and results in UNSAT. We can run the loop till 10 (no need for so many iterations). To prove claim 1 and 2 we need type-constraints 1, and using claim 1+2 we can prove claim 3 (I think via claims-opt option).</p>
<p>Older version of type-constraints use to work well. I think not all the added type-constraints are in the end added to the SMT query (can be the remove of incrementality).</p>
<p>=========================<br />The code:</p>
<pre>
int sum ()
{
int s=0;
unsigned n;
for (int i = 0; i <10; i++)
{
n = nondetUInt();
s=s+n;
}
return s;
}
int main()
{
int a,b,c;
a=sum();
assert(a>=0);
b=sum();
assert(b>=0);
c=a+b;
assert(c>=0);
}
</pre><br />Please add this test in the end to the regression test with reference to TACAS17 paper. hifrog - To do #7600 (Resolved): Cleaning check_sum_theoref_singlehttps://scm.ti-edu.ch/issues/76002018-07-09T21:16:52ZMartin Blichablicha@d3s.mff.cuni.cz
<p>Hack was used to go around OpenSMT problem in LRA incrementality.<br />This should be fixed now, so a new LRA solver does not need to be created in each iteration.</p>
<p>Rewrite the method so a single OpenSMT instance is used on LRA level.<br />Write tests for checking correctness.</p>