1. 06 Dec, 2020 1 commit
    • Xavier Leroy's avatar
      Error when using -main without -interp · b40aef6c
      Xavier Leroy authored
      Outside of -interp mode, -main has no (known) effect but could be
      confused for a linker option that sets the program's entrypoint, say.
      It's safer to reject the option.
      b40aef6c
  2. 30 Oct, 2020 1 commit
    • Xavier Leroy's avatar
      Add -main option to specify entrypoint function in interpreter mode (#374) · b1b853a2
      Xavier Leroy authored
      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.
      b1b853a2
  3. 08 Jul, 2020 1 commit
  4. 09 Jul, 2019 1 commit
  5. 05 Jul, 2019 2 commits
  6. 06 Jun, 2019 1 commit
    • Xavier Leroy's avatar
      If-conversion optimization · 8e3a7344
      Xavier Leroy authored
      Extends the instruction selection pass with an if-conversion optimization:
      some if/then/else statements are converted into "select" operations,
      which in turn can be compiled down to branchless instruction sequences
      if the target architecture supports them.
      
      The statements that are converted are of the form
      
              if (cond) { x = a1; } else { x = a2; }
              if (cond) { x = a1; }
              if (cond) { /*skip*/; } else { x = a2; }
      
      where a1, a2 are "safe" expressions, containing no operations that can
      fail at run-time, such as memory loads or integer divisions.
      
      A heuristic in backend/Selectionaux.ml controls when the optimization occurs,
      depending on command-line flags and the complexity of the "then" and "else"
      branches.
      8e3a7344
  7. 10 May, 2019 2 commits
    • Bernhard Schommer's avatar
      Added options -fcommon and -fno-common (#164) · 1eaf745c
      Bernhard Schommer authored
      The option -fcommon controls whether uninitialized global
      variables are placed in the COMMON section. If the option is given
      in the negated form, -fno-common, variables are not placed in the
      COMMON section. They are placed in the same sections as gcc does.
      
      If the variables are not placed in the COMMON section merging of
      tentative definitions is inhibited and multiple definitions lead
      to a linker error, as it does for gcc.
      1eaf745c
    • Bernhard Schommer's avatar
      Check for alignment of command-line switches. · 47c86d46
      Bernhard Schommer authored
      Add a check for alignment on command-line switches `-falign-*`.
      The check is similar to the one for the alignment attribute and
      ensures that only powers of two can be specified.
      47c86d46
  8. 02 Aug, 2018 1 commit
  9. 09 Feb, 2018 1 commit
  10. 08 Feb, 2018 1 commit
    • 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.
      f02f00a0
  11. 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.
      5920d4c5
  12. 11 Jan, 2018 1 commit
  13. 05 Jan, 2018 2 commits
  14. 04 Jan, 2018 2 commits
  15. 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.
      ca9219d4
  16. 13 Dec, 2017 1 commit
  17. 07 Dec, 2017 1 commit
  18. 27 Nov, 2017 2 commits
    • Xavier Leroy's avatar
      Remove temporary .o files after linking (#36) · a674c56d
      Xavier Leroy authored
      When -c is not given, .o files are now generated in /tmp, but they are still not erased.
      
      This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits.
      
      Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
      a674c56d
    • Xavier Leroy's avatar
      Remove temporary .o files after linking (#36) · 5d4cba91
      Xavier Leroy authored
      When -c is not given, .o files are now generated in /tmp, but they are still not erased.
      
      This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits.
      
      Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
      5d4cba91
  19. 16 Oct, 2017 1 commit
  20. 25 Sep, 2017 1 commit
  21. 18 Sep, 2017 1 commit
    • Gergö Barany's avatar
      Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203) · c4dcf7c0
      Gergö Barany authored
      * Clarify that ARMv6 is in fact ARMv6T2
      
      The ARMv6 comes in two flavors depending on the version of the Thumb
      instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2.
      CompCert only supports Thumb2, so its ARMv6 architecture should really be
      called ARMv6T2. This makes a difference: the GNU assembler rejects most of
      the instructions CompCert generates for ARMv6 with "-mthumb" if the
      architecture is specified as ".arch armv6" as opposed to ".arch armv6t2".
      
      This patch fixes the architecture specification in the target printer and
      the internal name of the architecture. It does not change the configure
      script's flags to avoid breaking changes.
      
      * Always use ARM movw/movt to load large immediates
      
      These move-immediate instructions used to be only emitted in Thumb mode, not
      in ARM mode. As far as I understand ARM's documentation, these instructions
      are available in *both* modes in ARMv6T2 and above. This should cover all of
      CompCert's ARM targets.
      
      Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is
      now identical to Clang, and the GNU assembler accepts these instructions in
      all configurations.
      
      * Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6
      
      - define separate architecture models for ARMv6 and ARMv6T2
      - introduce `Archi.move_imm` parameter on ARM to identify models with
        `movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM
        and Thumb mode)
      
      * Fixes for support for architectures with Thumb2
      
      - rename relevant parameter to `Archi.thumb2_support`
      - on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb)
      - allow generation of `sbfx` in ARM mode if Thumb2 is supported
      c4dcf7c0
  22. 24 Aug, 2017 1 commit
  23. 28 Jun, 2017 1 commit
    • Bernhard Schommer's avatar
      Formatted json printing. · 6bece636
      Bernhard Schommer authored
      Instead of just dumping the json output it is now a little bit
      formatted for better reading.
      
      Furthermore the AsmToJson function for the non powerpc targets now
      prints the json value "null" sucht that the resulting json file is
      valid json.
      6bece636
  24. 26 Jun, 2017 1 commit
  25. 28 Apr, 2017 1 commit
    • Xavier Leroy's avatar
      RISC-V port and assorted changes · f642817f
      Xavier Leroy authored
      This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes.
      
      The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/
      
      This port required the following additional changes:
      
      - Integers: More properties about shrx
      
      - SelectOp: now provides smart constructors for mulhs and mulhu
      
      - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu.
      
      - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert.  Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library.
      
      - test/: add SIMU make variable to run tests through a simulator
      
      - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers
      
      commit da14495c01cf4f66a928c2feff5c53f09bde837f
      Author: Xavier Leroy <xavier.leroy@inria.fr>
      Date:   Thu Apr 13 17:36:10 2017 +0200
      
          RISC-V port, continued
      
          Now working on Asmgen.
      
      commit 36f36eb3a5abfbb8805960443d087b6a83e86005
      Author: Xavier Leroy <xavier.leroy@inria.fr>
      Date:   Wed Apr 12 17:26:39 2017 +0200
      
          RISC-V port, first steps
      
          This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64).  Work in progress.
      f642817f
  26. 07 Apr, 2017 1 commit
  27. 08 Mar, 2017 1 commit
  28. 14 Feb, 2017 3 commits
  29. 03 Feb, 2017 1 commit
    • Xavier Leroy's avatar
      Refactor the classification of attributes · 3babd253
      Xavier Leroy authored
      Introduce Cutil.class_of_attribute to return the class of the given attribute: one among
      Attr_type  attribute related to types  (e.g. "aligned")
      Attr_struct attribute related to struct/union/enum types (e.g. "packed")
      Attr_function attribute related to function types (e.g. "noreturn")
      Attr_name  attribute related to variable and function declarations (e.g. "section")
      Attr_unknown  attribute was not declared
      
      Cutil.declare_attribute is used to associate a class to a custom attribute.
      Standard attributes (const, volatile, _Alignas, etc) are Attr_type.
      
      cfronted/C2C.ml: declare the few attributes that CompCert honors currently.
      cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only.
      3babd253
  30. 27 Jan, 2017 1 commit
  31. 25 Jan, 2017 1 commit
  32. 18 Jan, 2017 1 commit
  33. 17 Jan, 2017 1 commit
    • Bernhard Schommer's avatar
      Added backtrace handler. · 43db836e
      Bernhard Schommer authored
      If CompCert crashes because of an uncaught exception the exception
      is caught toplevel and the backtrace is printed plus an additional
      message to include the backtrace in a support request, if buildnr
      and tag are available.
      Bug 20681.
      43db836e