aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
Commit message (Collapse)AuthorAgeFilesLines
...
| * | Bugfix livenessLéo Gourdin2021-03-231-12/+8
| | |
| * | Remove first nop when doing expansionLéo Gourdin2021-03-211-188/+212
| | |
| * | Adding miniCSE here tooLéo Gourdin2021-03-081-10/+10
| | |
| * | Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexpLéo Gourdin2021-03-068-182/+245
| |\ \
| | * | some simplification in miniCSELéo Gourdin2021-03-061-17/+14
| | | |
| | * | Adding a mini CSE pass in the expansion oracleLéo Gourdin2021-03-068-193/+263
| | | |
| * | | Adding a flag to test fp_init_expLéo Gourdin2021-03-021-150/+157
| | | |
| * | | Adding fp init expansionsLéo Gourdin2021-03-021-0/+15
| | | |
| * | | Merge remote-tracking branch 'origin/riscv-still-asmcondexp' into ↵Léo Gourdin2021-03-023-96/+1088
| |\ \ \ | | | | | | | | | | | | | | | riscv-work-fpinit-stillexp
| | * | | Asmcondexp branche useful to benchmark expansionsLéo Gourdin2021-03-023-96/+1088
| | |/ /
| * / / [Admitted checker] Oracle expansion for float/float32 constant initLéo Gourdin2021-03-022-6/+27
| |/ /
* | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-015-16/+24
| | | | | | | | | | | | cfrontend/C2C.ml
* | | replacing omega with lia in some fileLéo Gourdin2021-03-292-9/+9
| | |
* | | fix riscv merge?Léo Gourdin2021-03-295-488/+0
| | |
* | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2311-177/+761
|\ \ \ | |/ / |/| / | |/ | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-2/+2
| | | | | | | | | | | | | | This is a generalization of the previous PrintAsmaux.common_section function that - handles initialized variables in addition to uninitialized variables; - can be used for Section_const, not just for Section_data.
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-1/+1
| | | | | | | | | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
| * Support re-normalization of function parameters at function entryXavier Leroy2021-01-161-1/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is complementary to 28f235806 Some ABIs leave more flexibility concerning function parameters than CompCert expects. For instance, the AArch64/ELF ABI allow the caller of a function to leave unspecified the "padding bits" of function parameters. As an example, a parameter of type "unsigned char" may not have zeros in bits 8 to 63, but may have any bits there. When the caller is compiled by CompCert, it normalizes argument values to the parameter types before the call, so padding bits are always correct w.r.t. the type of the argument. This is no longer guaranteed in interoperability scenarios, when the caller is not compiled by CompCert. This commit adds a general mechanism to insert "re-normalization" conversions on the parameters of a function, at function entry. This is controlled by the platform-dependent function Convention1.return_value_needs_normalization. The semantic preservation proof is still conducted against the CompCert model, where the argument 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 pass arguments that are not normalized.
| * RISC-V: fix FP calling conventionsXavier Leroy2021-01-144-117/+171
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a follow-up to e81d015e3. In the RISC-V ABI, FP arguments to functions are passed in integer registers (or pairs of integer registers) in two cases: 1- the FP argument is a variadic argument 2- the FP argument is a fixed argument but all 8 FP registers reserved for parameter passing have been used already. The previous implementation handled only case 1, with some problems. This commit implements both 1 and 2. To this end, 8 extra FP caller-save registers are used to hold the values of the FP arguments that must be passed in integer registers. Fixup code moves these FP registers to integer registers / register pairs. Symmetrically, at function entry, the integer registers / register pairs are moved back to the FP registers. 8 extra FP registers is enough because there are only 8 integer registers used for parameter passing, so at most 8 FP arguments may need to be moved to integer registers.
| * RISC-V: wrong fixup code generated for vararg calls with fixed FP argsXavier Leroy2021-01-101-12/+18
| | | | | | | | | | | | | | | | | | This is a follow-up to 2076a3bb3. Integer registers were wrongly reserved for fixed FP arguments, causing variadic FP arguments to end up in the wrong integer registers. Added regression test in test/regression/varargs2.c
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-299-76/+76
| | | | | | | | | | | | | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
| * RISC-V: revised calling conventions for variadic functionsXavier Leroy2020-12-252-63/+105
| | | | | | | | | | Fixed (non-variadic) arguments follow the standard calling conventions. It's only the variadic arguments that need special treatment.
| * Changed cc_varargs to an option typeBernhard Schommer2020-12-252-4/+5
| | | | | | | | | | | | Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs.
* | Merge conflicts solved and cleaning in Asmgenproof after expansionLéo Gourdin2021-03-024-1148/+106
| |
* | Merge remote-tracking branch 'origin/riscV-cmov' into riscv-workLéo Gourdin2021-03-0214-19/+624
|\ \
| * | Adding missing operators in PrintOp for debuggingLéo Gourdin2021-02-251-0/+5
| | |
| * | écrase X31riscV-cmovDavid Monniaux2021-02-031-1/+2
| | |
| * | Merge remote-tracking branch 'origin/kvx-work' into riscV-cmovDavid Monniaux2021-02-031-1/+1
| |\ \
| * | | detect redundant cmovDavid Monniaux2021-02-022-3/+34
| | | |
| * | | fix code generation for select(b, r, r)David Monniaux2021-02-021-2/+7
| | | |
| * | | fix problem if rt = rfDavid Monniaux2021-02-021-6/+8
| | | |
| * | | Cmov TsingleDavid Monniaux2021-02-023-33/+43
| | | |
| * | | implement for another register configurationDavid Monniaux2021-02-021-1/+8
| | | |
| * | | some more cases implementedDavid Monniaux2021-02-021-12/+25
| | | |
| * | | PselectdDavid Monniaux2021-02-023-0/+33
| | | |
| * | | cmov on integersDavid Monniaux2021-02-022-11/+88
| | | |
| * | | begin synthesizing selectDavid Monniaux2021-02-023-2/+34
| | | |
| * | | asmgen OselectlDavid Monniaux2021-02-022-0/+11
| | | |
| * | | begin implementing selectDavid Monniaux2021-02-027-6/+113
| | | |
| * | | select01_longDavid Monniaux2021-02-011-130/+10
| | | |
| * | | repr etc.David Monniaux2021-02-011-4/+2
| | | |
| * | | bitwise_select_value_correctDavid Monniaux2021-02-011-0/+12
| | | |
| * | | int64_of_value some moreDavid Monniaux2021-02-011-14/+15
| | | |
| * | | int64_of_valueDavid Monniaux2021-02-011-0/+77
| | | |
| * | | Asmgen for bits / floatDavid Monniaux2021-02-011-0/+13
| | | |
| * | | bits to floatDavid Monniaux2021-02-019-5/+82
| | | |
| * | | adding builtinsDavid Monniaux2021-02-014-6/+27
| | | |
| * | | Obits_of_single etcDavid Monniaux2021-02-013-3/+46
| | | |
| * | | define some semantics in AsmDavid Monniaux2021-02-012-3/+24
| | | |
| * | | select_longDavid Monniaux2021-01-301-0/+38
| | | |
generated by cgit (git 2.34.1) at 2024-05-20 01:52:56 +0000