1. 18 Jul, 2018 1 commit
  2. 17 Jul, 2018 1 commit
    • Andrei Paskevich's avatar
      Ident: disambiguated symbolic notation · 295cacf4
      Andrei Paskevich authored
      It is possible to append an arbitary number of quote symbols
      at the end of an prefix/infix/mixfix operator:
                  applied form      standalone form
                    -' 42               (-'_)
                    x +' y              (+')
                    a[0]' <- 1          ([]'<-)
      Pretty-printing will use the quote symbols for disambiguation.
      The derived symbols can be produced by Why3 by appending
      a suffix of the form "_toto" or "'toto". These symbols can
      be parsed/printed as "(+)_toto" or "(+)'toto", respectively.
  3. 07 Jul, 2018 1 commit
    • Andrei Paskevich's avatar
      confine all notation handling inside Ident · 0fea401c
      Andrei Paskevich authored
      This commit removes all hard-coded "infix ..", "prefix ..",
      and "mixfix .." from the rest of the code, and handles the
      symbolic notation entirely inside Ident. It does not change
      the notation itself.
  4. 05 Jun, 2018 1 commit
  5. 01 Jun, 2018 1 commit
  6. 17 May, 2018 1 commit
  7. 16 Apr, 2018 2 commits
  8. 21 Mar, 2018 1 commit
    • Guillaume Melquiond's avatar
      Homogenize constructor names. · 6ef0273e
      Guillaume Melquiond authored
      The pattern-matching construct in the logic is now systematically named
      "Tcase" in constructors (Ptree.Tmatch -> Tcase). The one in the
      programs (supporting exceptions) is now systematically named "Ematch"
      (Expr.Ecase -> Ematch, Dexpr.DEcase -> DEmatch). They are now homogeneous
      with the other constructors: Term.Tcase, Dterm.DTcase, Ptree.Ematch,
      Mltree.Ematch. Smart constructor Expr.e_case was renamed accordingly.
  9. 20 Mar, 2018 1 commit
  10. 14 Feb, 2018 1 commit
  11. 11 Jan, 2018 1 commit
  12. 01 Dec, 2017 1 commit
  13. 28 Nov, 2017 1 commit
    • Andrei Paskevich's avatar
      Ity: "spoil" effect on type variables · 330bd7e5
      Andrei Paskevich authored
      Type variables that appear in the result types of "pure"
      or logical functions are "spoiled" and cannot be instantiated
      with mutable types. Abstract program functions ("val") are assumed
      to not spoil type variables, and no explicit effect annotation is
      provided for this effect. Constructors, projections, and function
      application do not spoil type variables.
      This effect prevent unsoundness that results from instantiating
      [constant magic : 'a] with a mutable type in a program. It is,
      however, less precise than tracking of magic values using
      pure type variables. For example, the following program
      does typecheck with pure type variables but not with the
      spoil effects.
        use seq.Seq
        type ref_hist 'a = {
                mutable contents : 'a;
          ghost mutable history  : Seq.seq {'a}
        let (:=) (r : ref_hist 'a) (v : 'a) =
          r.history <- Seq.cons (pure { r.contents }) r.history;
          r.contents <- v
        let test (r : ref_hist (ref_hist unit)) =
          r := r.contents
      Indeed, (:=) spoils 'a, and precludes it from being instantiated
      with a mutable type in "test".
  14. 24 Nov, 2017 1 commit
  15. 23 Nov, 2017 1 commit
  16. 22 Nov, 2017 1 commit
  17. 20 Nov, 2017 1 commit
  18. 07 Nov, 2017 1 commit
  19. 17 Oct, 2017 1 commit
  20. 13 Jun, 2017 1 commit
    • Andrei Paskevich's avatar
      Expr: execute abstract blocks and whiteboxes with unfiltered effect · f9ff4e02
      Andrei Paskevich authored
      This commit also contains a fix for a curious exploit of our type
      system which was made possible by a combination of local exceptions
      and a special treatment of abstract blocks and whiteboxes.
      Local exceptions allow us to exploit the type inference mechanism
      and to force the same regions onto unrelated expressions. This is due
      to the fact that local exceptions are region-monomorphic (this may be
      relaxed in future). Of course, this was always possible via the API,
      and the false aliases do not threaten the soundness of the system,
      thanks to the following critical invariant:
        An allocation of a new mutable value always has an associated reset
        effect which invalidates the existing variables of the same type.
      So, if two variables share a region, then exactly one of three
      conditions must hold:
      1. They are actually aliased, and modification of one must change
         the other in the VC.
      2. They are not aliased, but the newer one invalidates the other:
         this is a case of false alias made benign by the reset effect.
      3. The shared region is not actually reachable from the newer one:
              let x = if true then None else Some r
         this is another false alias, without an associated reset effect,
         yet still benign since the shared region is not reachable from x.
      However, the type system and the VC generator must have the exact
      same view on who's who's alias. If the VCgen encounters in the
      same control flow two variables with a shared region in the type,
      then the type system must have ensured one of the three conditions
      above. Prior to this commit, there were two cases which violated
      - An exception raised in an abstract block that does not have
        an exceptional postcondition for it, escapes into the main
        control flow.
      - A whitebox, by its nature, is fully handled inside the main
        control flow.
      The violation came from the fact that abstract blocks and whiteboxes
      are stored as cexps and so their effect is filtered by Ity.create_cty
      in order to hide effects on variables allocated and collected inside
      the block. This is a useful and necessary feature, except when the
      VC of the block escapes into the main control flow and the forced
      false aliases -- unchecked by the type system -- are seen by VCgen.
      The implemented fix resolves the issue by restoring the hidden
      effects for abstract blocks and whiteboxes.
      Check bench/programs/bad-typing/false_alias*.mlw for two concrete
  21. 11 Jun, 2017 1 commit
  22. 10 Jun, 2017 1 commit
  23. 09 Jun, 2017 1 commit
  24. 08 Jun, 2017 2 commits
    • Andrei Paskevich's avatar
      WhyML: "{qualid}" for logical symbols and snapshotted variables · a44cccbb
      Andrei Paskevich authored
      x.{f} is allowed and can be used for unary applications
      M.{f} is not allowed, use {M.f} instead
    • Andrei Paskevich's avatar
      Mlw: for-loops over range types · 2f7b69b5
      Andrei Paskevich authored
      In the surface language, the loop index is always int in
      the loop invariant and all annotations and pure terms inside
      the loop. If you want to access the original range-typed index,
      use "let copy_i = i in" in the program code before your assertion.
      Of course, you cannot do that for the loop invariant, which is
      what we want.
  25. 05 Jun, 2017 2 commits
    • Andrei Paskevich's avatar
      Mlw: labels can act as local exceptions · cda6d915
      Andrei Paskevich authored
      Useful to break out of the loops:
        label Break in
        while ... do
          label Continue in
          ... raise Break ...
          ... raise Continue ...
      When a label is put over a non-unit expression,
      raise acts as return:
        label Return in
        if ... then raise Return 42; 0
      Also, "return <expr>" returns from the innermost function.
      This includes abstract blocks, too, so if you want to return
      across an abstract block, you should rather use a label at
      the top of the main function. TODO/FIXME: maybe we should
      let "return" pass across abstract blocks by default, to
      avoid surprises?
      One shortcoming of the labels-as-exceptions is that they cannot
      be used to transmit tuples with ghost elements, nor return ghost
      values from non-ghost expressions. A local exception with an
      explicit mask should be used instead. Similarly, to return
      a partially ghost value from a function, it must have have
      its mask explicitly written (which is a good practice anyway).
      We cannot know the mask of an expr before we construct it,
      but in order to construct it, we need to create the local
      exceptions first.
      Another caveat is that while it is possible to catch an exception
      generated by a label, you should avoid to do so. We only declare
      the local exception if the expression under the label _raises_
      the exception, and thus the following code will not typecheck:
        label X in (try raise X with X -> () end)
      Indeed, the expression in the parentheses does not raise X,
      and so we do not declare a local exception X for this label,
      and so the program contains an undeclared exception symbol.
    • Andrei Paskevich's avatar
      Mlw: API for local exceptions · 53b3ec88
      Andrei Paskevich authored
  26. 03 Jun, 2017 1 commit
  27. 22 May, 2017 1 commit
  28. 20 May, 2017 1 commit
  29. 11 May, 2017 1 commit
    • Andrei Paskevich's avatar
      Pdecl: split type declarations in chunks · b6e2a7b6
      Andrei Paskevich authored
      Refinement code requires private types to reside in
      separate program declarations. So we split type decls
      into chunks where all non-free types are declared
      separately and only constructible (Ddata) types are
      kept together. The code preserves the original order
      wherever possible.
      Also, export ls_of_rs and fd_of_rs from Expr: these are
      used everywhere in src/mlw anyway.
      Also, remove some range/float-related "assert false".
  30. 28 Apr, 2017 2 commits
  31. 12 Apr, 2017 1 commit
  32. 28 Feb, 2017 1 commit
    • Clément Fumex's avatar
      Add the ability to · f0547868
      Clément Fumex authored
      * declare range types and float types,
      * use integer (resp. real) literals for those types through casting,
      * specify how to print them in drivers.
      Change in syntax
      * use
        type t = < range 1 2 >   (* integers from 1 to 2 *)
        type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)
        the two projections :
        and the predicate :
      * Restrict the use of "'" in whyml:
        Users are not allowed to introduce names where a quote symbol
        is followed by a letter. Thus, the following identifiers are
        whereas toto'phi is not.
      Note: we do not yet support negative numbers in range declaration
      and casting of a literal.
  33. 15 Feb, 2017 1 commit
  34. 18 Apr, 2016 1 commit
  35. 14 Apr, 2016 2 commits