Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | | | | | Flushing debug output | Cyril SIX | 2020-12-09 | 1 | -1/+1 | |
| | | | | | ||||||
* | | | | | The last fix for get_loop_info was giving false positives. Fixing that. | Cyril SIX | 2020-12-08 | 1 | -2/+12 | |
| | | | | | ||||||
* | | | | | Fixing get_loop_info : part 2 | Cyril SIX | 2020-12-08 | 1 | -8/+28 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Loops with multiple CBs were only partially predicted for some cases (the header CB would get predicted, but not the CBs inside) This would happen in the case of breaks leading to another loop, such as: ```c void lift_check_level() { int i; int middle = lift_one_level >> 2; if ( lift_cntValid ) { for ( lift_level = 1; lift_level < 14; ++lift_level ) { if ( lift_cnt < lift_levelPos[lift_level] - middle ) break; /* This break */ } } else lift_level = 0; for ( i = 0; i < 14; ++i ) lift_ctrl_io_led[i] = ( i == lift_level - 1 ); } ``` | |||||
* | | | | | Fixing loop detection in get_loop_info - part 1 | Cyril SIX | 2020-12-08 | 1 | -16/+8 | |
| | | | | | | | | | | | | | | | | | | | | Various typos made the code fail silently for certain loops | |||||
* | | | | | Moving code | Cyril SIX | 2020-12-08 | 1 | -71/+72 | |
| | | | | | ||||||
* | | | | | More debug | Cyril SIX | 2020-12-08 | 1 | -6/+21 | |
| | | | | | ||||||
* | | | | | More debug | Cyril SIX | 2020-12-08 | 1 | -3/+3 | |
| | | | | | ||||||
* | | | | | Do not duplicate nodes that don't need to when unrolling the body | Cyril SIX | 2020-12-08 | 1 | -4/+18 | |
| | | | | | ||||||
* | | | | | Fix on find_last_node_before_loop | Cyril SIX | 2020-12-08 | 1 | -3/+7 | |
| |_|/ / |/| | | | | | | | | | | | It was too permissive | |||||
* | | | | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 11 | -286/+1393 | |
|\ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure | |||||
| * | | | | Comment | Cyril SIX | 2020-12-04 | 1 | -0/+1 | |
| | | | | | ||||||
| * | | | | Less aggressive tail duplication | Cyril SIX | 2020-12-04 | 1 | -6/+11 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | In some cases of two imbricated loops, we would tail-duplicate too much, because of the input trace traversing both loop headers. | |||||
| * | | | | Clean-up debug | Cyril SIX | 2020-12-04 | 1 | -4/+2 | |
| | | | | | ||||||
| * | | | | Fixed infinite loop on find_last_node_before_loop | Cyril SIX | 2020-12-04 | 1 | -3/+6 | |
| | | | | | | | | | | | | | | | | | | | | Happened when a loop was predicted not to be taken | |||||
| * | | | | Slight perf improvement | Cyril SIX | 2020-12-02 | 1 | -2/+2 | |
| | | | | | ||||||
| * | | | | [expensive] Behavior change when the loop has two final instructions | Cyril SIX | 2020-12-02 | 1 | -9/+57 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | Right now though the compilation time is too high for glpk, I need to figure out why | |||||
| * | | | | Duplicateaux: Generalization of look_ahead | Cyril SIX | 2020-12-01 | 1 | -3/+5 | |
| | |/ / | |/| | | ||||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | Cyril SIX | 2020-12-01 | 3 | -8/+161 | |
| |\| | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: arm/Op.v common/Values.v kvx/Op.v | |||||
| | * | | store2_sound | David Monniaux | 2020-11-25 | 1 | -1/+1 | |
| | | | | ||||||
| | * | | clever_kill_store_sound | David Monniaux | 2020-11-25 | 1 | -7/+5 | |
| | | | | ||||||
| | * | | kill_store_sound | David Monniaux | 2020-11-25 | 1 | -0/+49 | |
| | | | | ||||||
| | * | | two lemmas admitted | David Monniaux | 2020-11-25 | 3 | -9/+115 | |
| | | | | ||||||
| * | | | Ignore loopback edges on tail-duplicate | Cyril SIX | 2020-12-01 | 1 | -0/+2 | |
| | | | | ||||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-24 | 1 | -2/+2 | |
| |\| | | ||||||
| | * | | tiny simplification in Tunnelingaux.ml | Sylvain Boulmé | 2020-11-24 | 1 | -2/+2 | |
| | | | | ||||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-19 | 4 | -257/+672 | |
| |\| | | ||||||
| | * | | minor fix in coq2html comment | Sylvain Boulmé | 2020-11-16 | 1 | -1/+2 | |
| | | | | ||||||
| | * | | Tunneling: improved elimination of conditions | Sylvain Boulmé | 2020-11-16 | 4 | -256/+670 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, the elimination of useless conditions done in the 2nd pass of the tunneling introduced some new "nop" instructions that were not eliminated. This commit solves this issue by anticipating the elimination of conditions in the 1st pass of the tunneling, the 2nd pass being unchanged. In case of cycles in the CFG, the full elimination of useless conditions may require several iterations in the 1st pass. Moreover, in the simulation proof, the measure counting the number of eliminated steps from each node, needs to be adapted according to the modifications on the 1st pass. Hence, this measure results from a quite complex fixpoint computation: proving its properties would be very difficult. This leads us to introduce an oracle, implementing the first pass and producing the expected measure. A certified verifier directly checks that the measure provided by the oracle satisfies the properties expected by the simulation proof. Introducing this oracle/verifier pair has here the following advantage: - the proof is simpler than the original one (e.g. having a certified union-find structure is no more necessary for this pass). - the oracle is very efficient, by using imperative data-structure to compute memoized fixpoints. At runtime, the overhead induced by the verifier computations (and the actual computation of the measure) seems largely compensated by the gains obtained through the imperative oracle. | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-06 | 2 | -27/+32 | |
| |\| | | ||||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-05 | 3 | -28/+109 | |
| |\ \ \ | ||||||
| * \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-04 | 1 | -1/+2 | |
| |\ \ \ \ | ||||||
| * \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-03 | 4 | -35/+114 | |
| |\ \ \ \ \ | ||||||
| * \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-31 | 3 | -17/+118 | |
| |\ \ \ \ \ \ | ||||||
| * \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-30 | 4 | -168/+78 | |
| |\ \ \ \ \ \ \ | ||||||
| * \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-29 | 4 | -48/+107 | |
| |\ \ \ \ \ \ \ \ | ||||||
| * \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-28 | 3 | -40/+24 | |
| |\ \ \ \ \ \ \ \ \ | ||||||
| * \ \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 4 | -19/+110 | |
| |\ \ \ \ \ \ \ \ \ \ | ||||||
| * | | | | | | | | | | | improved CSE3 | David Monniaux | 2020-10-27 | 1 | -12/+12 | |
| | | | | | | | | | | | | ||||||
| * | | | | | | | | | | | progress in proofs on new CSE3 | David Monniaux | 2020-10-27 | 1 | -3/+34 | |
| | | | | | | | | | | | | ||||||
| * | | | | | | | | | | | deactivate LICM by default | David Monniaux | 2020-10-27 | 1 | -20/+11 | |
| | | | | | | | | | | | | ||||||
| * | | | | | | | | | | | begin fixing CSE3 to keep more inductive stuff | David Monniaux | 2020-10-27 | 2 | -10/+19 | |
| | | | | | | | | | | | | ||||||
| * | | | | | | | | | | | invariant printing more aligned with RTL dumps | David Monniaux | 2020-10-27 | 1 | -2/+2 | |
| | | | | | | | | | | | | ||||||
| * | | | | | | | | | | | print invariants | David Monniaux | 2020-10-27 | 1 | -11/+46 | |
| | | | | | | | | | | | | ||||||
| * | | | | | | | | | | | attempt at store -> load.s | David Monniaux | 2020-10-26 | 1 | -2/+3 | |
| | | | | | | | | | | | | ||||||
| * | | | | | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 8 | -143/+845 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-02 | 1 | -2/+9 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepass | David Monniaux | 2020-09-21 | 1 | -1/+482 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||||
| | * | | | | | | | | | | | | | risc-V now without trapping instructions | David Monniaux | 2020-09-21 | 1 | -0/+24 | |
| | | | | | | | | | | | | | | | ||||||
| | * | | | | | | | | | | | | | moved Risc-V div ValueAOp to central location | David Monniaux | 2020-09-21 | 1 | -0/+215 | |
| | | | | | | | | | | | | | | | ||||||
| | * | | | | | | | | | | | | | moved some "total" value domain functions to a central location | David Monniaux | 2020-09-21 | 1 | -1/+243 | |
| | | | | | | | | | | | | | | |