aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-085-26/+136
|\
| * Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0411-242/+577
| |\ | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-185-26/+136
| |\ \
| | * | Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
| | | | | | | | | | | | | | | | configure flags -use-external-Flocq and -use external-MenhirLib.
| | * | Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-1/+1
| | | | | | | | | | | | | | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
| | * | RISC-V implementation of __builtin_clz* and __builtin_ctz*Xavier Leroy2020-07-272-0/+134
| | | | | | | | | | | | | | | | Using binary search loops expanded at point of use.
| | * | No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
| | | | | | | | | | | | | | | | __builtin_fabs has already been expanded in backend/Selection.v .
| | * | Move shared code in new file.Bernhard Schommer2020-06-282-18/+0
| | | | | | | | | | | | | | | | | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
| | * | Remove the `can_reserve_register` function.Bernhard Schommer2020-06-282-3/+0
| | | | | | | | | | | | | | | | | | | | The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
| | * | Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | | | | | | | | | | | | | | | | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-029-239/+553
|\ \ \ \ | | |_|/ | |/| |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-242-3/+14
| |\ \ \
| * | | | allow changing the target coreDavid Monniaux2020-10-222-120/+160
| | | | |
| * | | | attempt at modeling RocketDavid Monniaux2020-10-221-0/+83
| | | | |
| * | | | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass ↵Sylvain Boulmé2020-10-171-0/+10
| | | | | | | | | | | | | | | | | | | | scheduler)
| * | | | so that all architectures compileDavid Monniaux2020-10-022-8/+16
| | | | |
| * | | | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-216-239/+390
| |\ \ \ \
| | * | | | risc-V now without trapping instructionsDavid Monniaux2020-09-214-74/+90
| | | | | |
| | * | | | moved Risc-V div ValueAOp to central locationDavid Monniaux2020-09-211-293/+0
| | | | | |
| | * | | | maketotal mod & divDavid Monniaux2020-09-216-165/+593
| | | |/ / | | |/| |
| * | | | wrong resourcesDavid Monniaux2020-09-181-1/+1
| | | | |
| * | | | EH1 schedulingDavid Monniaux2020-09-181-5/+18
| | | | |
| * | | | bogus OpWeights for Risc-VDavid Monniaux2020-09-181-0/+19
| |/ / /
* | | | op_depends_on_memory_correctDavid Monniaux2020-11-251-6/+24
| | | |
* | | | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+10
| | | |
* | | | pointer_eq copiedDavid Monniaux2020-11-251-0/+10
| |/ / |/| |
* | | fix bug #223 on Risc-VDavid Monniaux2020-11-232-3/+14
|/ /
* | Adding copyrightsCyril SIX2020-05-043-0/+38
| |
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-202-3/+11
|\ \
| * | test whether the instructions are allowedDavid Monniaux2020-04-191-0/+2
| | |
| * | porting to ppc riscV x86David Monniaux2020-04-011-3/+9
| | |
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-085-207/+329
|\| |
| * | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-261-7/+10
| |\|
| | * Update the RISC-V calling conventions, continued (#227)Xavier Leroy2020-03-021-7/+10
| | | | | | | | | | | | | | | | | | | | | | | | Double FP arguments passed on stack were incorrectly aligned: they must be 8-aligned but were 4-aligned only. This was due to the use of `Location.typealign`, which is the minimal hardware-supported alignment for a given type, namely 1 word for type Tfloat. To get the correct alignments, `Location.typesize` must be used instead.
| * | riscV/DuplicateOpcodeHeuristic.mlDavid Monniaux2020-03-171-3/+27
| | |
| * | fixes for risc-VDavid Monniaux2020-03-031-1/+1
| | |
| * | fix for risc-VDavid Monniaux2020-03-031-9/+7
| | |
| * | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-032-0/+149
| |\ \ | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| | * | CSE2 alias analysis for Risc-VDavid Monniaux2020-03-032-0/+149
| | |/
| * | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-0311-39/+189
| |\ \ | | |/ | |/| | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | Update the RISC-V calling conventions (#221)Xavier Leroy2020-02-262-137/+149
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We were implementing the ABI described in the RISC-V Instruction Set Manual, version 2.1. However, this ABI was superseded by the RISC-V ELF psABI specification. This commit changes the calling conventions to better match the ELF psABI specification. This should greatly improve interoperability with code compiled by other RISC-V compilers. One incompatibility remains: when all 8 FP argument registers have been used, further FP arguments should be passed in integer argument registers if available, while this PR passes them on stack.
| * | Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-64/+0
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The "size_arguments" function and its properties can be systematically derived from the "loc_arguments" function and its properties. Before, the RISC-V port used this derivation, and all other ports used hand-written "size_arguments" functions and proofs. This commit moves the definition of "size_arguments" to the platform-independent file backend/Conventions.v, using the systematic derivation, and removes the platform-specific definitions. This reduces code and proof size, and makes it easier to change the calling conventions.
* | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-253-13/+18
|\ \ \
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-243-13/+18
| |\| | | | |/ | |/| | | | mppa-work-upstream-merge
| | * Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-211-1/+1
| | | | | | | | | | | | | | | | | | "open!" is the form used in the examples in the OCaml manual. Based on a quick poll it seems to be the preferred form of the OCaml core dev team.
| | * Support re-normalization of values returned by function callsXavier Leroy2020-02-211-0/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Some ABIs leave more flexibility concerning function return values than CompCert expects. For example, the x86 ABI says that a function result of type "char" is returned in register AL, leaving the top 24 bits of register EAX unspecified, while CompCert expects EAX to contain 32 valid bits, namely the zero- or sign-extension of the 8-bit result. This commits adds a general mechanism to insert "re-normalization" conversions on the results of function calls. Currently, it only deals with results of small integer types, and inserts zero- or sign-extensions if so instructed by a platform-dependent function, Convention1.return_value_needs_normalization. The conversions in question are inserted early in the front-end, so that they can be optimized away in the back-end. The semantic preservation proof is still conducted against the CompCert model, where the return values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to return values that are not normalized.
| | * Refine the type of function results in AST.signatureXavier Leroy2020-02-212-12/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
* | | fixes for aarch64 arm ppc ppc64David Monniaux2020-02-241-1/+3
|/ /
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-081-2/+2
|\| | | | | | | mppa-work-upstream-merge
| * Incorrect computation of extra stack size for vararg calls in RISC-V (#213)Bernhard Schommer2020-02-051-2/+2
| | | | | | | | | | Currently, the extra size for the variable arguments is too small for the 64 bit RISC-V and the extra arguments are stored in the wrong stack slots.
generated by cgit (git 2.34.1) at 2024-07-04 02:53:51 +0000