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> 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 - Bug #7760 (New): Infinite loop in theory refinementhttps://scm.ti-edu.ch/issues/77602018-08-24T14:05:23ZMartin Blichablicha@d3s.mff.cuni.cz
<p>In current version (e.g. f4aaed49) there is bug in theory refinement algorithm. In cases 6 and 7 there is an infinite loop.<br />The variable in the condition (last) is not modified inside the loop.</p>
<p>case 7 :<br /> // backward with multiple refinement & dependencies<br /> last = exprs.size()-1;
{<br /> while (last >= 0){<br /> smtcheck_opensmt2t_cuf decider2(bw,<br /> options.get_unsigned_int_option("type-byte-constraints"),<br /> "backward with multiple refinement & dependencies" <br /> );<br /> decider2.check_ce(exprs, model, refined, weak, last, -1, -1, 1);<br /> }<br /> }<br /> break;</p> hifrog - To do #7728 (New): Refactor theory refinement codehttps://scm.ti-edu.ch/issues/77282018-08-21T11:36:10ZMartin Blichablicha@d3s.mff.cuni.cz
<p>Code related to theory refinement should be refactored/simplfied.<br />Karine should have some version prepared.</p>