USI & SUPSI Source Code Management (SCM): Issueshttps://scm.ti-edu.ch/https://scm.ti-edu.ch/favicon.ico?15601711372019-09-26T11:54:36ZUSI & SUPSI Source Code Management (SCM)
Redmine 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> hifrog - 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 #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 #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 - 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> hifrog - Bug #7280 (New): crash in solver in VTT (3)https://scm.ti-edu.ch/issues/72802018-05-07T17:49:28ZSepideh Asadisepideh.a65@gmail.com
<p>File is: /cprover/regression/funfrog/P2P_Joints_TG3_rec_1.c<br />Verification not successful; here is the last few lines: ...</p>
<ul>
<li>INLINING function: simpleDiv</li>
<li>INLINING function: sqrt_<br />Processing a deferred function: fabs_<br />Processing a deferred function: fabs_<br />Processing a deferred function: getNum<br />Processing a deferred function: simpleDiv<br />Processing a deferred function: sqrt_<br />Processing a deferred function: getNum<br />Processing a deferred function: simpleDiv<br />Processing a deferred function: sqrt_<br />SYMEX TIME: 0.348<br />All SSA steps: 16542<br />Ignored SSA steps after slice: 2925<br />SLICER TIME: 0.077<br />Incrementally adding partitions to the SMT solver<br />; uf_solver query time so far: 0.000029</li>
</ul>
<p>Command terminated by signal 6<br />real 162.77</p> hifrog - Bug #7279 (Resolved): crash in VTT (2)https://scm.ti-edu.ch/issues/72792018-05-07T17:38:50ZSepideh Asadisepideh.a65@gmail.com
<p>File is:.../cprover/regression/funfrog/VTT/P2P_Joints_TG3_e.c<br />File is:.../cprover/regression/funfrog/VTT/VTT1.c<br />File: /cprover/regression/funfrog/VTT/P2P_Joints_TG3_e_BUG.c<br />File /cprover/regression/funfrog/VTT/VTT.c<br />File /cprover/regression/funfrog/VTT/P2P_Joints_TG3_e.c</p>
<p>Claim number # 1 is SAFE</p>
<p>Caught exception: identifier tag-#anon#ST[S32'a1'|S32'a2'|S32'v'|S32't1'|S32't2'|S32't3'|S32'delta'|S32'initPos'|S32'initVel'] not found<br />time 108.58</p>
<hr /> hifrog - Bug #7278 (Resolved): crash in VTT (1)https://scm.ti-edu.ch/issues/72782018-05-07T15:10:45ZSepideh Asadisepideh.a65@gmail.com
<p><strong>File</strong>: /cprover/regression/funfrog/VTT/P2P_Joints_TG3_e_num_4.c</p>
<p><strong>how to run</strong>: ./hifrog --unwind 10 --sum-theoref</p>
<p><strong>Error log:</strong> <p>Verification not successful, here is the last few lines: ...</p>
</p>
<p>Processing a deferred function: sqrt_<br />Processing a deferred function: sqrt_<br />SYMEX TIME: 0.708<br />All SSA steps: 672<br />Ignored SSA steps after slice: 214<br />SLICER TIME: 0.007<br />; uf_solver query time so far: 0.000000<br />; 0 | 0 0 | 84.680 s | 871.938 MB</p>
<p>---trying to locally refine the summary in UF---</p>
<p>---EUF was not enough, lets change the encoding to LRA---</p>
<p>; Warning: disabling SATElite preprocessing to track proof<br />hifrog: ~/cprover/src/funfrog/solvers/smtcheck_opensmt2.cpp:1090: PTRef smtcheck_opensmt2t::substitute(smt_itpt&, const std::vector<symbol_exprt>&): Assertion `symbols.size() == static_cast<std::size_t>(args.size())' failed.<br />Command terminated by signal 6<br />time 85.37</p> hifrog - Bug #7274 (New): Caught exception: byte_extract flatting with negative offsethttps://scm.ti-edu.ch/issues/72742018-05-06T00:38:52ZSepideh Asadisepideh.a65@gmail.com
<p>File:<br />ntdrivers/kbfiltr_false-valid-deref.i.cil.c</p>
<p>how to run:<br />./hifrog --logic prop or --sum-theoref --unwind 10</p>
<p>Error message: <br />Caught exception: byte_extract flatting with negative offset: byte_extract_little_endian
* type: struct
* tag: _IO_STACK_LOCATION</p> hifrog - Bug #7271 (Feedback): crash in ldv-challenges as signal 6: what(): map::athttps://scm.ti-edu.ch/issues/72712018-05-03T16:14:05ZSepideh Asadisepideh.a65@gmail.com
<p>File:<br />~/hi-bench/challenge-bench/sv-comp17/c/ldv-challenges/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-ethernet-via-via-velocity_true-unreach-call.cil.c</p>
<p>---------------------------<br />How to run:<br />./hifrog --sum-theoref --unwind 10 file.c</p>
<p>---------------------------<br />Error msg:<br />Use QF_UF logic.<br />terminate called after throwing an instance of 'std::out_of_range'<br /> what(): map::at<br />Command terminated by signal 6</p>
<hr />
<p>initial observation:<br />the error is caused by hifrog asking for a goto function which is not known. There is a line of code in the program: <br />asm volatile ("lfence": : : "memory");</p>
<p>And perhaps it could come from there.</p> hifrog - Bug #5355 (New): /regression/hifrog/benchmarks/06_main5.chttps://scm.ti-edu.ch/issues/53552017-06-25T20:31:49ZSepideh Asadisepideh.a65@gmail.com
<p>/hifrog --claim 1 --theoref --no-itp --unwind 10 --bitwidth 32 --heuristic 4 /regression/hifrog/benchmarks/06_main5.c ---> SAT</p>
<p>Obtained counter-examples are refined<br />(15 / 26 expressions bit-blasted)<br />ASSERTION DOES NOT HOLD</p>
<p>VERIFICATION FAILED<br />TOTAL TIME FOR CHECKING THIS CLAIM: 16.787</p>
<p>------------------------------------------------<br />CBMC reports as SUCCESSFUL</p> hifrog - Bug #5330 (New): bug in cafe.c related to cprover frameworkhttps://scm.ti-edu.ch/issues/53302017-06-20T19:44:31ZSepideh Asadisepideh.a65@gmail.com
<p>hifrog: goto_symex_state.cpp:639: void goto_symex_statet::rename(exprt&, const namespacet&, goto_symex_statet::levelt): Assertion `to_if_expr(expr).true_case().type()== to_if_expr(expr).false_case().type()' failed.<br />Command terminated by signal 6</p>
<p>~/hifrog/trunk/cprover/src/funfrog/hifrog --claim 4 --theoref --no-itp --unwind 10 --bitwidth 32 --heuristic 4 cafe.c</p> hifrog - Bug #4998 (Feedback): bug in QF_BOOL: wrong result for prop in benchs in directrory ntdr...https://scm.ti-edu.ch/issues/49982017-04-12T15:03:35ZSepideh Asadisepideh.a65@gmail.com
<p>/hifrog --claim 1 --logic prop --bitwidth 8 --unwind 1 ~/hi-bench/challenge-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c</p>
<p>VERIFICATION FAILED</p>
<p>wrong result! because claim 1 should hold</p> hifrog - Bug #4997 (New): --theoref bug : quadratic explosion in ntdrivers-simplified benchmarkshttps://scm.ti-edu.ch/issues/49972017-04-12T12:34:01ZSepideh Asadisepideh.a65@gmail.com
<p>/hifrog --claim 1 --theoref ~/dev/hi-bench/challenge-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c</p>
<p>Parts of debug:<br />...<br />....<br />; Warning: disabling SATElite preprocessing to track proof<br />^C^C<br />Program received signal SIGINT, Interrupt.<br />0x00000000005c300a in operator!= (a1=..., a2=...)<br /> at /home/asadis/dev/opensmt-debug/include/opensmt/Pterm.h:43<br />43 inline friend bool operator!= (const PTRef& a1, const PTRef& a2) { return a1.x != a2.x; }<br />(gdb) bt <br />#0 0x00000000005c300a in operator!= (a1=..., a2=...)<br /> at /home/asadis/dev/opensmt-debug/include/opensmt/Pterm.h:43<br />#1 0x00007ffff7acc7f4 in operator== (k1=..., k2=...) at ../../src/pterms/Pterm.h:69<br />#2 0x00007ffff7ad0e01 in Equal<PTLKey>::operator() (this=0x1d53ae9, k1=..., k2=...)<br /> at ../../src/minisat/mtl/Map.h:32<br />#3 0x00007ffff7ace677 in Map<PTLKey, PTRef, PTLHash, Equal<PTLKey> >::has (<br /> this=0x1d53ae8, k=...) at ../../src/minisat/mtl/Map.h:149<br />#4 0x00007ffff7accece in PtStore::hasBoolKey (this=0x1d539c0, k=...)<br /> at ../../src/pterms/PtStore.h:175<br />#5 0x00007ffff7ac5acf in Logic::insertTermHash (this=0x1d53708, sym=..., terms_in=...)<br /> at Logic.C:1111<br />#6 0x00007ffff7ac44e7 in Logic::mkEq (this=0x1d53708, args=...) at Logic.C:831<br />#7 0x00000000005ccaf2 in Logic::mkEq (this=0x1d53708, a1=..., a2=...)<br /> at /home/asadis/dev/opensmt-debug/include/opensmt/Logic.h:279<br />#8 0x00007ffff7aec8e8 in BVLogic::mkEq (this=0x1d53708, a1=..., a2=...) at BVLogic.h:274<br />#9 0x00007ffff7a7b942 in BitBlaster::notifyEquality (this=0x1e93410, tr=...)<br /> at BitBlaster.C:2202<br />#10 0x00007ffff7a7b449 in BitBlaster::notifyEqualities (this=0x1e93410)<br /> at BitBlaster.C:2162<br />#11 0x00000000005db719 in smtcheck_opensmt2t_cuf::refine_ce_mul (this=0x1e647e0, <br /> exprs=std::vector of length 2594, capacity 4096 = {...}, <br /> is=std::set with 1184 elements = {...}) at solvers/smtcheck_opensmt2_cuf.cpp:1442<br />#12 0x00000000005a58e1 in theory_refinert::assertion_holds_smt (this=0x7fffffffd2c0, <br /> assertion=..., store_summaries_with_assertion=true) at theory_refiner.cpp:178<br />#13 0x0000000000576027 in check_claims (ns=..., leaping_program=..., goto_functions=..., <br /> claim_map=std::map with 1 elements = {...}, <br /> claim_numbers=std::map with 2 elements = {...}, options=..., _message_handler=..., <br /> claim_nr=1) at check_claims.cpp:177<br />#14 0x0000000000570cf2 in funfrog_parseoptionst::check_function_summarization (<br /> this=0x7fffffffdd90, ns=..., goto_functions=...) at parseoptions.cpp:541<br />#15 0x0000000000570395 in funfrog_parseoptionst::doit (this=0x7fffffffdd90)<br />---Type <return> to continue, or q <return> to quit---q<br /> at parseoptionQuit<br />(gdb) f 9<br />....<br />...<br />main reason for this bug:<br />Theory combination between BV and CUF</p>
<p>need to be added millions of equalities in binding, indicating that qfcuf holds if and only if BV holds.</p> cow - Bug #862 (New): Cow doesn't compile for Moose Build 43 (PULL REQUEST)https://scm.ti-edu.ch/issues/8622015-07-06T13:00:51ZErich Fostererich.foster@usi.ch
<p>The master branch still doesn't compile for the latest version of Moose. The problem is _f in include/materials/GuccioneCostaRot.h this should be a constant.</p>