aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| | * | 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
| | * | Update the output of clightgen to pick the `$` notation from its new placeXavier Leroy2021-04-231-1/+3
| | | | | | | | | | | | | | | | Follow-up to bb5dab848
| | * | Remove `-version-file` option from option summaryXavier Leroy2021-04-231-1/+0
| | | | | | | | | | | | | | | | | | | | The `-version-file` option was removed in commit 600803cae, but remained in the option summary, as reported in #386.
| | * | Move `$` notation in submodule `ClightNotations` and scope `clight_scope`Xavier Leroy2021-04-231-11/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This avoids a nasty conflict with Ltac2 notations as reported in #392. The old `$` notation in scope `string_scope` was not used yet, AFAIK. The new submodule and the new scope are the right places to add future notations to facilitate working with the output of clightgen. Fixes: #392
| | * | Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-194-36/+16
| | | |
| | * | Bump minimal Coq version to 8.9.0Xavier Leroy2021-04-191-2/+2
| | | | | | | | | | | | | | | | This is required to have List.repeat in the standard library (next commit).
| | * | Elab bitfields: check size of type <=32bit rather than checking rank (#387)Amos Robinson2021-04-194-2/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When desugaring a bitfield, allow any integral type that is 32 bits or smaller. Previously this was checking the rank of the type rather than the size. This rank check caused issues with standard headers that declare `uint32_t` to be an `unsigned long` rather than an `unsigned int`. Here, any bitfields declared as `uint32_t` were failing to compile even though they are still actually 32 bits. Co-authored-by: Amos Robinson <amos@gh.st>
| | * | Refactor cparser/Parse.mlXavier Leroy2021-04-191-31/+29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Use pipeline notation `|>` for legibility and better GC behavior (in bytecode at least). - Introduce auxiliary functions. - Remove useless function parameters. - Fix the timing of the "Emulations" pass (because of an extra parameter, what was timed took zero time).
| | * | Ensure compatibility with future versions of MenhirLibXavier Leroy2021-04-191-6/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After Menhir version 20210310, the `Fail_pr` constructor of the `parse_result` type becomes `Fail_pr_full` with two extra arguments. This PR enables CompCert to handle both versions of the `parse_result` type in MenhirLib.
| | * | Do not depend on projection parameter names (#388)Xia Li-yao2021-03-251-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters. There was one place in CompCert where one of these automatically-generated names was used. This commit avoids using this name.
| * | | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-0177-1940/+4260
| |\ \ \
| | * | | removing some Expansion when loading float/single constantsLéo Gourdin2021-06-011-16/+22
| | | | |
| | * | | Merge branch 'kvx-work' of ↵Léo Gourdin2021-05-311-1/+0
| | |\ \ \ | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
| | | * | | just remove a debug printLéo Gourdin2021-05-291-1/+0
| | | | | |
| | * | | | bugfix A64 peephole (cf Scade/Fighter example)Léo Gourdin2021-05-311-6/+5
| | |/ / /
| | * | | Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-198-48/+1410
| | | | |
| | * | | Merge branch 'riscv-work-fpinit-stillexp' into kvx-workLéo Gourdin2021-05-190-0/+0
| | |\ \ \
| | | * | | xorimmsubmission_OOPSLA2021_RISCVLéo Gourdin2021-04-092-0/+77
| | | | | |
| | | * | | removing useless flag checkLéo Gourdin2021-04-091-3/+1
| | | | | |
| | * | | | debug prints uniformizedLéo Gourdin2021-05-181-69/+66
| | | | | |
| * | | | | Commenting out __builtin_expect from AbsIntCyril SIX2021-06-011-2/+2
| | | | | |
| * | | | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-01167-1119/+1692
| | | | | | | | | | | | | | | | | | | | | | | | cfrontend/C2C.ml
| * | | | | Updating varargs2 results for kvxCyril SIX2021-06-011-0/+1
| | | | | |
| * | | | | Remove /home/yuki/Work/VERIMAG/CompCertCyril SIX2021-06-011-1/+1
| | | | | |
| * | | | | fix aarch64 merge?Léo Gourdin2021-03-297-846/+19
| | | | | |
| * | | | | replacing omega with lia in some fileLéo Gourdin2021-03-2933-267/+296
| | | | | |
| * | | | | fix riscv merge?Léo Gourdin2021-03-295-488/+0
| | | | | |
| * | | | | fix CI arm and armhfSylvain Boulmé2021-03-241-2/+6
| | | | | |
| * | | | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-23201-4415/+9534
| |\ \ \ \ \ | | | |_|/ / | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | * | | | Coq 8.13.1 is supportedXavier Leroy2021-03-091-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | Closes: #389
| | * | | | Fix regression on PowerPC / DiabXavier Leroy2021-02-232-4/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-239-42/+90
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-236-35/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | Silence some new warnings of Coq 8.13Xavier Leroy2021-01-211-1/+17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Either because the code change that would silence the warning is not desirable, or because it would break compatibility with earlier versions of Coq. Explain the silenced warnings as comments in the Makefile.
| | * | | | Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-2130-133/+136
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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`.
| | * | | | Define `fold_ind_aux` and `fold_ind` transparentlyXavier Leroy2021-01-211-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The extraction mechanism wants to extract them (because they are in Type, probably). The current opaque definition causes a warning at extraction-time.
| | * | | | "macosx" is now called "macos"Xavier Leroy2021-01-1816-25/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
| | * | | | macOS: turn #warning offXavier Leroy2021-01-181-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The standard includes print irrelevant warnings using `#warning`. The warnings can be restored by passing `-W#warning` to `ccomp`.
| | * | | | Remove regression/interop1 testXavier Leroy2021-01-184-417/+1
| | | | | | | | | | | | | | | | | | | | | | | | Now subsumed by the tests in abi/
| | * | | | Testing calling conventions and interoperability with another C compilerXavier Leroy2021-01-185-1/+583
| | | | | | | | | | | | | | | | | | | | | | | | Using a combination of fixed and randomly-generated function signatures.
| | * | | | Support re-normalization of function parameters at function entryXavier Leroy2021-01-167-27/+58
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | Change warning for pragmas inside functionsXavier Leroy2021-01-161-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Follow-up to 35e2b11db. Put the warning "pragmas are ignored inside functions" inside the Unnamed category, so that it is displayed by default and cannot be disabled.
| | * | | | 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.
| | * | | | Coq 8.13.0 is supportedXavier Leroy2021-01-141-3/+3
| | | | | | | | | | | | | | | | | | | | | | | | However it produces new warnings that should be investigated later.
| | * | | | RISC-V: fix FP calling conventionsXavier Leroy2021-01-146-122/+176
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | Replace `omega` tactic with `lia`, continuedXavier Leroy2021-01-131-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | Follow-up to aba0e740f
| | * | | | Improve branch tunnelingXavier Leroy2021-01-132-60/+328
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The previous branch tunneling was missing optimization opportunities introduced by the optimization of conditional branches. For example: L1: instr; branch L2 L2: if cond then branch L3 else branch L4 L3: branch L4 L4: ... was transformed into L1: instr; branch L2 L2: branch L4 L3: branch L4 L4: ... missing a tunneling opportunity (branch L2 -> branch L4). This commit improves branch tunneling so that the expected code is produced: L1: instr; branch L4 L2: branch L4 L3: branch L4 L4: ... To this end, additional equalities are introduced in the union-find data structure corresponding to optimizable conditional branches. In rare cases these additional equalities trigger new opportunities for optimizing conditional branches. Hence we iterate the analysis until no optimizable conditional branch remains.
| | * | | | Revised correctness proof for record_gotoXavier Leroy2021-01-131-68/+29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We used to define an instrumented version record_goto' that also builds the measure f, prove it correct, then show equivalence with record_goto. The new proofs make do without the instrumented version. They prove strong existence of the measure, as in `{ f | branch_map_correct (record_goto fn) f}`.
| | * | | | Add new fold_ind induction principle for foldsXavier Leroy2021-01-131-63/+82
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | fold_inv is in Type, hence can prove goals such as `{ x | P x }`. Also, no extensionality property is needed. fold_rec is now derived from fold_inv.
| | * | | | Add lemma list_norepet_revXavier Leroy2021-01-131-0/+8
| | | | | |
generated by cgit (git 2.34.1) at 2024-07-03 03:43:17 +0000