1. 29 Jan, 2015 1 commit
    • Robbert Krebbers's avatar
      mem_force no longer flattens the entire subobject for "unsigned char" · 5644d68f
      Robbert Krebbers authored
      The operation "mem_force Γ m a" used to apply the identify function to
      pricisely the object "a", even in case "a" is an "unsigned char" address
      refering to an individual byte. This caused the ctree substructure of the
      entire subobject to disappear and had the undesired effect that:
        mem_force Γ a m ⊑{Γ,true@Γm} m
      failed to hold (i.e. unused reads cannot be removed).
  2. 27 Jan, 2015 1 commit
    • Robbert Krebbers's avatar
      Let the malloc expression non-deterministically yield NULL. · fdcc90dd
      Robbert Krebbers authored
      * This behavior is "implementation defined" and can be turned on and off
        using the Boolean field "alloc_can_fail" of the class "Env".
      * The expression "EAlloc" is now an r-value of pointer type instead of an
      * The executable semantics for expressions is now non-deterministic. Hence,
        some proofs had to be revised.
  3. 25 Jan, 2015 2 commits
  4. 23 Dec, 2014 1 commit
    • Robbert Krebbers's avatar
      More lenient pointer equality. · 914f32ee
      Robbert Krebbers authored
      Pointer equality is now defined using absolute object offsets. The treatment
      is similar to CompCert:
      * Equality of pointers in the same object is defined provided the object has
        not been deallocated.
      * Equality of pointers in different objects is defined provided both pointers
        have not been deallocated and both are strict (i.e. not end-of-array).
      Thus, pointer equality is defined for all pointers that are not-end-of-array
      and have not been deallocated. The following examples have defined behavior:
        int x, y;
        printf("%d\n", &x == &y);
        int *p = malloc(sizeof(int)), *q = malloc(sizeof(int));
        printf("%d\n", p == q);
        struct S { int a; int b; } s, *r = &s;
        printf("%d\n", &s.a + 1 == &(r->b));
      The following not:
        int x, y;
        printf("%d\n", &x + 1 == &y);
  5. 17 Dec, 2014 1 commit
  6. 16 Dec, 2014 1 commit
    • Robbert Krebbers's avatar
      Allow frozen pointer annotations to be refined. · 26917d00
      Robbert Krebbers authored
      The refinement relation on addresses allows union references to be refined:
        (β2 → β1) → RUnion i s β1 ⊆ RUnion i s β2
      The result is that frozen values are below their unfrozen variant, which made
      it possible to prove that constant propagation (see constant_propagation.v) can
      be performed on the level of the memory model.
  7. 23 Nov, 2014 1 commit
  8. 15 Nov, 2014 1 commit
    • Robbert Krebbers's avatar
      More accurate formalization of integer ranks. · da7a14bb
      Robbert Krebbers authored
      Integers with the same size, are no longer supposed to have the same rank. As a
      result, the C integer types (char, short, int, long, long long) are different
      (and thus cannot alias) even if they have the same size. We now have to use a
      more involved definition of integer promotions and usual arithmetic conversions.
      However, this new definition follows the C standard literally.
  9. 06 Nov, 2014 1 commit
  10. 10 Oct, 2014 1 commit
  11. 08 Oct, 2014 1 commit
    • Robbert Krebbers's avatar
      Allow memory refinements to behave like simple renaming. · c5c0d373
      Robbert Krebbers authored
      Memory refinements now carry a boolean parameter that has the following
      [false] : Behave like a simple renaming of memories that merely allows to
                permute object identifiers. It does not allow to refine memories
                into a more defined version.
      [true]  : Behave like before. Objects can be injected, and memory contents can
                be refined into a more defined variant.
      We make refinements parametric in these two variant to avoid code duplication,
      and because the [false] variant is a special case of the [true] variant.
      For completeness of the executable semantics, we now use the [false] variant.
  12. 07 Oct, 2014 1 commit
  13. 03 Oct, 2014 1 commit
  14. 30 Sep, 2014 2 commits
  15. 24 Sep, 2014 1 commit
  16. 16 Sep, 2014 1 commit
  17. 13 Sep, 2014 1 commit
  18. 12 Sep, 2014 2 commits
  19. 06 Sep, 2014 4 commits
  20. 03 Sep, 2014 5 commits
  21. 25 Aug, 2014 1 commit
  22. 22 Aug, 2014 2 commits
    • Robbert Krebbers's avatar
      Modify typing judgments to depend on a description of the types of objects in · 7f9c5994
      Robbert Krebbers authored
      memory instead of the whole memory itself.
      This has the following advantages:
      * Avoid parametrization in {addresses,pointers,pointer_bits,bits}.v
      * Make {base_values,values}.v independent of the memory, this makes better
        parallelized compilation possible.
      * Allow small memories (e.g. singletons as used in separation logic) with
        addresses to objects in another part to be typed.
      * Some proofs become easier, because the memory environments are preserved
        under many operations (insert, force, lock, unlock).
      It also as the following disadvantages:
      * At all kinds of places we now have explicit casts from memories to memory
        environments. This is kind of ugly. Note, we cannot declare memenv_of as a
        Coercion because it is non-uniform.
      * It is a bit inefficient with respect to the interpreter, because memory
        environments are finite functions instead of proper functions, so calling
        memenv_of often (which we do) is not too good.
    • Robbert Krebbers's avatar
      Make simplify_error_equality a bit faster. · 7040c040
      Robbert Krebbers authored
      It is still rather slow, though.
  23. 09 Aug, 2014 1 commit
  24. 07 Aug, 2014 1 commit
  25. 06 Aug, 2014 2 commits
  26. 04 Aug, 2014 1 commit
  27. 10 Jul, 2014 1 commit
  28. 04 Jul, 2014 1 commit