aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* invariant guaranteedDavid Monniaux2020-02-042-4/+56
|
* wellformedness for memoryDavid Monniaux2020-02-042-17/+158
|
* begin well formednessDavid Monniaux2020-02-042-15/+130
|
* stuff information into a recordDavid Monniaux2020-02-042-46/+63
|
* another version of proof that allows Vundef in loaded valuesDavid Monniaux2020-02-031-18/+18
|
* commentsDavid Monniaux2020-02-032-0/+14
|
* with loads too ?David Monniaux2020-01-282-8/+119
|
* load_soundDavid Monniaux2020-01-281-0/+96
|
* find_load_soundDavid Monniaux2020-01-281-4/+92
|
* begin adding loadsDavid Monniaux2020-01-281-2/+7
|
* much better - seems to eliminate CSE not containing loadsDavid Monniaux2020-01-282-2/+18
|
* still buggyDavid Monniaux2020-01-282-56/+95
|
* connected (just a silly problem)David Monniaux2020-01-281-2/+8
|
* CSE2 now works for expressionsDavid Monniaux2020-01-282-47/+69
|
* now going back to opDavid Monniaux2020-01-281-45/+6
|
* reworkDavid Monniaux2020-01-281-20/+49
|
* sem_rel_b_geDavid Monniaux2020-01-281-61/+152
| | | | progress
* sem_rel_b_geDavid Monniaux2020-01-281-18/+77
|
* CSE2 split in two filesDavid Monniaux2020-01-282-827/+837
|
* progressDavid Monniaux2020-01-271-0/+467
|
* use in transformationDavid Monniaux2020-01-271-3/+21
|
* find_op_soundDavid Monniaux2020-01-271-1/+110
|
* goes to the end but does not find available opsDavid Monniaux2020-01-271-13/+5
|
* simpler definitionsDavid Monniaux2020-01-271-41/+24
|
* static analysis doneDavid Monniaux2020-01-271-20/+7
|
* kill_mem_soundDavid Monniaux2020-01-271-8/+59
|
* renamed kill_reg into kill_memDavid Monniaux2020-01-271-11/+11
|
* gen_oper_soundDavid Monniaux2020-01-271-1/+37
|
* oper_soundDavid Monniaux2020-01-271-0/+27
|
* oper1_soundDavid Monniaux2020-01-271-1/+10
|
* arg replaceDavid Monniaux2020-01-271-1/+87
|
* move soundDavid Monniaux2020-01-271-19/+85
|
* begin proving stuffDavid Monniaux2020-01-271-0/+436
|
* Remove no longer needed file PrintLTLinBernhard Schommer2019-11-121-115/+0
|
* Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-022-8/+8
| | | | | | | Some hints will move from the core database to the `ordered_type` database (see https://github.com/coq/coq/pull/9772). This commit prepares for this move by adding `with ordered_type` to the invocations of `auto` and `eauto` that use the hints in question.
* 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".
* 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.
* 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.
* If-conversion optimizationXavier Leroy2019-06-064-72/+584
| | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
* Type inference and type checking for CminorXavier Leroy2019-06-061-0/+797
| | | | | | | This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-314-5/+5
| | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
generated by cgit (git 2.34.1) at 2024-07-04 11:01:00 +0000