1. 28 Apr, 2017 5 commits
    • 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
    • Xavier Leroy's avatar
    • Bernhard Schommer's avatar
      befe8643
    • Xavier Leroy's avatar
      Modest optimization of leaf functions (continued) · 53c1757e
      Xavier Leroy authored
      - Avoid reloading LR before a tail call if we're in a leaf function
      - Factor out the code that reloads LR if necessary (function Asmgen.transl_epilogue)
      - Factor out the corresponding parts of the proof (Asmgenproof1.transl_epilogue_correct, Asmgenproof.step_simulation)
      53c1757e
    • Xavier Leroy's avatar
      Modest optimization of leaf functions · 2b3e1f02
      Xavier Leroy authored
      Leaf functions are functions that do not call any other function.  For leaf functions, it is not necessary to save the LR register on function entry nor to reload LR on function return, since LR contains the correct return address throughout the function's execution.
      
      This commit suppresses the reloading of LR before returning from a leaf function.  LR is still saved on the stack on function entry, because doing otherwise would require extensive changes in the Stacking pass of CompCert.  However, preliminary experiments indicate that we get good speedups by avoiding to reload LR, while avoiding to save LR makes little difference in speed.
      
      To support this optimization and its proof:
      - Mach is extended with a `is_leaf_function` Boolean function and a `wf_state` predicate to provide the semantic characterization.
      - Asmgenproof* is extended with a `important_preg` Boolean function that means "data register or LR".  A number of lemmas that used to show preservation of data registers now show preservation of LR as well.
      2b3e1f02
  2. 10 Apr, 2017 2 commits
  3. 07 Apr, 2017 3 commits
  4. 06 Apr, 2017 2 commits
    • Xavier Leroy's avatar
      Another optimization of empty if/else and other useless conditional branches · e5b37a6d
      Xavier Leroy authored
      This commit eliminates useless conditional branches during the branch tunneling pass over LTL.  Conditional branches where both successors go to the same LTL node are turned into unconditional branches, which will stay or be eliminated by the subsequent Linear pass.
      
      One code pattern that triggers this optimization is an empty if/else at the C source level.  Commit 4d7a459 eliminates these empty if/else statements early, during the Compcert C -> Clight translation.  I think it's good to have both optimizations:
      - Early elimination makes sure these empty if/else cause no overhead whatsoever, and in particular cannot degrade the precision of later static analyses.
      - Late elimination catches the case where a nonempty if/else in the source becomes empty as a consequence of optimizations.
      
      Future work?  If the optimization in Tunneling triggers, it might be worth re-running the Tunneling pass once more, to make sure that the "Lgoto" introduced by the optimization is properly tunneled / skipped over when appropriate.
      e5b37a6d
    • Michael Schmidt's avatar
      6ce07727
  5. 03 Apr, 2017 1 commit
  6. 24 Mar, 2017 4 commits
  7. 23 Mar, 2017 1 commit
  8. 20 Mar, 2017 2 commits
  9. 08 Mar, 2017 3 commits
  10. 23 Feb, 2017 1 commit
  11. 21 Feb, 2017 2 commits
  12. 19 Feb, 2017 1 commit
  13. 17 Feb, 2017 12 commits
  14. 16 Feb, 2017 1 commit
    • Bernhard Schommer's avatar
      Added handling for noreturn std functions. · 20c7b4d2
      Bernhard Schommer authored
      The C11 standard declares exit,abort,_Exit,quick_exit and
      thrd_exit as _Noreturn however this is not included in older C
      libs and leads to false negatives in reporting _Noreturn and
      return type warnings. This can be avoided by enhancing the
      noreturn check of the Cflow analysis to also test if one of the
      above functions is called.
      Bug 21009
      20c7b4d2