aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-295-22/+33
|\
| * PPC64: revised generation of rldic* instructionsXavier Leroy2021-10-284-20/+31
| | | | | | | | | | | | | | | | | | | | | | | | In Op.v, the definitions of is_rldl_mask and is_rldr_mask mask were swapped: - rldl is for [00001111] masks that clear on the left, hence start with 1s and finish with 0s; - rldr is for [11110000] masks that clear on the right, hence start with 0s and finish with 1s. In Asmgen.v, the case for masks of the form [00011111100] that can generate a rldic instruction was incorrectly detected.
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-2/+2
| | | | | | | | This avoids a new warning of Coq 8.14.
* | Merge remote-tracking branch 'origin/master' into kvx-workDavid Monniaux2021-10-011-1/+1
|\|
| * Typo in expand_builtin_memcpy_smallXavier Leroy2021-10-011-1/+1
| | | | | | | | Follow-up to c34d25e01
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-245-172/+178
|\|
| * Fix wrong expansion of __builtin_memcpy_alignedXavier Leroy2021-09-231-2/+2
| | | | | | | | | | | | | | | | | | In the "small" case, there was an error in the choice of temporary registers to use when one argument is a stack location and the other is a register. The chosen temporary could conflict with the argument that resides in a register. Fixes: #412
| * Fix the type and the semantics of BI_bselXavier Leroy2021-09-221-4/+17
| | | | | | | | The return type is Tint8unsigned (i.e. _Bool), not Tint.
| * Share code for memory access for PowerPCBernhard Schommer2021-09-064-166/+159
| | | | | | | | | | | | Instead of duplicating the memory access code in `Asmexpand.ml` we move the code for each of the different addressings in `Asmgen.v` into separate functions that then can be reused in `Asmexpand.ml`.
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-084-16/+20
| | | | | | | | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
| * Support __builtin_unreachableXavier Leroy2021-05-021-0/+3
| | | | | | | | Not yet used for optimizations.
| * More fixes for ld/std issue.Bernhard Schommer2021-04-241-11/+40
| | | | | | | | | | | | | | Volatile load and store are expanded later and also use the ld/std instructions, therefore the same fixes that are applied as well for them. Bug 30983
| * Tentative first fix for offsets of ld/std.Bernhard Schommer2021-04-245-152/+259
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The offsets immediates used in the ld and std instructions must be a multiple of the word size. This commit changes the two functions which are used when generating load/stores in Asmgen, accessind and transl_memory_access. For accessind one only needs an additional check that the offset is a multiple of the word size for the case that the high part of the offset is zero, since otherwise the immediate is loaded into a register anyway. The transl_memory_access function needs some slightly more complex adoption. For all variants that do not construct the address in a register before hand we must check that the offsets are multiples of the word size and additionally if a symbol is used that the alignment of the symbol is also a multiple of the word size. Therefore a new parameter is introduced that allows checking the alignment. In order to reduce the code duplication for the proofs these two functions get an additional parameter in order to indicate wether the offset needs to be a multiple of the word size or not. Bug 30983
* | cleanupLéo Gourdin2021-09-011-1/+0
| |
* | op simplify BTL introLéo Gourdin2021-07-201-0/+1
| |
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-019-179/+322
| | | | | | | | cfrontend/C2C.ml
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2311-109/+107
|\| | | | | | | | | | | | | | | | | 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
| * Fix regression on PowerPC / DiabXavier Leroy2021-02-231-2/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | On PowerPC/Diab, common declarations must not be used for small data sections. Add a `~common` option to `PrintAsmaux.variable_section` to control the use of common declarations. The default is whatever is specified on the command line using the `-fcommon` and `-fno-common` options. Use `~common:false` for `Section_small_data` on PowerPC / Diab. Note that on PowerPC/Linux, GCC uses common declarations for uninitialized variables in small data section, so we keep doing this in CompCert as well.
| * Section handling: finer control of variable initializationXavier Leroy2021-02-231-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8.
| * Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-14/+8
| | | | | | | | | | | | | | 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-212-8/+8
| | | | | | | | | | | | | | 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.
| * PowerPC: wrong computation of the position of the first vararg argumentXavier Leroy2021-01-151-2/+3
| | | | | | | | | | | | | | | | | | In function Asmexpand.next_arg_locations: If 7 integer parameter passing registers have been used already, and the next fixed arguments are Tlong then Tint, the Tlong argument was correctly analyzed as being passed on the stack, but the Tint argument was incorrectly analyzed as being passed in the 8th register.
| * Replace `omega` tactic with `lia`, continuedXavier Leroy2021-01-131-1/+1
| | | | | | | | Follow-up to aba0e740f
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-299-81/+81
| | | | | | | | | | | | | | | | | | | | | | 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`.
| * Changed cc_varargs to an option typeBernhard Schommer2020-12-251-1/+1
| | | | | | | | | | | | 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.
* | fix ci ?Léo Gourdin2021-03-022-0/+2
| |
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-081-2/+1
|\ \
| * | rm instructions now unusedDavid Monniaux2020-12-081-2/+1
| | |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-0819-148/+90
|\| |
| * | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-0813-103/+29
| |\|
| | * PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | | | | | | | | | | | Inlined built-in functions destroy GPR0
| | * 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.
| * | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-044-3/+88
| |\ \ | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * \ \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-188-45/+61
| |\ \ \ | | | |/ | | |/|
| | * | 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
| | * | 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.
| | * | Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-271-12/+0
| | | | | | | | | | | | | | | | These functions are now available on all targets.
| | * | 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 .
| | * | Added asserts for constraints of PowerPC builtinsBernhard Schommer2020-07-011-0/+6
| | | |
| | * | Fix typo in name of builtin function.Bernhard Schommer2020-07-011-1/+1
| | | |
| | * | 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-5/+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.
* | | | cond_depends_onDavid Monniaux2020-12-021-7/+7
| | | |
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-021-0/+1
|\ \ \ \ | | |_|/ | |/| |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-242-3/+73
| |\ \ \
| * | | | op_valid_pointer_eq ppcDavid Monniaux2020-10-191-0/+14
| | | | |
generated by cgit (git 2.34.1) at 2024-05-09 01:57:06 +0000