1. 11 Oct, 2018 1 commit
  2. 12 Sep, 2018 1 commit
  3. 15 Jun, 2018 1 commit
  4. 15 Mar, 2018 1 commit
  5. 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
      this:
      
      - 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
      examples.
      f9ff4e02
  6. 15 May, 2017 1 commit
  7. 01 Jan, 2017 1 commit
  8. 22 Feb, 2016 2 commits
  9. 05 Feb, 2016 1 commit
    • Andrei Paskevich's avatar
      Mlw_expr: fix potentially unsound pattern matching in programs · 2d1a5883
      Andrei Paskevich authored
      split the ppat_ghost field in program patterns into two distinct
      conditions:
      - ppat_ghost, indicating that the pattern starts as ghost,
        meaning that all variables in it are ghost, too;
      - ppat_fail, meaning that the pattern contains a refutable
        ghost subpattern, which makes the match in the extracted code
        impossible, which makes the whole match expression ghost.
      
      Until now, the two conditions were disjunctively combined, making
      admissible the invalid pattern matching in bench/p/b-d/ghost4.mlw.
      2d1a5883
  10. 10 Jan, 2016 1 commit
    • Andrei Paskevich's avatar
      Mlw_expr: fix potentially unsound pattern matching in programs · eda92a0b
      Andrei Paskevich authored
      split the ppat_ghost field in program patterns into two distinct
      conditions:
      - ppat_ghost, indicating that the pattern starts as ghost,
        meaning that all variables in it are ghost, too;
      - ppat_fail, meaning that the pattern contains a refutable
        ghost subpattern, which makes the match in the extracted code
        impossible, which makes the whole match expression ghost.
      
      Until now, the two conditions were disjunctively combined, making
      admissible the invalid pattern matching in bench/p/b-d/ghost4.mlw.
      eda92a0b
  11. 24 Aug, 2015 1 commit
  12. 03 Jul, 2015 1 commit
  13. 11 Sep, 2014 1 commit
  14. 20 Jan, 2014 1 commit
    • Andrei Paskevich's avatar
      WhyML: add "diverges", "reads {}", and "writes {}" effect clauses · 83858597
      Andrei Paskevich authored
      - "diverges" states that the computation may not terminate (which
        does not mean that is always diverges: just as any other effect
        annotation, this clause states a possibility of a side effect).
      
      - "reads {}" states that the computation does not access any variable
        except those that are listed elsewhere in the specification (or the
        proper function arguments, if "reads" is in a function spec).
      
      - "writes {}" states that the computation does not modify any mutable
        value.
      
      - If a function definition or an abstract computation may diverge,
        but there is no "diverges" clause in the specification, a warning
        is produced. If a function definition or an abstract computation
        always terminates, but there is a "diverges" clause in the spec,
        an error is produced.
      
      - If there is a "reads" or a "writes" clause in a function definition
        or an abstract computation, then every modified value must be listed
        in "writes" and every accessed external variable not mentioned in
        the spec must be listed in "reads". (Notice that this is a stricter
        requirement than before, when the presence of a "writes" clause
        did not require to specify "reads".) However, one does not have to
        write "reads {}" or "writes {}" if the corresponding lists are empty.
      83858597
  15. 19 Jan, 2014 1 commit
  16. 20 Nov, 2013 1 commit
  17. 28 Apr, 2013 1 commit
  18. 24 Apr, 2013 1 commit
  19. 22 Apr, 2013 2 commits
    • Andrei Paskevich's avatar
      one more test · 66257bde
      Andrei Paskevich authored
      66257bde
    • Andrei Paskevich's avatar
      whyml: ensure the absence of alias in function types · 3cd56b05
      Andrei Paskevich authored
      One exception to this rule is the the result type in a non-recursive
      function may contain regions coming the function's arguments (though
      not from the context). It is sometimes useful to write a function
      around a constructor or a projection: see function [create] in
      verifythis_fm2012_LRS.mlw. For recursive functions we impose
      the full non-alias discipline.
      3cd56b05
  20. 07 Apr, 2013 2 commits
    • Andrei Paskevich's avatar
      whyml: drop read effects · 9fd9469c
      Andrei Paskevich authored
      Now that ghost writes are checked via e_syms.syms_pv,
      there is no use for read effects anymore.
      9fd9469c
    • Andrei Paskevich's avatar
      whyml: reimplement verification of the ghost writes · 30c225b4
      Andrei Paskevich authored
      This fixes one bug and several deficiencies in the previous
      implementation, which was based on read effects. One caveat
      about the current version is that we treat all type variables
      in a polymorphic type as visible (= non-ghost) even if they
      only occur in the ghost fields. For example, the following
      code is rejected:
      
        type strange 'a = { ghost contents : 'a }
      
        let test () =
          let x = { contents = ref 0 } in
          x.contents := 42
      
      Even though the field [contents] is ghost and cannot be reached
      from the real-world code, the type of x is [strange (ref int)]
      and the region of the reference is considered to be visible.
      Thus the last assignment is seen as an illicit ghost write.
      
      On the other hand,
      
        type strange 'a = { ghost contents : ref 'a }
      
      and
      
        type strange 'a = { ghost mutable contents : 'a }
      
      permit ghost writes into [contents] without problem.
      Ghost writes into ghost variables are also okay.
      30c225b4
  21. 06 Apr, 2013 1 commit
    • Andrei Paskevich's avatar
      whyml: keep track of pvsymbols and psymbols in expressions · dce120fa
      Andrei Paskevich authored
      this commit changes the way of tracking occurrences of regions
      and type variables for the purposes of generalization, effect
      filtering, and effect checks. It restricts the previous
      implementation in two aspects:
      
      - a psymbol p can be monomorphic (= non-generalizable) in an effect
        only if p depends (= is defined via) a pvsymbol whose type contains
        the affected region. See bench/programs/bad-typing/recfun.mlw
        for an example. This restriction is required for soundness.
      
      - an argument of a psymbol cannot contain a region shared with
        another argument or an external pvsymbol. However, we do not
        require (so far) that the argument's type doesn't contain the same
        region twice and we allow the result type to contain known regions.
        This restriction is not necessary for soundness, and is introduced
        only to avoid some unintentional user errors and reduce the gap
        between the types that can be implemented in a "let" and the types
        that can be declared in a "val".
      dce120fa
  22. 27 Mar, 2013 1 commit
  23. 04 Mar, 2013 1 commit
    • Andrei Paskevich's avatar
      whyml: match expression is ghost if we look inside ghost fields · 43b684d0
      Andrei Paskevich authored
      We store in every lsymbol a new integer field ls_constr,
      equal to zero if the lsymbol is not a constructor, and equal
      to the number of constructors of the lsymbol's type otherwise.
      It is allowed to declare or define an lsymbol with ls_constr > 0
      as an ordinary function (otherwise algebraic type elimination
      wouldn't work - though we might still check this in theories),
      but it is forbidden to use a wrong ls_constr in algebraic type
      definitions.
      
      The ghostness of a match expression is now determined as follows:
      
      If at least one branch expression is ghost,
        then the match is ghost;
      else if there is only one branch,
        then the match is not ghost;
      else if the matched expression is ghost,
        then the match is ghost;
      else if at least one pattern matches a ghost field
              against a constructor with ls_constr > 1
        then the match is ghost;
      else
        the match is not ghost.
      
      We do just enough to recognize obvious non-ghost cases, and
      make no attempt to handle redundant matches or to detect
      exhaustive or-patterns in subpatterns.
      43b684d0
  24. 03 Mar, 2013 1 commit
    • Andrei Paskevich's avatar
      track dangerous applications of equality · bb6734a1
      Andrei Paskevich authored
      In programs, but also in pure theories, it is not safe to compare
      arbitrary types. For example, if we have a record with ghost fields,
      a comparison may produce different results before and after ghost
      code elimination. Even for pure types like 'map' or 'set', it is
      unlikely that the result of logical equality will be the same as
      the result of OCaml structural equality on the implemented type.
      
      This commit makes the first step towards fixing this issue.
      We proceed in the following way:
      
      1. Every lsymbol (pure function or predicate symbol) carries
         a subset of type variables of its signature, called "opaque
         type variables". By marking a type variable 'a opaque in an
         lsymbol's signature, the user guarantees that this lsymbol
         can be implemented without ever comparing values of type 'a.
         In other words, this is a promise not to break into a type
         variable.
      
         The corresponding syntax is: "predicate safe (x y : ~'a)".
      
         All type variables in undefined symbols are non-opaque,
         unless annotated otherwise. Non-opaque is the default
         to keep the change conservative.
      
         Opacity of type variables in defined symbols is inferred
         from the definition. If the definition violates a given
         opacity annotation, an exception is raised. Notice that
         we only check definitions in _theory_ declarations. One
         can define an lsymbol in a _task_ in a way that violates
         opacity. We cannot forbid it, because various elimination
         transformations would replace safe operations (such as
         matching) with equalities. This is not a problem, since in
         the pure logical realm of provers opacity is not required
         One exception would be Coq, whose transformation chain must
         never perform such operations.
      
         All type variables in inductive predicates are non-opaque.
         Indeed, we can redefine equality via an inductive predicate.
         [TODO: find safe forms of inductive definitions and implement
         more reasonable restrictions.]
      
         All type variables in constructors and field symbols are opaque.
      
         It is forbidden to instantiate an opacity-preserving symbol
         with an opacity-breaking one in a clone substitution.
      
      2. Similar type variable tracking is implemented for program symbols.
         Type variables in the signature of a "val" are non-opaque unless
         annotated otherwise. Opacity of type variables in defined symbols
         is inferred from the definition, and an exception is raised, if
         a given annotation is violated.
      
         The internal mechanism of tracking is different: the "eff_compar"
         field in effects contains the type variables that occur under
         equality or any other opacity-breaking operation. In this respect,
         our API is inconsistent between lsymbols and psymbols: the former
         asks for the opaque tvsymbols, the latter requires us to fill the
         spec with "comparison effects" for the non-opaque ones. [TODO:
         add the "~opaque" argument to create_psymbol and make the WhyML
         core fill the effect under the hood.]
      
         Every time an lsymbol or a psymbol is applied in a program,
         we check the substitution into its signature's type variables.
         If a non-opaque type variable is instantiated with a program type,
         an exception is raised. [TODO: be more precise and reject only
         types with ghost and model components - being mutable, private,
         or carrying an invariant doesn't conflict with equality.]
      
         Notice that we do not allow to compare program types even in
         the ghost code. This is not needed if we only consider the
         problems of the code extraction, but _might_ be necessary,
         if we also want to protect Coq realisations (see below).
      
      This commit fixes the immediate problem of breaking the ghost
      guarantees when equality or some other opacity-breaking lsymbol
      is applied in a program to a type with ghost or "model" parts.
      
      This leaves the problem of code extraction for programs that
      compare complex types such as maps or sets (Coq driver is
      affected by this, too, I guess). The next step is to provide
      annotations for problematic type constructors. A declaration
      "type ~map 'a 'b" would mean "logical equality on this type
      is likely to be different from the structural equality on any
      implementation of this type - therefore do not apply equality
      to it: neither in programs (because this can't be implemented),
      nor in pure functions (because they are extracted, too, and
      because this can't be realized with Leibniz equality in Coq)."
      [TODO: discuss and implement.]
      
      [TODO: mb choose better term for "opaque" and notation for ~'a.]
      bb6734a1
  25. 12 Oct, 2012 1 commit
  26. 04 Aug, 2012 1 commit
  27. 02 Aug, 2012 1 commit
  28. 20 Jul, 2012 1 commit
  29. 13 Jul, 2012 1 commit
  30. 12 Jul, 2012 1 commit
  31. 23 Jun, 2012 1 commit
  32. 03 Feb, 2012 2 commits
  33. 20 Sep, 2011 1 commit
  34. 14 Sep, 2011 1 commit
  35. 04 Aug, 2011 1 commit
  36. 11 Jul, 2011 1 commit