1. 25 Feb, 2016 1 commit
  2. 10 Feb, 2016 1 commit
  3. 11 Jan, 2016 2 commits
  4. 10 Jan, 2016 1 commit
    • Andrei Paskevich's avatar
      Mlw: allow non-ghost expressions to return (partially) ghost values · 4c79348a
      Andrei Paskevich authored
      this is still work in progress and no testing was done so far.
      
      Highlights of this commit:
      
      - "(ghost 42, 15)" is now a non-ghost expression that can be returned
        from a function and/or matched against a "(ghost x, y)" pattern.
        Only the tuple constructor and direct pattern matching are magical:
        "let z = (ghost 42, 15) in ..." still makes z ghost, and therefore
        "snd (ghost 42, 15)" is ghost, too.
      
      - "if c then e1 else ghost e2" and "let z = e1 in ghost e2" are now
        non-ghost expressions with a ghost result. This means that e1 may
        have visible effects. Of course, if e2 raises exceptions, the whole
        expression is ghostified. Contamination is still done when possible,
        that is, when the contaminated expression has no visible effects.
      
      - "let ghost x = e1 in e2" no longer ghostifies e1.
      
      - "let f (ghost x) = ... in f e1" no longer ghostifies e1.
      
      - new syntax: variables in program patterns may be marked ghost.
        In particular: "let x, ghost y = ...".
      
      - new syntax: the function result type may be written as a partially
        ghost tuple: "val f ... : ghost int" or "any (int, ghost bool)".
        The ghostness annotation is required for top-level and recursive
        functions.
      
      - exceptions can carry partially ghost tuples (API only, WIP)
      4c79348a
  5. 07 Dec, 2015 1 commit
  6. 24 Nov, 2015 1 commit
  7. 15 Nov, 2015 1 commit
    • Andrei Paskevich's avatar
      Mlw: admit fields with mutable types in private records · f522e56e
      Andrei Paskevich authored
      this should not be problematic as long as these fields do not occur
      in the invariants (actual or refined). In other words, a value of
      a private type exists no matter what is stored in the field.
      
      Also, admit non-private mutable types without actual mutable fields.
      It is actually impossible to create a write effect for such types,
      and the only consequence of being mutable is that they are assigned
      a region, and so every value of such type can be tracked individually.
      One use case for this is a non-private record with an invariant,
      which either has fields with mutable types or has type parameters
      that we wish to instantiate with mutable types. If we modify these
      mutable components, this may break the record's invariant. Now, if
      the record itself is immutable (and thus has no associated region),
      then we must reestablish the invariant immediately, otherwise we
      lose track of the value. Even if this extra flexibility does not
      prove useful in the end, it seems to be harmless.
      
      Also, admit type definitions of the form
        type t 'a = (private|abstract)? mutable? {} invariant*
      which define private empty records (even if not declared private).
      
      Also, "type t 'a" is now equivalent to "type t 'a = private {}".
      f522e56e
  8. 13 Nov, 2015 1 commit
  9. 10 Nov, 2015 1 commit
  10. 08 Nov, 2015 1 commit
  11. 18 Sep, 2015 1 commit
  12. 22 Aug, 2015 1 commit
  13. 31 Jul, 2015 1 commit
  14. 30 Jul, 2015 1 commit
    • Léon Gondelman's avatar
      Ity: resets are protected by a common set of covers · faf9a2be
      Léon Gondelman authored
      The effects now must satisfy the following invariants:
      
      1. Every region in eff_writes, eff_taints, and eff_covers
         must occur in the type of some variable in eff_reads.
      
      2. Both eff_taints and eff_covers are subsets of eff_writes.
      
      3. eff_covers and eff_resets are disjoint.
      
      4. Every region in eff_writes is either in eff_covers or
         is stale (according to Ity.reg_r_stale) and forbidden
         for the later use.
      
      Also, this commit rewrites Ity.eff_assign and Ity.eff_strong
      (renamed now to eff_reset_overwritten) to handle correctly
      parallel assignments.
      faf9a2be
  15. 15 Jul, 2015 1 commit
    • Andrei Paskevich's avatar
      Parser: relation chaining is guided by the operator group · c67b99bd
      Andrei Paskevich authored
      All infix operations in the weakest priority group (those containing
      at least one of the characters '=', '<', '>', or '~') are considered
      non-associative and the chains (t1 OP t2 OP t3) are translated into
      conjunctions (t1 OP t2 /\ t2 OP t3).
      
      This does not concern implication '->' and equivalence '<->'
      which are right-associative. like the rest of propositional
      connectives.
      c67b99bd
  16. 07 Jul, 2015 1 commit
  17. 02 Jul, 2015 1 commit
  18. 27 Jun, 2015 1 commit
  19. 24 Jun, 2015 2 commits
  20. 09 Jun, 2015 3 commits
  21. 28 May, 2015 1 commit
  22. 21 May, 2015 1 commit
  23. 29 Apr, 2015 1 commit
  24. 21 Mar, 2015 1 commit
  25. 20 Mar, 2015 2 commits
  26. 19 Mar, 2015 1 commit
  27. 18 Feb, 2015 1 commit
  28. 22 Jan, 2015 2 commits
  29. 21 Jan, 2015 2 commits
  30. 20 Jan, 2015 1 commit
  31. 19 Jan, 2015 1 commit
    • Andrei Paskevich's avatar
      Expr: rename 'psymbol' to 'rsymbol' (routine) · 58586dac
      Andrei Paskevich authored
      1. We really need to distinguish first-class functions (mappings),
      pure logical functions (functions and predicates), and program
      functions (routines).
      
      2. The ps_ prefix is already used for predicate symbols.
      
      3. 'psymbol' and 'pvsymbol' are too similar.
      58586dac
  32. 18 Jan, 2015 1 commit
  33. 06 Jan, 2015 1 commit