aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-186-162/+214
|\
| * Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-301-1/+1
| | | | | | | | | | | | | | When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function. This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option. The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.
| * Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-0/+2
| | | | | | | | __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-0/+12
| | | | | | | | These functions are now available on all targets.
| * Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+2
| |
| * Move shared code in new file.Bernhard Schommer2020-06-281-1/+1
| | | | | | | | | | 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-281-1/+1
| | | | | | | | | | The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
| * Improve printing of builtin function invocationsXavier Leroy2020-06-251-0/+3
| | | | | | | | In particular __builtin_sel.
| * SimplExpr: remove unused definition "sd_cast_set"Xavier Leroy2020-06-151-2/+0
| | | | | | | | Follow-up to commit 070babef.
| * SimplExpr: better translation of casts in a "for effects" contextXavier Leroy2020-06-153-136/+166
| | | | | | | | | | | | | | | | This is useful for statements such as `(void) expr;` where we would prefer not to explicitly compute intermediate values of type `void` and store them in Clight temporary variables. See issue #361 for a real-world occurrence of this phenomenon.
| * Move reserved_registers to CPragmas.Bernhard Schommer2020-04-201-1/+6
| | | | | | | | | | | | | | The list of reserved_registers is never reset between the compilation of multiple files. Instead of storing them in IRC they are moved in the CPragmas file and reset in the a new reset function for Cpragmas whic is called per file.
* | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-0/+9
|\ \
| * | begin installing profilingDavid Monniaux2020-04-081-1/+1
| | |
| * | added EF_profilingDavid Monniaux2020-04-081-0/+9
| | |
* | | Merge remote-tracking branch 'origin/mppa-expect3' into mppa-workDavid Monniaux2020-04-099-45/+86
|\ \ \
| * | | expect operationDavid Monniaux2020-04-072-27/+35
| | | |
| * | | Oexpect in frontendDavid Monniaux2020-04-076-16/+47
| | | |
| * | | start implementing expect as exprDavid Monniaux2020-04-071-0/+1
| | | |
| * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-expectDavid Monniaux2020-04-0611-124/+328
| |\| |
| * | | __builtin_expect defined as its first argumentDavid Monniaux2019-09-251-2/+3
| | | |
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-082-31/+46
|\ \ \ \ | | |/ / | |/| |
| * | | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-011-2/+2
| |\ \ \ | | | |/ | | |/|
| | * | Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-291-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Introduce an error message for section attributes with non string arguments,and another for multiple, ambiguous section attributes. This is more consistent with the handling of other attributes, like packed, than the old behavior of silently ignoring them.
| * | | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-031-29/+44
| |\| | | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| | * | Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-021-29/+44
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | According to ISO C, `free(NULL)` is correct and does nothing. This commit updates accordingly the formal semantics of the `free` external function and the reference interpreter. Closes: #334
| * | | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-031-4/+36
| |\ \ \ | | |/ / | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
* | | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-259-76/+232
|\ \ \ \
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-248-74/+229
| |\| | | | | | | | | | | | | | | | | | mppa-work-upstream-merge
| | * | | Support re-normalization of values returned by function callsXavier Leroy2020-02-212-33/+137
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-216-39/+78
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | More precise determination of small data accesses (#220)Bernhard Schommer2020-02-201-3/+15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We can get linker errors for addresses of the form "symbol + offset" where "symbol" is in the small data area and "offset" is large enough to overflow the relative displacement from the SDA base register. To avoid this, this commit enriches `C2C.atom_is_small_data`, which is the implementation of `Asm.symbol_is_small_data` in the PPC port, with a check that the offset is within the bounds of the symbol. If it is not, `Asm.symbol_is_small_data` returns `false` and Asmgen produces an absolute addressing instead of a SDA-relative addressing. To implement the check, we record the sizes of symbols in the atom table, just like we already record their alignments.
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-132-2/+3
| |\| | | | | |/ / | |/| | | | | | mppa-work-upstream-merge
| | * | Take the sign into account for int to ptr cast.Bernhard Schommer2020-02-122-2/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Casting from an integer constant to pointer on 64 bit architectures did not take the signedness into account and always interpreted the integer as unsigned which causes some incompatibility with libc implementations.
* | | | thread local declarations now workDavid Monniaux2020-02-241-1/+5
| | | |
* | | | it now works, no more ugly hack to access thread local dataDavid Monniaux2020-02-241-0/+9
| | | |
* | | | seems to process _Thread_local but not till backendDavid Monniaux2020-02-241-7/+14
|/ / /
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-12-091-0/+5
|\| | | | | | | | | | | mppa-work-upstream-merge
| * | Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-281-0/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time. This PR extends the check for a representable offset for the addressing of global variables to also check whether the variable is correctly aligned. Only if both conditions are met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic loadsymbol sequence.
* | | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-202-17/+45
|\| | | |/ |/| | | mppa-work-upstream-merge
| * -dclight output: use nicer names for temporary variablesXavier Leroy2019-09-161-2/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The temporary variables introduced by SimplLocals reuse the same integer identifiers as the local variables they come from. This commit ensures that these variables are printed as "$var", where "var" is the original variable name, instead of "$NNN" as before. The "$NNN" form is retained for temporary variables that do not correspond to a source-level local variable, such as the temporary variables introduced by SimplExpr. This commit should make no difference for "ccomp -dclight", because the Clight that is printed is the Clight version 1 produced by SimplExpr, where every temporary is fresh and does not correspond to a source-level local variable. This commit does change the output of "clightgen -dclight", because the Clight that is printed is the Clight version 2 produced by SimplLocals. The printed Clight is much more legible thanks to the more meaningful temporary variable names.
| * clightgen -dclight: print function parameters correctlyXavier Leroy2019-09-162-15/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | The Clight output of clightgen is Clight version 2, after SimplLocals conversion, where function parameters are temporary variables, not variables. This commit makes sure the function parameters are printed as temporary variables and not as variables. In passing, it generalizes the Clight pretty-printer so that it can print both Clight version 1 and Clight version 2. Closes: #314
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-08-285-14/+17
|\| | | | | | | mppa-work-upstream-merge
| * bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-1/+3
| | | | | | | | | | | | | | | | | | | | | | | | * Added semantic for byte swap builtins The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics. The semantics is given in terms of the decode/encode functions used for the memory model. * Added bswap64 expansion to PowerPC 32 bits. * Added bswap64 expansion for ARM.
| * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-054-13/+14
| | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-196-65/+227
|\| | | | | | | mppa-work-upstream-merge
| * Make __builtin_sel available from C source codeXavier Leroy2019-07-175-31/+157
| | | | | | | | | | It is type-checked like a conditional expression then translated to a call to the known builtin function.
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-9/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Remove the cparser/Builtins moduleXavier Leroy2019-07-171-7/+10
| | | | | | | | | | | | | | | | | | Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
| * Change the expected types for arguments to __builtin_annot, and extended asmXavier Leroy2019-06-191-5/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently, the arguments to __builtin_annot, __builtin_ais_annot, __builtin_debug, and extended asm statements are treated like arguments to an unprototyped or vararg function call. In particular, arguments of type "float" are converted to "double", generating useless code. To avoid this extra, useless conversion, this commit changes the types expected for the arguments to these built-ins and to extended asm statements. Now they are the types of the arguments themselves, after performing the usual unary conversions (e.g. char -> int), but without the problematic float -> double conversion. This ensures that no code is generated to change the representation of the arguments.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-036-10/+9
|\| | | | | | | mppa-if-conversion
generated by cgit (git 2.34.1) at 2024-07-04 02:48:11 +0000