1. 16 Feb, 2018 3 commits
    • Bernhard Schommer's avatar
      Rename abi for ppc-linux targets. · 455b3384
      Bernhard Schommer authored
    • Michael Schmidt's avatar
      Fix typo in comment · 95395781
      Michael Schmidt authored
    • Xavier Leroy's avatar
      Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59) · 16608ca8
      Xavier Leroy authored
      When x is known to be either 0 or 1, comparisons such as
      x == 0   x != 0    x == 1    x != 1
      can be optimized away.  This optimization was already performed
      for signed comparisons.  This commit extends the optimization to
      unsigned comparisons as well.
      Additionally, for PowerPC only, some unsigned (dis)equality comparisons are
      turned into signed comparisons when we know it makes no difference,
      i.e. when both arguments are guaranteed not to be pointers.  The
      reason is that Asmgen can produce shorter instruction sequences for
      some signed equality comparisons than for the corresponding unsigned
      It's important to optimize unsigned integer comparisons because casts
      to the C99 type _Bool are compiled as x !=u 0 unsigned comparisons.
      In particular, cascades of casts to _Bool are now reduced to a single
      cast much more often than before.
  2. 12 Feb, 2018 2 commits
    • Bernhard Schommer's avatar
    • Xavier Leroy's avatar
      In "symbol + ofs" addressing modes, limit the range of "ofs" in 64 bits · 26a4436b
      Xavier Leroy authored
      In 32-bit mode, a symbolic reference "symbol + ofs" (address of "symbol" plus "ofs" bytes) can always be resolved by the linker into a 32-bit quantity that fits the 32-bit displacement field of x86 addressing modes.
      Not so in 64-bit mode: first, the displacement field is still 32 bits but the full address is 64 bits; second, the displacement is relative to the RIP instruction pointer.  In the "small code model" that CompCert uses for x86-64, excessively large offsets lead to link-time overflows of this 32-bit displacement field.
      This commit addresses the issue by limiting the "ofs" part of "symbol + ofs" global addressing models to the range [-2^24, 2^24 - 1].  As explained in the AMD64 ELF ABI document, this is a safe range in the small code model, under the assumption that no global symbol is bigger than 2^24 bytes.  GCC seems to be using a wider range [-2^31, 2^24 - 1] but I'd rather be safe.
      The limitation of the "ofs" offset is achieved by extending the mechanisms already present to ensure that "ofs" in "reg + ofs" indexed addressing modes fits in 32-bit signed:
      - Op.addressing_valid checks that the "ofs" part of "symbol + ofs" addressing modes is in the correct interval;
      - SelectOp.addressing turns invalid addressings into lea's + indexed addressings;
      - Asmgen.normalize_addrmode_64 turns lea's with invalid addressings into simpler lea's + addq of the large offset.
  3. 09 Feb, 2018 2 commits
  4. 08 Feb, 2018 5 commits
    • Michael Schmidt's avatar
      Configure check for PIE (#55) · d8da5069
      Michael Schmidt authored
      When checking for -no-pie and -nopie, evaluate gcc output for error message like 'unknown argument'.  (Relying on the error code is not enough.)
    • Xavier Leroy's avatar
      x86 ConstpropOp.addr_strength_reduction: always check validity of resulting addressing · 14aad5e8
      Xavier Leroy authored
      In the original code, the addressing_valid check is skipped if we are in 32 bits, because we know the check is always true.  This is correct but not obvious nor future-proof.  (In the future we may want to make addressing_valid more strict.)
      This commit restructures ConstpropOp.addr_strength_reduction so that the addressing_valid check is always performed.
    • Xavier Leroy's avatar
      Truncation of array sizes when converting them to Coq's Z type · de0ff0bc
      Xavier Leroy authored
      The size (number of elements) of an array type is represented as an OCaml int64 in the parse tree, and as a Coq Z in the CompCert C AST.  However, the C2C.convertInt function used to do this conversion produces a Coq int (32 bits) type, taking the array size modulo 2^32.  This is not correct, esp. on a 64-bit target.
      This commit refactors C2C around three integer conversion functions:
      convertInt32  producing a Coq "int" (32 bit)
      convertInt64  producing a Coq "int64" (64 bit)
      convertIntZ  producing a Coq "Z" (arbitrary precision)
    • Bernhard Schommer's avatar
      Extend the modorder tool to handle Coq files as well (#54) · f80498e1
      Bernhard Schommer authored
      This is useful to e.g. identify the .vo files from CompCert that a clightgen-generated .v file needs.
      Also: the "result" field of the record type is now initialized with the LHS of the dependency, not the RHS.  It doesn't matter because the result field is unused, but it makes more sense now.
    • Bernhard Schommer's avatar
      Refactor the handling of errors and warnings (#44) · f02f00a0
      Bernhard Schommer authored
      * Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/
      * Replaced eprintf error.  Instead of having eprintf msg; exit 2 use the functions from the
      Diagnostics module.
      * Raise on error before calling external tools.
      * Added diagnostics to clightgen.
      * Fix error handling of AsmToJson.
      * Cleanup error handling of Elab and C2C.
      *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
  5. 06 Feb, 2018 1 commit
  6. 29 Jan, 2018 1 commit
    • Bernhard Schommer's avatar
      Share code for common options. · 5920d4c5
      Bernhard Schommer authored
      In order to avoid more divergence between the command line options of
      clightgen and ccomp the code for the common options, the language support
      options, the version string and the general options.
  7. 17 Jan, 2018 3 commits
  8. 15 Jan, 2018 2 commits
  9. 13 Jan, 2018 5 commits
  10. 11 Jan, 2018 4 commits
  11. 10 Jan, 2018 3 commits
  12. 09 Jan, 2018 1 commit
  13. 08 Jan, 2018 2 commits
  14. 05 Jan, 2018 3 commits
    • Bernhard Schommer's avatar
    • Bernhard Schommer's avatar
      Added toolchain specific option for dcc. (#47) · 91601d4b
      Bernhard Schommer authored
      CompCert now accepts the target configuration option of the diab
      data compiler and passes it on to the preprocessor, assembler and
      Bug 20521
    • Xavier Leroy's avatar
      Resynchronize the LICENSE file and the license headers in individual files (#45) · 9ccb6a24
      Xavier Leroy authored
      Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file.  OVer the years those two markings got inconsistent.
      This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed.
      Some build-related files were dual-licensed but some others were not.  Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v
      Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed.  Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST
      which is not in lib/
  15. 04 Jan, 2018 2 commits
  16. 03 Jan, 2018 1 commit
    • Bernhard Schommer's avatar
      Remove all temporary files at program exit (#46) · ca9219d4
      Bernhard Schommer authored
      Replaced calls to Filename.temp_file by own version Driveraux.tmp_file.
      The Driveraux.tmp_file function takes care that the temporary files are
      removed at exit.
      Consequently there is no need to explicitly remove temp files in Driver.