aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| | * | Simplify two scripts in Zbits (#369)Maxime Dénès2020-09-181-2/+2
| | | | | | | | | | | | | | | | | | | | Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity.
| | * | Add new static-assert token for deLexer utility; bug 29273Michael Schmidt2020-08-041-0/+1
| | | |
| | * | Add comments we missed to sync to GitHubChristoph Cullmann2020-07-301-0/+2
| | | |
| | * | Add missing comment for print_version_file_and_exitChristoph Cullmann2020-07-301-0/+1
| | | |
| | * | Remove support for x86-32 under macOSXavier Leroy2020-07-292-45/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 32-bit executables cannot be built since XCode 10.0 (sep 2018). 32-bit executables cannot be executed since MacOS 10.15 (oct 2019). Better remove x86-32 support and fail at configuration time instead of at the end of the build.
| | * | Allow string_literals_list in _Static_assert.Bernhard Schommer2020-07-272-24/+25
| | | | | | | | | | | | | | | | | | | | | | | | Not all pre-processors concatenate string literal lists, however they are allowed in _Static_assert. This is similar to the rules for inline assembly etc.
| | * | Add test for __builtin_sqrt and __builtin_fabsfXavier Leroy2020-07-272-0/+7
| | | |
| | * | Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-277-5/+8
| | | | | | | | | | | | | | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
| | * | Refactor regression testing of built-in functionsXavier Leroy2020-07-2713-110/+447
| | | | | | | | | | | | | | | | | | | | | | | | Share the testing code for built-in functions that are available on all target platforms. Improve testing of __builtin_clz* and __builtin_ctz*
| | * | Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-275-46/+12
| | | | | | | | | | | | | | | | These functions are now available on all targets.
| | * | AArch64 implementation of __builtin_ctz*Xavier Leroy2020-07-273-1/+11
| | | | | | | | | | | | | | | | Using the "rbit" instruction (reverse bits).
| | * | RISC-V implementation of __builtin_clz* and __builtin_ctz*Xavier Leroy2020-07-272-0/+134
| | | | | | | | | | | | | | | | Using binary search loops expanded at point of use.
| | * | Add support for __builtin_fabsfXavier Leroy2020-07-274-0/+13
| | | |
| | * | No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-275-12/+0
| | | | | | | | | | | | | | | | __builtin_fabs has already been expanded in backend/Selection.v .
| | * | More checks for __builtin_va_start (#250)Bernhard Schommer2020-07-211-6/+10
| | | | | | | | | | | | | | | | We check that this builtin function is only called from within a variadic function and has the correct number of arguments.
| | * | cparser/handcrafted.messages: missing blank lineXavier Leroy2020-07-211-0/+1
| | | |
| | * | Updated handcrafted.messages.Bernhard Schommer2020-07-211-0/+108
| | | | | | | | | | | | | | | | | | | | Added error descriptions for the new syntax errors introduced by '_Static_assert'.
| | * | Support _Static_assert from C11Xavier Leroy2020-07-217-1060/+1116
| | | |
| | * | Support __builtin_constant_p as in GCC and Clang (#367)Xavier Leroy2020-07-211-0/+10
| | | | | | | | | | | | | | | | | | | | Returns 1 if the argument is a constant expression, 0 otherwise. Closes: #366
| | * | Use the correct location for Slabaled in transform.Bernhard Schommer2020-07-211-2/+2
| | | |
| | * | Added error for redefined builtin.Bernhard Schommer2020-07-203-0/+6
| | | | | | | | | | | | | | | | | | | | | | | | We check in the initial environment if a function is already defined to avoid redefinition of functions that are part of the builtin environment.
| | * | Added missing semicolon.Bernhard Schommer2020-07-151-1/+1
| | | |
| | * | Bytecode-only build, continuedXavier Leroy2020-07-151-0/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | If ocamlopt is not available, use ocamlc instead of ocamlopt to build auxiliary tools (tools/modorder, tools/ndfun). This is a follow-up to commit 9af28924.
| | * | Revised detection of menhirLib directory, continued (#365)Xavier Leroy2020-07-151-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a follow-up to commit 3b1f3dd5, which was wrong in that errors in a shell pipeline were not correctly detected. Fixes: #363
| | * | No trailing commas for --version-file option.Bernhard Schommer2020-07-091-1/+1
| | | |
| | * | Fix typo.Bernhard Schommer2020-07-081-1/+1
| | | |
| | * | Revert "Use the same version string."Bernhard Schommer2020-07-081-3/+10
| | | | | | | | | | | | | | | | This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790.
| | * | Use the same version string.Bernhard Schommer2020-07-081-10/+3
| | | | | | | | | | | | | | | | | | | | | | | | The version string dumped in the file should be the same as the version string printed by `-version`. The option is also not printed by `-help` since it is for internal use only.
| | * | Remove no longer needed option enforce-buildnrBernhard Schommer2020-07-081-10/+1
| | | |
| | * | Introduce additional "branch" build information.Bernhard Schommer2020-07-087-13/+20
| | | |
| | * | Add option to print version information in fileBernhard Schommer2020-07-081-1/+17
| | | |
| | * | Bytecode-only build (#243)Xavier Leroy2020-07-072-4/+29
| | | | | | | | | | | | | | | | | | | | | | | | If ocamlopt (the native-code OCaml compiler) is not available, fall back to building with ocamlc (the bytecode OCaml compiler). Fixes: #359
| | * | Revised detection of menhirLib directory (#248)Xavier Leroy2020-07-071-2/+6
| | | | | | | | | | | | | | | | | | | | Use `ocamlfind query menhirLib` in preference to `menhir --suggest-menhirLib`. Fixes: #363
| | * | 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
| | | |
| | * | Added missing hint database name.Bernhard Schommer2020-06-301-1/+1
| | | |
| | * | Move shared code in new file.Bernhard Schommer2020-06-2817-96/+46
| | | | | | | | | | | | | | | | | | | | 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-2810-19/+1
| | | | | | | | | | | | | | | | | | | | The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
| | * | Use library function.Bernhard Schommer2020-06-281-4/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The function String.uppercase was deprecated and the replacement function String.upercase_ascii was only available from OCaml 4.03.0. Since the minimal OCaml version is now 4.05.0 we can use the function String.upercase_ascii.
| | * | Use Hashtbl.find_opt.Bernhard Schommer2020-06-288-9/+8
| | | | | | | | | | | | | | | | | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
| | * | Eliminate known builtins whose result is ignoredXavier Leroy2020-06-252-40/+54
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A typical example is `(void) __builtin_sel(a, b, c)`. It is safe to generate zero code for these uses of builtins because builtins whose semantics are known to the compiler are pure. Other builtins with side effects (e.g. `__builtin_trap`) are not known and will remain in the compiled code. It is useful to generate zero code for these uses of builtins because some of them (e.g. `__builtin_sel`) must be transformed into proper CminorSel expressions during instruction selection. Otherwise, they propagate all the way to ExpandAsm, causing a "not implemented" error there.
| | * | Improve printing of builtin function invocationsXavier Leroy2020-06-251-0/+3
| | | | | | | | | | | | | | | | In particular __builtin_sel.
| | * | Preliminary support for Coq 8.12Xavier Leroy2020-06-212-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Based on testing with beta-1 release. The deprecation warning about the "omega" tactic is ignored while we decide when to switch to "lia" instead.
| | * | Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-213-3/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | As detected by the new warning in Coq 8.12. The use of Fixpoint here is not warranted and either an oversight or a leftover from an earlier version.
| | * | 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.
| | * | Compatibility with coq 8.11.2Bernhard Schommer2020-06-081-1/+1
| | | | | | | | | | | | | | | | Updated configure script to also allow coq version 8.11.2
| | * | Improve portability of the test for annotations inclightgenXavier Leroy2020-06-052-0/+4
| | | | | | | | | | | | | | | | __builtin_ais_annot is not supported for macOS nor for Cygwin.
| | * | clightgen: fix the printing of annotationsXavier Leroy2020-06-052-59/+14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The printing of EF_annot and EF_annot_val was missing the extra "kind" parameter introduced in commit 6a010b4. Also: the automatic translation of annotations into Coq assertions was confusing and prevented other uses of __builtin_annot statements in conjunction with clightgen. I believe it was never used. This commit removes this translation. Closes: #360
| | * | clightgen: fix usage messageXavier Leroy2020-06-011-2/+2
| | | | | | | | | | | | | | | | Closes: #358
generated by cgit (git 2.34.1) at 2024-07-12 05:28:18 +0000