aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* simplification of Duplicate: remove xfunctionSylvain Boulmé2019-11-142-187/+154
|
* Merge remote-tracking branch 'origin/mppa-duplicate-rtl-alt' into mppa-workCyril SIX2019-10-242-60/+77
|\
| * An alternative proof where the match_state does not depend on the translationSylvain Boulmé2019-10-232-60/+77
| |
* | eq_condition already existedDavid Monniaux2019-10-162-2/+2
| |
* | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-1610-51/+146
|\ \ | |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * Reworked json export.Bernhard Schommer2019-09-123-29/+37
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The json export prints formatted json, which takes a lot of additional time, however the result is only consumed by other tools and not meant for human reading. This commit implements several small changes in order to speedup the json export: * Removal of usage of the Format Module * Replacing `fprintf` calls by calls to function that print directly, such as `output_string`, etc. * Replacing list of all instruction names by a set of all instructions
| * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
| | | | | | Some changes were not correctly propagated to all architectures.
| * AArch64 portXavier Leroy2019-08-087-37/+97
| | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
| * Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
| | | | | | | | | | | | | | | | | | | | This is a variant of exec_straight where it is allowed to take zero steps. In other words, exec_straight0 is the "star" relation, while exec_straight is the "plus" relation. In the end we need "plus" relations in simulation diagrams, to show the absence of stuttering. But the "star" relation exec_straight0 is useful to reason about code fragments that are always preceded or followed by at least one instruction.
| * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+0
| | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* | Finished Duplicate proof.Cyril SIX2019-10-072-36/+58
| |
* | IcondCyril SIX2019-10-072-0/+26
| |
* | Fixing identity PTree in Duplicateaux oracleCyril SIX2019-10-071-2/+8
| |
* | ItailcallCyril SIX2019-10-072-2/+17
| |
* | IreturnCyril SIX2019-10-072-1/+9
| |
* | Ibuiltin proofCyril SIX2019-10-042-0/+31
| |
* | IcallCyril SIX2019-10-032-0/+27
| |
* | Iload and IstoreCyril SIX2019-10-032-3/+43
| |
* | Proof for IopCyril SIX2019-10-032-1/+20
| |
* | Preparing the terrain for the rest of the instructions with one successorCyril SIX2019-10-031-5/+17
| |
* | Duplicate - Proof of verificator for InopCyril SIX2019-10-032-4/+83
| |
* | Starting implementing the verificatorCyril SIX2019-10-022-1/+34
| |
* | Identity oracle realizing verify_mapping_entrypointCyril SIX2019-10-021-1/+4
| |
* | Proof of first axiomCyril SIX2019-09-112-4/+25
| |
* | Fixing Linking problemCyril SIX2019-09-112-31/+31
| |
* | Utilisation d'un intermédiaire xfunction contenant le revmapCyril SIX2019-09-112-47/+81
| |
* | Duplicate: proof complete, assuming revmap, revmap_correct and revmap_entrypointCyril SIX2019-09-061-5/+21
| |
* | Duplicate: big progress on step_simulation, only Ijumptbl leftCyril SIX2019-09-053-85/+148
| |
* | Duplicate: changement de match_nodesCyril SIX2019-09-041-36/+44
| |
* | Duplicate: exec_function_external et exec_returnCyril SIX2019-09-041-3/+7
| |
* | Duplicate: exec_function_internalCyril SIX2019-09-042-2/+43
| |
* | transf_initial_statesCyril SIX2019-09-043-12/+84
| |
* | Duplicate: match_statesCyril SIX2019-09-031-2/+10
| |
* | Duplicate: match_nodesCyril SIX2019-09-031-8/+57
| |
* | Start of match_statesCyril SIX2019-09-031-3/+23
| |
* | Stubs for Duplicate passCyril SIX2019-09-033-0/+63
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-08-281-2/+0
|\ \ | | | | | | | | | mppa-work-upstream-merge
| * | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-051-2/+0
| |/ | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* | various fixesDavid Monniaux2019-07-193-24/+4
| |
* | helpers broke compilationDavid Monniaux2019-07-192-11/+0
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-1917-128/+466
|\| | | | | | | mppa-work-upstream-merge
| * Improve CSE for known built-in functionsXavier Leroy2019-07-172-7/+14
| | | | | | | | Known built-in functions are guaranteed not to change memory.
| * Perform constant propagation for known built-in functionsXavier Leroy2019-07-174-16/+168
| | | | | | | | | | | | | | When an external function is a known built-in function and it is applied to compile-time integer or FP constants, we can use the known semantics of the builtin to compute the result at compile-time.
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-112/+231
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later.
| * Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-086-7/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
| * Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-051-3/+3
| | | | | | | | | | Easier to type, and consistent with `-Os` (optimize for smaller code / optimize for fewer conditional branches).
| * Extended asm: print register names according to their typesXavier Leroy2019-06-171-9/+14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When printing an extended asm code fragment, placeholders %n are replaced by register names. Currently we ignore the fact that some assemblers use different register names depending on the width of the data that resides in the register. For example, x86_64 uses %rax for a 64-bit quantity and %eax for a 32-bit quantity, but CompCert always prints %rax in extended asm statements. This is problematic if we want to use 32-bit integer instructions in extended asm, e.g. int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); produces addl %rax, %rdx which is syntactically incorrect. Another example is ARM FP registers: D0 is a double-precision float, but S0 is a single-precision float. This commit partially solves this issue by taking into account the Cminor type of the asm parameter when printing the corresponding register. Continuing the previous example, int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); now produces addl %eax, %edx This is not perfect yet: we use Cminor types, because this is all we have at hand, and not source C types, hence "char" and "short" parameters are still printed like "int" parameters, which is not good for x86. (I.e. we produce %eax where GCC might have produced %al or %ax.) We'll leave this issue open.
* | finish merging master branch (fixes problems in glpk colamd)David Monniaux2019-06-063-43/+0
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-06-063-5/+59
|\|
| * Cminortyping: relax typechecking of function callsXavier Leroy2019-06-061-12/+15
| | | | | | | | | | | | | | Sometimes the result of a void function is assigned to a variable. This can occur with C conditional expressions ?: at type void, e.g. the "assert" macro of MacOS. A similar relaxation was already there in RTLtyping.
generated by cgit (git 2.34.1) at 2024-07-12 01:22:05 +0000