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. 09 May, 2021 1 commit
  2. 08 May, 2021 2 commits
  3. 02 May, 2021 4 commits
    • Xavier Leroy's avatar
      Fix evaluation order in emulation of bitfield assignment · 1f35599a
      Xavier Leroy authored
      A bitfield assignment `x.b = f()` is expanded into a read-modify-write
      on `x.carrier`.  Wrong results can occur if `x.carrier` is read before
      the call to `f()`, and `f` itself modifies a bitfield with the same
      carrier `x.carrier`.
      
      In this temporary fix, we play on the evaluation order implemented by
      the SimplExpr pass of CompCert (left-to-right for side-effecting
      subexpression) to make sure the read part of the read-modify-write
      sequence occurs after the evaluation of the right-hand side.
      
      More substantial fixes will be considered later.
      
      Fixes: #395
      1f35599a
    • Xavier Leroy's avatar
      Support __builtin_expect · 3b448f59
      Xavier Leroy authored
      Not yet used for optimizations.
      
      Actually, __builtin_expect is removed during C2C conversion, otherwise
      the conversion to type "long" produces inefficient code on 64-bit platforms.
      3b448f59
    • Xavier Leroy's avatar
      Support __builtin_unreachable · 320c5559
      Xavier Leroy authored
      Not yet used for optimizations.
      320c5559
    • Xavier Leroy's avatar
      Fix spurious error on initialization of struct with flexible array member · 38b0babd
      Xavier Leroy authored
      
      
      The following is correct but was causing a "wrong type for array initializer"
      fatal error.
      
      ```
      struct s { int n; int d[]; };
      void f(void) { struct s x = {0}; }
      ```
      Co-authored-by: default avatarMichael Schmidt <github@mschmidt.me>
      38b0babd
  4. 29 Apr, 2021 2 commits
  5. 27 Apr, 2021 2 commits
  6. 24 Apr, 2021 2 commits
    • Bernhard Schommer's avatar
      More fixes for ld/std issue. · ff88fc9f
      Bernhard Schommer authored
      Volatile load and store are expanded later and also use the ld/std
      instructions, therefore the same fixes that are applied as well for
      them.
      Bug 30983
      ff88fc9f
    • Bernhard Schommer's avatar
      Tentative first fix for offsets of ld/std. · 69e17574
      Bernhard Schommer authored
      The offsets immediates used in the ld and std instructions must be a
      multiple of the word size. This commit changes the two functions which
      are used when generating load/stores in Asmgen, accessind and
      transl_memory_access.
      
      For accessind one only needs an additional check that the offset is a
      multiple of the word size for the case that the high part of the offset
      is zero, since otherwise the immediate is loaded into a register anyway.
      
      The transl_memory_access function needs some slightly more complex
      adoption. For all variants that do not construct the address in a
      register before hand we must check that the offsets are multiples of the
      word size and additionally if a symbol is used that the alignment of the
      symbol is also a multiple of the word size. Therefore a new parameter is
      introduced that allows checking the alignment.
      
      In order to reduce the code duplication for the proofs these two
      functions get an additional parameter in order to indicate wether the
      offset needs to be a multiple of the word size or not.
      Bug 30983
      69e17574
  7. 23 Apr, 2021 3 commits
  8. 19 Apr, 2021 5 commits
  9. 25 Mar, 2021 1 commit
    • Xia Li-yao's avatar
      Do not depend on projection parameter names (#388) · 6106e043
      Xia Li-yao authored
      coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters.
      There was one place in CompCert where one of these automatically-generated names was used.
      This commit avoids using this name.
      6106e043
  10. 09 Mar, 2021 1 commit
  11. 23 Feb, 2021 3 commits
    • Xavier Leroy's avatar
      Fix regression on PowerPC / Diab · 014883f2
      Xavier Leroy authored
      On PowerPC/Diab, common declarations must not be used for small data sections.
      
      Add a `~common` option to `PrintAsmaux.variable_section` to control
      the use of common declarations.  The default is whatever is specified
      on the command line using the `-fcommon` and `-fno-common` options.
      
      Use `~common:false` for `Section_small_data` on PowerPC / Diab.
      
      Note that on PowerPC/Linux, GCC uses common declarations for uninitialized
      variables in small data section, so we keep doing this in CompCert as well.
      014883f2
    • Xavier Leroy's avatar
      Section handling: finer control of variable initialization · ed89275c
      Xavier Leroy authored
      Distinguish between:
      - uninitialized variables, which can go in COMM if supported
      - variables initialized with fixed, numeric quantities,
        which can go in a readonly section if "const"
      - variables initialized with symbol addresses which may need relocation,
        which cannot go in a readonly section even if "const",
        but can go in a special "const_data" section.
      
      Also: on macOS, use ".const" instead of ".literal8" for literals,
      as not all literals have size 8.
      ed89275c
    • Xavier Leroy's avatar
      Introduce and use PrintAsmaux.variable_section · 30feb31c
      Xavier Leroy authored
      This is a generalization of the previous PrintAsmaux.common_section
      function that
      - handles initialized variables in addition to uninitialized variables;
      - can be used for Section_const, not just for Section_data.
      30feb31c
  12. 21 Jan, 2021 3 commits
  13. 18 Jan, 2021 4 commits
  14. 16 Jan, 2021 2 commits
    • Xavier Leroy's avatar
      Support re-normalization of function parameters at function entry · 478ece46
      Xavier Leroy authored
      This is complementary to 28f235806
      
      Some ABIs leave more flexibility concerning function parameters than
      CompCert expects.
      
      For instance, the AArch64/ELF ABI allow the caller of a function to
      leave unspecified the "padding bits" of function parameters.  As an
      example, a parameter of type "unsigned char" may not have zeros in
      bits 8 to 63, but may have any bits there.
      
      When the caller is compiled by CompCert, it normalizes argument values
      to the parameter types before the call, so padding bits are always
      correct w.r.t. the type of the argument.  This is no longer guaranteed
      in interoperability scenarios, when the caller is not compiled by CompCert.
      
      This commit adds a general mechanism to insert "re-normalization"
      conversions on the parameters of a function, at function entry.
      This is controlled by the platform-dependent function
      Convention1.return_value_needs_normalization.
      
      The semantic preservation proof is still conducted against the
      Com...
      478ece46
    • Xavier Leroy's avatar
      Change warning for pragmas inside functions · 6bef8690
      Xavier Leroy authored
      Follow-up to 35e2b11d.
      
      Put the warning "pragmas are ignored inside functions" inside the Unnamed
      category, so that it is displayed by default and cannot be disabled.
      6bef8690
  15. 15 Jan, 2021 1 commit
    • Xavier Leroy's avatar
      PowerPC: wrong computation of the position of the first vararg argument · 15f35478
      Xavier Leroy authored
      In function Asmexpand.next_arg_locations:
      
      If 7 integer parameter passing registers have been used already,
      and the next fixed arguments are Tlong then Tint, the Tlong argument
      was correctly analyzed as being passed on the stack, but the Tint
      argument was incorrectly analyzed as being passed in the 8th register.
      15f35478
  16. 14 Jan, 2021 2 commits
    • Xavier Leroy's avatar
      Coq 8.13.0 is supported · 0895388e
      Xavier Leroy authored
      However it produces new warnings that should be investigated later.
      0895388e
    • Xavier Leroy's avatar
      RISC-V: fix FP calling conventions · 88567ce6
      Xavier Leroy authored
      This is a follow-up to e81d015e.
      
      In the RISC-V ABI, FP arguments to functions are passed in integer registers
      (or pairs of integer registers) in two cases:
      1- the FP argument is a variadic argument
      2- the FP argument is a fixed argument but all 8 FP registers reserved for
         parameter passing have been used already.
      
      The previous implementation handled only case 1, with some problems.
      
      This commit implements both 1 and 2.  To this end, 8 extra FP
      caller-save registers are used to hold the values of the FP arguments
      that must be passed in integer registers.  Fixup code moves these FP
      registers to integer registers / register pairs.  Symmetrically, at
      function entry, the integer registers / register pairs are moved back
      to the FP registers.
      
      8 extra FP registers is enough because there are only 8 integer
      registers used for parameter passing, so at most 8 FP arguments may
      need to be moved to integer registers.
      88567ce6
  17. 13 Jan, 2021 2 commits
    • Xavier Leroy's avatar
      Replace `omega` tactic with `lia`, continued · 522285d1
      Xavier Leroy authored
      Follow-up to aba0e740
      522285d1
    • Xavier Leroy's avatar
      Improve branch tunneling · 7f152e2f
      Xavier Leroy authored
      The previous branch tunneling was missing optimization opportunities
      introduced by the optimization of conditional branches.  For example:
      
      L1: instr; branch L2
      L2: if cond then branch L3 else branch L4
      L3: branch L4
      L4: ...
      
      was transformed into
      
      L1: instr; branch L2
      L2: branch L4
      L3: branch L4
      L4: ...
      
      missing a tunneling opportunity (branch L2 -> branch L4).
      
      This commit improves branch tunneling so that the expected code is produced:
      
      L1: instr; branch L4
      L2: branch L4
      L3: branch L4
      L4: ...
      
      To this end, additional equalities are introduced in the union-find
      data structure corresponding to optimizable conditional branches.
      
      In rare cases these additional equalities trigger new opportunities for
      optimizing conditional branches.  Hence we iterate the analysis
      until no optimizable conditional branch remains.
      7f152e2f