github-actions[bot]
commented
3 months ago Test Results
9 files ±0 20 suites ±0 0s :stopwatch: ±0s 645 tests +2 645 :white_check_mark: +2 0 :zzz: ±0 0 :x: ±0 2 057 runs ±0 2 056 :white_check_mark: ±0 1 :zzz: ±0 0 :x: ±0
Results for commit 72802df7. ± Comparison against base commit 3d66dddc.
This pull request removes 4 and adds 6 tests. Note that renamed tests count towards both.
``` load_store_dep.sat.sail mem_builtins.unsat.sail store_load.sat.sail store_load_scattered.sat.sail ``` ``` issue573_1.sat.sail issue573_2.sat.sail linked_int.unsat.sail linked_int2.unsat.sail revrev_endianness2.unsat.sail revrev_endianness3.unsat.sail ```:recycle: This comment has been updated with latest results.
This commit reworks the Sail->SMT backend to use the new shared primtive generation logic that Sail->SV uses. Various older features have been removed to simplify the code.
The Sail->SV backend has been refactored to use modules rather than just functions, but this has left it in quite the broken state for the time being.
There are a few known issues with the Sail->SMT pipeline that pre-date this commit, for example function arguments with complex constraints are sometimes generalised, and we would require additional well-formedness checks to be inserted to guard against this. There is now a small test that demonstrates the lack of these well-formedness checks in Sail->SMT.
Fix path condition computation to use post-dominators in order to handle cases where the graph has some non-structured control flow.