1. 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 28f23580
      
      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
      CompCert model, where the argument values of functions are already
      normalized.  What the proof shows is that the extra conversions have
      no effect in this case.  In future work we could relax the CompCert
      model, allowing functions to pass arguments that are not normalized.
      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
  2. 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
  3. 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
  4. 13 Jan, 2021 5 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
    • Xavier Leroy's avatar
      Revised correctness proof for record_goto · e16f5d1d
      Xavier Leroy authored
      We used to define an instrumented version record_goto' that also
      builds the measure f, prove it correct, then show equivalence with
      record_goto.
      
      The new proofs make do without the instrumented version.  They prove
      strong existence of the measure, as in
      `{ f | branch_map_correct (record_goto fn) f}`.
      e16f5d1d
    • Xavier Leroy's avatar
      Add new fold_ind induction principle for folds · bbf3b414
      Xavier Leroy authored
      fold_inv is in Type, hence can prove goals such as `{ x | P x }`.
      Also, no extensionality property is needed.
      
      fold_rec is now derived from fold_inv.
      bbf3b414
    • Xavier Leroy's avatar
      Add lemma list_norepet_rev · dd191041
      Xavier Leroy authored
      dd191041
  5. 10 Jan, 2021 1 commit
  6. 07 Jan, 2021 1 commit
    • Xavier Leroy's avatar
      Ignore and warn about pragmas inside functions · 35e2b11d
      Xavier Leroy authored
      Pragmas can occur either outside external declarations, at the top level
      of a compilation unit, or within a compound statement, inside a function
      definition.
      
      The parse tree in cparse/C.mli cannot represent pragmas occuring within
      a compound statement.
      
      In this case, the elaborator used to silently move the pragma to top
      level, just before the function definition where the pragma occurs.
      
      It looks safer to just ignore pragmas occurring inside a function
      definition, and emit a specific warning.
      35e2b11d
  7. 29 Dec, 2020 2 commits
    • 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
    • Xavier Leroy's avatar
      Remove useless parameters in theorems int_round_odd_bits and int_round_odd_le · 2e202e2b
      Xavier Leroy authored
      IEEE754_extra: clear unused context so that none of the context is
      picked up by tactics and ends as extra parameters to theorems
      int_round_odd_bits and int_round_odd_le
      
      Floats: simplify uses of int_round_odd_bits and int_round_odd_le
      accordingly.
      2e202e2b
  8. 28 Dec, 2020 3 commits
  9. 26 Dec, 2020 5 commits
  10. 25 Dec, 2020 3 commits
  11. 24 Dec, 2020 3 commits
  12. 11 Dec, 2020 1 commit
  13. 06 Dec, 2020 5 commits
    • 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
    • Xavier Leroy's avatar
      PowerPC modeling of registers destroyed by pseudo-instructions · 5e389894
      Xavier Leroy authored
      Inlined built-in functions destroy GPR0
      5e389894
    • Xavier Leroy's avatar
      ARM modeling of registers destroyed by pseudo-instructions · a4cfb9c2
      Xavier Leroy authored
      Pflid destroys IR14
      Inlined built-in functions destroy IR14
      a4cfb9c2
    • Xavier Leroy's avatar
      AArch64 modeling of registers destroyed by pseudo-instructions · 0df99dc4
      Xavier Leroy authored
      Pfmovimms, Pfmovimmd destroy X16
      Pbtbl preserves X17
      Inlined built-in functions destroy X16 and X30
      0df99dc4
    • Xavier Leroy's avatar
      Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructions · ef5477a4
      Xavier Leroy authored
      Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat
      PowerPC operations.
      
      The pseudoinstructions were used to implement these operations,
      as follows:
      
      Pfcfi  : Ofloatofint   i.e. the conversion signed int32 -> float64
      Pfcfiu : Ofloatofintu  i.e. the conversion unsigned int32 -> float64
      Pfctiu : Ointuoffloat  i.e. the conversion float64 -> unsigned int32
      
      These pseudoinstructions were expanded (in Asmexpand.ml) in terms of
      
      Pfcfid  : signed int64 -> float64
      Pfctidz : float64 -> signed int64
      
      and int32/int64 conversions.
      
      This commit performs this expansion during instruction selection
      (SelectOp.vp):
      
      floatofint(n)  becomes floatoflong(longofint(n))
      floatofintu(n) becomes floatoflong(longuofint(n))
      intuoffloat(n) becomes cast32unsigned(longoffloat(n))
      
      Then there is no need for the 3 removed operations and the 3 removed
      pseudoinstructions.
      
      More importantly, the correctness of these expansions is now proved as
      part of instruction selection, using the corresponding results from
      Floats.v.
      ef5477a4
  14. 16 Nov, 2020 1 commit
  15. 14 Nov, 2020 2 commits
  16. 09 Nov, 2020 1 commit
  17. 08 Nov, 2020 1 commit
  18. 07 Nov, 2020 1 commit