aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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-092-11/+9
|
* progress moving to list of itemsDavid Monniaux2020-12-093-92/+233
|
* CSE3 with Abst_sameDavid Monniaux2020-12-081-1/+1
|
* analysis with Abst_sameDavid Monniaux2020-12-083-22/+39
|
* CSE3 now runs on its own fixpoint iterator not based on Kildall.vDavid Monniaux2020-12-083-115/+4
|
* Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-084-555/+242
|\
| * fix new register erasing scheme for AArch64David Monniaux2020-12-083-553/+241
| |
| * rm instructions now unusedDavid Monniaux2020-12-081-2/+1
| |
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-08157-2244/+4035
|\|
| * Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-0818-115/+48
| |\
| | * Error when using -main without -interpXavier Leroy2020-12-061-0/+2
| | | | | | | | | | | | | | | | | | Outside of -interp mode, -main has no (known) effect but could be confused for a linker option that sets the program's entrypoint, say. It's safer to reject the option.
| | * PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | | | | | | | | | | | Inlined built-in functions destroy GPR0
| | * ARM modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | | | | | | | | | | | | | | Pflid destroys IR14 Inlined built-in functions destroy IR14
| | * AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-8/+11
| | | | | | | | | | | | | | | | | | Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30
| | * Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-0612-99/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat PowerPC operations. The pseudoinstructions were used to implement these operations, as follows: Pfcfi : Ofloatofint i.e. the conversion signed int32 -> float64 Pfcfiu : Ofloatofintu i.e. the conversion unsigned int32 -> float64 Pfctiu : Ointuoffloat i.e. the conversion float64 -> unsigned int32 These pseudoinstructions were expanded (in Asmexpand.ml) in terms of Pfcfid : signed int64 -> float64 Pfctidz : float64 -> signed int64 and int32/int64 conversions. This commit performs this expansion during instruction selection (SelectOp.vp): floatofint(n) becomes floatoflong(longofint(n)) floatofintu(n) becomes floatoflong(longuofint(n)) intuoffloat(n) becomes cast32unsigned(longoffloat(n)) Then there is no need for the 3 removed operations and the 3 removed pseudoinstructions. More importantly, the correctness of these expansions is now proved as part of instruction selection, using the corresponding results from Floats.v.
| * | Fixing test/regression for KVXv3.8_kvxCyril SIX2020-12-076-2/+409
| | |
| * | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-04104-1053/+11993
| |\ \ | | | | | | | | | | | | | | | | | | | | 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
| | | |
| | * | Fixed infinite loop on find_last_node_before_loopCyril SIX2020-12-041-3/+6
| | | | | | | | | | | | | | | | Happened when a loop was predicted not to be taken
| | * | Slight perf improvementCyril SIX2020-12-022-4/+4
| | | |
| | * | [expensive] Behavior change when the loop has two final instructionsCyril SIX2020-12-021-9/+57
| | | | | | | | | | | | | | | | | | | | Right now though the compilation time is too high for glpk, I need to figure out why
| | * | Duplicateaux: Generalization of look_aheadCyril SIX2020-12-011-3/+5
| | | |
| * | | Fixing compilation for KVXCyril SIX2020-12-043-2/+7
| | | |
| * | | still issues with FR in kvxDavid Monniaux2020-12-033-27/+26
| | | |
| * | | some fixes for KVXDavid Monniaux2020-12-032-6/+0
| | | |
| * | | fix Makefile pour kvxDavid Monniaux2020-11-191-1/+1
| | | |
| * | | un peu de progrès sur le MakefileDavid Monniaux2020-11-191-1/+1
| | | |
| * | | Asmgenproof1 pas sur kvxDavid Monniaux2020-11-191-1/+5
| | | |
| * | | essai de limitation des paquets KalrayDavid Monniaux2020-11-191-1/+1
| | | |
| * | | rm unneeded open statements in MLDavid Monniaux2020-11-191-3/+0
| | | |
| * | | fix MakefileDavid Monniaux2020-11-191-1/+1
| | | |
| * | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-18133-2071/+3462
| |\ \ \ | | | |/ | | |/|
| | * | Updates for release 3.8v3.8Xavier Leroy2020-11-163-5/+10
| | | |
| | * | Do not use -warn-error when building from a release tarballXavier Leroy2020-11-141-2/+9
| | | | | | | | | | | | | | | | | | | | Stopping on warnings is useful for development builds, but unhelpful for released software.
| | * | Support Coq 8.12.1Xavier Leroy2020-11-142-3/+3
| | | |
| | * | Update READMEXavier Leroy2020-11-091-4/+4
| | | |
| | * | Update ChangesXavier Leroy2020-11-081-0/+48
| | | |
| | * | Added semantics for the PowerPC sel and mulh built-insBernhard Schommer2020-11-071-4/+44
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The semantics of the various selection functions are defined analogously to the ones from the type generic sel function. The semantics for the various high word multiplication functions is defined using the Integer functions. Bug 30035
| | * | Added missing printer for PowerPC 64 bit comparison.Bernhard Schommer2020-11-061-0/+8
| | | | | | | | | | | | | | | | | | | | These comparisons are supported in the hybrid 64 bit mode. Bug 30035
| | * | Added implementation for fmin/fmax for aarch64.Bernhard Schommer2020-11-063-0/+12
| | | | | | | | | | | | | | | | | | | | The two built-in function map to the fmax and fmin instruction. Bug 30035
| | * | Better "make clean"Xavier Leroy2020-11-011-1/+1
| | | |
| | * | Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-304-20/+42
| | | | | | | | | | | | | | | | | | | | | | | | | | | | When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function. This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option. The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.
| | * | Add `string_of_ident` conversionXavier Leroy2020-10-121-0/+110
| | | | | | | | | | | | | | | | | | | | | | | | This is the left inverse of `ident_to_string`. Closes: #372
| | * | Remove -version-file optionXavier Leroy2020-10-121-19/+2
| | | | | | | | | | | | | | | | It is specific to AbsInt's commercial version of CompCert.
| | * | Support Cygwin 64 bitsXavier Leroy2020-10-0517-118/+415
| | | | | | | | | | | | | | | | | | | | | | | | - Add support for the Win64 ABI to the x86_64 port - Update vararg support to handle Win64 conventions - Configure support for x86_64-cygwin64
| | * | Test clightgen with -short-idents and -normalize optionsXavier Leroy2020-09-221-0/+6
| | | | | | | | | | | | | | | | Use different combination of options for different test files.
generated by cgit (git 2.34.1) at 2024-07-06 15:00:49 +0000