aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Collapse)AuthorAgeFilesLines
* 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
| | | | |
| * | | | so that all architectures compileDavid Monniaux2020-10-021-0/+1
| | |/ / | |/| |
* | | | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+10
| | | |
* | | | pointer_eq copiedDavid Monniaux2020-11-251-0/+14
| |/ / |/| |
* | | bug #223 fix on PPCDavid Monniaux2020-11-232-3/+73
|/ /
* | 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-profiling' into mppa-featuresDavid Monniaux2020-04-121-0/+1
|\ \ \
| * | | missing cases preventing compilationDavid Monniaux2020-04-081-0/+1
| |/ /
* | | Merge remote-tracking branch 'origin/mppa-expect3' into mppa-workDavid Monniaux2020-04-091-1/+1
|\ \ \
| * | | adapt the other targets for the new field in CEcondDavid Monniaux2020-04-081-1/+1
| |/ /
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-086-132/+203
|\| |
| * | DuplicateOpcodeHeuristic ppcDavid Monniaux2020-03-171-3/+27
| | |
| * | fix for ppcDavid Monniaux2020-03-031-14/+22
| | |
| * | ported for ppcDavid Monniaux2020-03-031-22/+17
| | |
| * | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-035-3/+173
| |\ \ | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| | * | CSE2 for powerpcDavid Monniaux2020-03-032-0/+152
| | |/
| | * Documentation comment for single_passed_as_singleXavier Leroy2020-03-021-1/+2
| | |
| | * In strict PPC ABI mode, pass single FP on stack in double FP formatXavier Leroy2020-03-021-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The EABI and the SVR4 ABI state that single-precision FP arguments passed on stack are passed as a 64-bit word, extended to double-precision. This commit implements this behavior by using a stack slot of type Tany64. Not only this ensures that the slot is of size and alignment 8 bytes, but it also ensures that it is accessed by stfd and lfd instructions, using single-extended-to-double format.
| | * Make single arg alignment depend on toolchain.Bernhard Schommer2020-03-023-3/+20
| | | | | | | | | | | | | | | | | | | | | | | | | | | GCC does passes single arguments as singles on the stack but diab and the eabi say single arguments should be passed as double on the stack. This commit changes the alignment of single arguments to 4 for gcc based backends.
| * | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-0311-10/+134
| |\ \ | | |/ | |/| | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-126/+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-17/+21
|\ \ \
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-243-17/+21
| |\| | | | |/ | |/| | | | mppa-work-upstream-merge
| | * 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-213-17/+15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
generated by cgit (git 2.34.1) at 2024-07-04 02:33:16 +0000