Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

  1. 19 May, 2021 1 commit
  2. 13 May, 2021 1 commit
  3. 09 Apr, 2021 2 commits
  4. 06 Apr, 2021 1 commit
  5. 30 Mar, 2021 2 commits
  6. 02 Mar, 2021 2 commits
  7. 11 Feb, 2021 1 commit
  8. 10 Feb, 2021 1 commit
  9. 06 Feb, 2021 1 commit
  10. 03 Feb, 2021 2 commits
  11. 02 Feb, 2021 2 commits
  12. 29 Dec, 2020 1 commit
    • Xavier Leroy's avatar
      Replace `omega` tactic with `lia` · aba0e740
      Xavier Leroy authored
      Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal.
      
      Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`,
      and `xomegaContradiction` with `lia` and `extlia`.
      
      Turn back on the deprecation warning for uses of `omega`.
      
      Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
      aba0e740
  13. 14 Jan, 2020 2 commits
  14. 07 Sep, 2019 1 commit
  15. 01 Jun, 2018 1 commit
    • Xavier Leroy's avatar
      Model external calls as destroying all caller-save registers · c58b4215
      Xavier Leroy authored
      The semantics of external function calls in LTL, Linear, Mach and Asm
      now consider that all caller-save registers are set to Vundef by the call.
      This models that fact that the external function can modify those registers
      arbitrarily.
      
      Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
      accordingly.
      c58b4215
  16. 22 Sep, 2017 2 commits
    • Bernhard Schommer's avatar
      Remove coq warnings (#28) · 8d5c6bb8
      Bernhard Schommer authored
      Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
      8d5c6bb8
    • Bernhard Schommer's avatar
      Remove coq warnings (#28) · a36b3b75
      Bernhard Schommer authored
      Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
      a36b3b75
  17. 28 Apr, 2017 3 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
      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
  18. 13 Feb, 2017 1 commit
  19. 01 Oct, 2016 1 commit
  20. 17 May, 2016 1 commit
    • Xavier Leroy's avatar
      Introduce register pairs to describe calling conventions more precisely · 82f9d1f9
      Xavier Leroy authored
      This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations.
      
      In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves.  We will need to change this in the future to support 64-bit processors.  The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting.  Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves.
      
      Summary of changes:
      - AST: introduce the type "rpair A" of register pairs
      - Conventions1, Conventions: use it when describing calling conventions
      - LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls
      - Events: suppress external_call', no longer useful
      - All passes from Allocation to Asmgen: adapt accordingly.
      82f9d1f9
  21. 15 Mar, 2016 1 commit
  22. 11 Mar, 2016 1 commit
  23. 06 Mar, 2016 1 commit
  24. 20 Oct, 2015 1 commit
  25. 14 Oct, 2015 1 commit
  26. 21 Aug, 2015 1 commit
  27. 27 Mar, 2015 1 commit
  28. 24 Nov, 2014 1 commit
  29. 18 Aug, 2014 1 commit
  30. 28 Jul, 2014 1 commit
  31. 23 Jul, 2014 1 commit
    • xleroy's avatar
      Merge of "newspilling" branch: · 2a0168fe
      xleroy authored
      - Support single-precision floats as first-class values
      - Introduce chunks Many32, Many64 and types Tany32, Tany64 to
        support saving and restoring registers without knowing
        the exact types (int/single/float) of their contents, just
        their sizes.
      - Memory model: generalize the opaque encoding of pointers to
        apply to any value, not just pointers, if chunks Many32/Many64
        are selected.
      - More properties of FP arithmetic proved.
      
      
      git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
      2a0168fe