Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CompCert version 3.15 #3279

Merged
merged 1 commit into from
Jan 3, 2025
Merged

CompCert version 3.15 #3279

merged 1 commit into from
Jan 3, 2025

Conversation

xavierleroy
Copy link
Contributor

C language support

  • Minimal syntactic support for _Float16 type (half-precision FP numbers). Function declarations using _Float16 are correctly parsed, but any actual use of _Float16 is rejected later during compilation. (525)
  • Support C99 array declarator syntax involving static and *. These annotations are correctly parsed, but ignored during typing and compilation. (539)

Code generation and optimization

  • Better support for _Bool type in the back-end and in the memory model.
  • This avoids redundant normalizations to _Bool.
  • Take types of function parameters into account during value analysis.
  • This avoids redundant normalizations on parameters of small integer types.
  • More conservative static analysis of pointer comparisons. (516)
  • Refined heuristic for if-conversion. Turn if-conversion off in some cases where it would prevent later optimization of conditional branches in the continuation of the if.
  • CSE: remember pointer alias information in Load equations, making it possible to remove more redundant memory loads. (518)
  • More precise value analysis of integer multiplication, division, modulus.
  • Constant propagation: optimize "known integer or undefined" results. For example, &x == &x, which is either 1 or undefined, is now replaced by 1.
  • Optimize (x ^ cst) != 0 into x != cst.
  • Avoid quadratic compile-time behavior on deeply-nested if statements. (519)

Bug fixes

  • More robust determination of symbols that may be defined in a shared object. (538)
  • Escape $NNN identifiers in generated x86 and ARM assembly code (541).
  • Wrong parameter scoping in function definitions such as int (*f(int y))(int x) { ... } (a function returning a pointer to a prototyped function).

Usability

  • Mark stack as non-executable in binaries produced by ccomp.
  • Check that preprocessed sources (.i files) do not contain backslash-newline sequences.
  • ./configure arm-linux now selects the hard-FP ABI, since Linux distributions no longer use the soft-FP ABI.

Supporting libraries

  • ARM library for 64-bit integer arithmetic: faster division, cleaned-up code.

Coq development

  • Support Coq 8.20.
  • Build: support TIMING and PROFILING like coq_makefile. (512)
  • Make dependency on Extraction explicit. (515)
  • Install .glob and .v files along .vo files. (527)

@palmskog palmskog merged commit 895ece1 into coq:master Jan 3, 2025
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants