aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Recording of prediction stats with COMPCERT_PROFILING_STATS environment flagCyril SIX2021-04-131-33/+93
| | | | | | | | | | | | | | | | | It only works correctly if both profiling and static prediction are used: it then compares both and gives stats in COMPCERT_PREDICT_STATS file. The stats are of the form: total correct mispredicts missed total = number of total CBs encountered correct = number of correct predictions mispredicts = times when static prediction did a wrong guess (predicted the opposite from profiling, or predicted Some _ when profiling said None) missed = times when static prediction was not able to give a verdict, though the profiling gave one
* removing unusued proof lineLéo Gourdin2021-04-091-1/+0
|
* Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-061-1/+2
|
* add has_type infoDavid Monniaux2021-01-311-1/+3
|
* Conditions now propagated by CSE3David Monniaux2021-01-205-264/+934
|\ | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
| * totally switch off conditions in cse3David Monniaux2020-12-092-16/+21
| |
| * begin implementing -fcse3-conditionsDavid Monniaux2020-12-092-8/+15
| |
| * CSE3 + conditions proofDavid Monniaux2020-12-092-34/+58
| |
| * apply_cond_soundDavid Monniaux2020-12-091-0/+14
| |
| * apply_cond0_soundDavid Monniaux2020-12-091-1/+25
| |
| * apply_cond1_soundDavid Monniaux2020-12-091-0/+30
| |
| * proof for jumptableDavid Monniaux2020-12-091-1/+27
| |
| * one 'admit' lessDavid Monniaux2020-12-091-2/+36
| |
| * avancement dans les preuvesDavid Monniaux2020-12-091-1/+34
| |
| * CSE3 compiles again, but some admitted lemmasDavid Monniaux2020-12-091-10/+8
| |
| * progress moving to list of itemsDavid Monniaux2020-12-093-92/+233
| |
| * analysis with Abst_sameDavid Monniaux2020-12-083-22/+39
| |
| * CSE3 now runs on its own fixpoint iterator not based on Kildall.vDavid Monniaux2020-12-082-114/+3
| |
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-0813-80/+183
| |\
| * | start checking for bugsDavid Monniaux2020-12-021-2/+115
| | |
| * | attempt at initial analysisDavid Monniaux2020-12-021-1/+35
| | |
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-024-5/+487
| |\ \
| * | | not yet the transfer functions that record predicatesDavid Monniaux2020-11-263-9/+78
| | | |
| * | | remains one admitDavid Monniaux2020-11-261-8/+46
| | | |
| * | | is_condition_present_soundDavid Monniaux2020-11-263-5/+23
| | | |
| * | | begin implementing cond tableDavid Monniaux2020-11-261-6/+13
| | | |
| * | | ajouté Cond, tout passeDavid Monniaux2020-11-263-40/+168
| | | |
| * | | passage à EquDavid Monniaux2020-11-263-189/+196
| | | |
| * | | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+14
| | | |
* | | | remove some useless "OK tt"Sylvain Boulmé2021-01-072-11/+11
| | | |
* | | | Merge branch 'kvx-work' of ↵David Monniaux2021-01-074-92/+13
|\ \ \ \ | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
| * | | | Making verify_mapping_mn_rec tail recursive (should fix arm CI) #231Cyril SIX2021-01-062-3/+2
| | | | |
| * | | | Solving a stack overflow issue (was failing in yarpgen ran000089 for armhf)Cyril SIX2021-01-061-9/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note : the issue is still present later in Duplicateproof. This is because I am examining an "identity ptree" which is way too big. I am having a look to see if I could make this ptree less big - to not include nodes that are identity
| * | | | Uniformizing a couple of debug print functionsCyril SIX2020-12-172-80/+2
| | | | |
* | | | | -fcse3-trivial-opsDavid Monniaux2021-01-072-3/+4
|/ / / /
* | | | Fixing wrong predictions on imbricated loopsCyril SIX2020-12-111-104/+114
| | | |
* | | | Fixing exponential blowup on get_loop_info.mark_path.exploreCyril SIX2020-12-091-33/+44
| | | |
* | | | Flushing debug outputCyril SIX2020-12-091-1/+1
| | | |
* | | | The last fix for get_loop_info was giving false positives. Fixing that.Cyril SIX2020-12-081-2/+12
| | | |
* | | | Fixing get_loop_info : part 2Cyril SIX2020-12-081-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 1Cyril SIX2020-12-081-16/+8
| | | | | | | | | | | | | | | | Various typos made the code fail silently for certain loops
* | | | Moving codeCyril SIX2020-12-081-71/+72
| | | |
* | | | More debugCyril SIX2020-12-081-6/+21
| | | |
* | | | More debugCyril SIX2020-12-081-3/+3
| | | |
* | | | Do not duplicate nodes that don't need to when unrolling the bodyCyril SIX2020-12-081-4/+18
| | | |
* | | | Fix on find_last_node_before_loopCyril SIX2020-12-081-3/+7
| |_|/ |/| | | | | | | | It was too permissive
* | | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0411-286/+1393
|\ \ \ | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * | | CommentCyril SIX2020-12-041-0/+1
| | | |
| * | | Less aggressive tail duplicationCyril SIX2020-12-041-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 debugCyril SIX2020-12-041-4/+2
| | | |
generated by cgit (git 2.34.1) at 2024-07-08 09:44:08 +0000