Difference between revisions of "User talk:Schuetzm/scope2"

From D Wiki
Jump to: navigation, search
Line 132: Line 132:
 
     // => SCOPE(needle)  := [] (incomplete)
 
     // => SCOPE(needle)  := [] (incomplete)
  
     for(int i = 0; i < haystack.length - needle.length) {
+
     for(int i = 0; i < haystack.length - needle.length; i++) {
 
         // haystack and needle are read here, but not assigned
 
         // haystack and needle are read here, but not assigned
         // => need scope at least as large as their lifetimes
+
         // => need large enough scope to be accessible at this point
         //    (actually the next higher lifetime would be sufficient,
+
         //    use the variables' lifetimes
        //    but that's more complicated to implement)
 
 
         // => SCOPE(haystack) |= [haystack] = [haystack] (incomplete)
 
         // => SCOPE(haystack) |= [haystack] = [haystack] (incomplete)
 
         // => SCOPE(needle)  |= [needle]  = [needle]  (incomplete)
 
         // => SCOPE(needle)  |= [needle]  = [needle]  (incomplete)
 +
        // (this is optional; instead, we could just assign them their own lifetimes)
 
         T[] sub;
 
         T[] sub;
 
         // => SCOPE(sub) := [] (incomplete)
 
         // => SCOPE(sub) := [] (incomplete)
Line 167: Line 167:
 
     // => satisfiable, now let's check the assignments:
 
     // => satisfiable, now let's check the assignments:
  
     for(int i = 0; i < haystack.length - needle.length) {
+
     for(int i = 0; i < haystack.length - needle.length; i++) {
 
         T[] sub;
 
         T[] sub;
 
         sub = haystack[i .. i + needle.length];
 
         sub = haystack[i .. i + needle.length];
         // [] := [return]    => OK
+
         // [sub] := [return]    => OK
 
         if(sub == needle) {
 
         if(sub == needle) {
 
             // equivalent to: if(opEquals(sub, needle))
 
             // equivalent to: if(opEquals(sub, needle))
Line 195: Line 195:
 
     // => SCOPE(b) = [] (incomplete)
 
     // => SCOPE(b) = [] (incomplete)
 
     return random() % 2 == 0 ? a : b;
 
     return random() % 2 == 0 ? a : b;
 +
    // => SCOPE(a) |= [a] = [a]
 +
    // => SCOPE(b) |= [b] = [b]
 
     // ?: operator affects both `a` and `b`
 
     // ?: operator affects both `a` and `b`
     // => SCOPE(a) |= SCOPE(return) = [] | [return] = [return]
+
     // => SCOPE(a) |= SCOPE(return) = [a] | [return] = [return]
     // => SCOPE(b) |= SCOPE(return) = [] | [return] = [return]
+
     // => SCOPE(b) |= SCOPE(return) = [b] | [return] = [return]
 
     // ---------------------------------------------------
 
     // ---------------------------------------------------
 
     // we now have:
 
     // we now have:
Line 238: Line 240:
 
     // `a` is read
 
     // `a` is read
 
     // => SCOPE(a) |= [a] = [] | [a] = [a] (incomplete)
 
     // => SCOPE(a) |= [a] = [] | [a] = [a] (incomplete)
     // `a` is returned
+
     // `a` is returned and stored in `b`
 
     // => SCOPE(a) |= SCOPE(b) = [a] | [] = [a] (final)
 
     // => SCOPE(a) |= SCOPE(b) = [a] | [] = [a] (final)
 
     // ---------------------------------------------------
 
     // ---------------------------------------------------
Line 266: Line 268:
 
     // ---------------------------------------------------
 
     // ---------------------------------------------------
 
     // => invalid assignment to global_string
 
     // => invalid assignment to global_string
 +
}
 +
</source>
 +
 +
=== Unused stores are ignored ===
 +
 +
<source lang="D">
 +
void foo() {
 +
    int* a, b;
 +
    // => SCOPE(a) = [] (incomplete)
 +
    // => SCOPE(b) = [] (final)
 +
    {
 +
        int x;
 +
        a = &x;
 +
        b = &x;
 +
    }
 +
    writeln(*a);
 +
    // as is read => make sure its scope is large enough
 +
    // => SCOPE(a) |= [a] = [] | [a] = [a] (final)
 +
    // ---------------------------------------------------
 +
    // we now have:
 +
    // SCOPE(a) = [a]
 +
    // SCOPE(b) = []
 +
    // => all resolved
 +
    // ---------------------------------------------------
 +
    // => satisfiable, now let's check the assignments:
 +
 +
    int* a, b;
 +
    // default initialization: a = b = null
 +
    // a: [a] := [static]    => OK
 +
    // b: []  := [static]    => OK
 +
    {
 +
        int x;
 +
        a = &x;    // [a] := [x]    => BAD
 +
        b = &x;    // []  := [x]    => OK
 +
    }
 +
    writeln(*a);
 +
    // deref: [] := [a] => OK
 +
    // => note how the dead value in `b` is ignored
 +
    //    this allows slightly more flexibility and avoids
 +
    //    a few false positives
 
}
 
}
 
</source>
 
</source>

Revision as of 13:45, 28 February 2015

Example for the inference algorithm

Dereferencing yields static scope

Applied to the function deadalnix used to demonstrate the rvalue/lvalue problem:

(1) foo() is @safe, making its param scoped:

void foo(scope int** a) {
    // no inference for `a` => self-owned
    // ("mystery scope" in your terms)
    // => SCOPE(a) := [a] (final)
    int** b;
    // => SCOPE(b) := [] (incomplete)
    b = a;
    // scope of `a` is fixed => do nothing
    int d;
    int* c;
    // => SCOPE(c) := [] (incomplete)
    c = &d;
    *b = c;
    // assignment from `c`:
    // => SCOPE(c) |= SCOPE(*b) = [] | [static] (final)
    // (dereferencing loses information => static)
    // ---------------------------------------------------
    // we now have:
    // SCOPE(a) = [a]
    // SCOPE(b) = []
    // SCOPE(c) = [static]
    // => all resolved
    // ---------------------------------------------------
    // => satisfiable, now let's check the assignments:

    int** b = a;        // []       := [a]         => OK
    int d;
    int* c = &d;        // [static] := [d]         => BAD
    *b = c;             // [static] := [static]    => OK
    // => invalid assignment
    // note how it even traces where the bad value comes from
}

(2) foo() is in a template, param scope gets inferred

void foo(T)(T** a) {
    // start with empty scope for params
    // => SCOPE(a) := [] (incomplete)
    T** b;
    // start with empty scope for locals
    // => SCOPE(b) := [] (incomplete)
    b = a;
    // only access to `a`:
    // => SCOPE(a) |= SCOPE(b)
    // => DEFER because SCOPE(b) is incomplete
    T d;
    T* c;
    // => SCOPE(c) = [] (incomplete)
    c = &d;
    *b = c;
    // assignment from `c`:
    // => SCOPE(c) |= SCOPE(*b) = [] | [static] = [static]
    // ---------------------------------------------------
    // we now have:
    // SCOPE(a) = []
    // SCOPE(b) = []
    // SCOPE(c) = [static]
    // unresolved:
    // SCOPE(a) |= SCOPE(b)
    // resolve:
    // SCOPE(a) := [] | [] = []
    // => all resolved
    // ---------------------------------------------------
    // => satisfiable, now let's check the assignments:

    int** b = a;        // []       := []         => OK
    int d;
    int* c = &d;        // [static] := [d]        => BAD
    *b = c;             // [static] := [static]   => OK
    // => invalid assignment
    // again, the culprit can be detected
}

(3) foo() takes unscoped pointer

void foo(int** a) {
    // no inference for `a` => static
    // => SCOPE(a) := [static] (final)
    int** b;
    // => SCOPE(b) := [] (incomplete)
    b = a;
    // scope of `a` is fixed => do nothing
    int d;
    int* c;
    // => SCOPE(c) := [] (incomplete)
    c = &d;
    *b = c;
    // assignment from `c`:
    // => SCOPE(c) |= SCOPE(*b) = [] | [static] (final)
    // ---------------------------------------------------
    // we now have:
    // SCOPE(a) = [static]
    // SCOPE(b) = []
    // SCOPE(c) = [static]
    // => all resolved
    // ---------------------------------------------------
    // => satisfiable, now let's check the assignments:

    int** b = a;        // []       := [static]    => OK
    int d;
    int* c = &d;        // [static] := [d]         => BAD
    *b = c;             // [static] := [static]    => OK
    // => invalid assignment
    // escape detection for locals works even without scope params
    // and in @system code
}

return inference

T[] findSubstring(T)(T[] haystack, T[] needle) {
    // find first occurrence of substring
    // naive implementation

    // => SCOPE(return)   := [return] (fixed)
    // [return] is a scope higher than all params
    // => SCOPE(haystack) := [] (incomplete)
    // => SCOPE(needle)   := [] (incomplete)

    for(int i = 0; i < haystack.length - needle.length; i++) {
        // haystack and needle are read here, but not assigned
        // => need large enough scope to be accessible at this point
        //    use the variables' lifetimes
        // => SCOPE(haystack) |= [haystack] = [haystack] (incomplete)
        // => SCOPE(needle)   |= [needle]   = [needle]   (incomplete)
        // (this is optional; instead, we could just assign them their own lifetimes)
        T[] sub;
        // => SCOPE(sub) := [] (incomplete)
        sub = haystack[i .. i + needle.length];
        // haystack and needle are read again; ignoring from now on
        // => SCOPE(haystack) |= SCOPE(sub)
        // => DEFER because SCOPE(sub) is incomplete
        if(sub == needle) {
            // sub is read here
            // => SCOPE(sub) |= [sub] = [sub] (final)
            return haystack[i .. $];
            // => SCOPE(haystack) |= SCOPE(return) = [haystack] | [return] = [return]
        }
    }
    return null;
    // nothing to do here, `null` has fixed static scope
    // ---------------------------------------------------
    // we now have:
    // SCOPE(haystack) = [return]
    // SCOPE(needle)   = [needle]
    // SCOPE(sub)      = [sub]
    // unresolved:
    // SCOPE(haystack) |= SCOPE(sub)
    // resolve:
    // SCOPE(haystack) := [return] | [sub] = [return]
    // => all resolved
    // ---------------------------------------------------
    // => satisfiable, now let's check the assignments:

    for(int i = 0; i < haystack.length - needle.length; i++) {
        T[] sub;
        sub = haystack[i .. i + needle.length];
        // [sub] := [return]    => OK
        if(sub == needle) {
            // equivalent to: if(opEquals(sub, needle))
            // let's assume `opEquals` takes both params by scope
            // sub:    [] := [sub]       => OK
            // needle: [] := [needle]    => OK
            return haystack[i .. $];
            // [return] := [return]    => OK
        }
    }
    return null;
    // [return] := [static]    => OK
}

// the inferred signature for T == immutable(char) is then
string findSubstring(scope string haystack return, scope string needle);

Multiple return params:

T chooseStringAtRandom(T)(T a, T b) {
    // => SCOPE(a) = [] (incomplete)
    // => SCOPE(b) = [] (incomplete)
    return random() % 2 == 0 ? a : b;
    // => SCOPE(a) |= [a] = [a]
    // => SCOPE(b) |= [b] = [b]
    // ?: operator affects both `a` and `b`
    // => SCOPE(a) |= SCOPE(return) = [a] | [return] = [return]
    // => SCOPE(b) |= SCOPE(return) = [b] | [return] = [return]
    // ---------------------------------------------------
    // we now have:
    // SCOPE(a) = [return]
    // SCOPE(b) = [return]
    // => all resolved
    // ---------------------------------------------------
    // => satisfiable, now let's check the assignments:

    return random() % 2 == 0 ? a : b;
    // RHS SCOPE(cond ? a : b) = MIN(SCOPE(a), SCOPE(b)) =
    //                         = MIN([return], [return]) = [return]
    // [return] := [return]    => OK
}

// the inferred signature for T == string is then
string chooseStringAtRandom(scope string a return, scope string b return);

Calling functions

string global_string;
void foo() {
    string[13] text = "Hello, world!";
    // => nothing, string[13] has no indirections
    string a;
    // => SCOPE(a) := [] (incomplete)
    a = findSubstring(text, "world");
    // equivalent to: ... findSubstring(text[], ...)
    // text[] is returned, but SCOPE(text[]) is fixed
    // => no inference
    global_string = findSubstring(text, "world");
    // ditto
    string[5] s1 = "Hello";
    string b;
    // => SCOPE(b) := [] (final)
    b = chooseStringAtRandom(s1, a);
    // SCOPE(s1[]) = [s1] (final)
    // `a` is read
    // => SCOPE(a) |= [a] = [] | [a] = [a] (incomplete)
    // `a` is returned and stored in `b`
    // => SCOPE(a) |= SCOPE(b) = [a] | [] = [a] (final)
    // ---------------------------------------------------
    // we now have:
    // SCOPE(a) = [a]
    // SCOPE(b) = []
    // => all resolved
    // ---------------------------------------------------
    // => satisfiable, now let's check the assignments:

    string[13] text = "Hello, world!";
    string a;
    a = findSubstring(text, "world");
    // equivalent to: ... findSubstring(text[], ...)
    // findSubstring takes both params as scope
    // text[]:  []  := [text]      => OK
    // "world": []  := [static]    => OK
    // findSubstring returns haystack
    // => equivalent to `a = text[]`
    // return:  [a] := [text]      => OK
    global_string = findSubstring(text, "world");
    // [static] := [text]    => BAD
    string[5] s1 = "Hello";
    string b;
    b = chooseStringAtRandom(s1, a);
    // [b] := MIN([s1], [a]) = [s1]    => // OK
    // ---------------------------------------------------
    // => invalid assignment to global_string
}

Unused stores are ignored

void foo() {
    int* a, b;
    // => SCOPE(a) = [] (incomplete)
    // => SCOPE(b) = [] (final)
    {
        int x;
        a = &x;
        b = &x;
    }
    writeln(*a);
    // as is read => make sure its scope is large enough
    // => SCOPE(a) |= [a] = [] | [a] = [a] (final)
    // ---------------------------------------------------
    // we now have:
    // SCOPE(a) = [a]
    // SCOPE(b) = []
    // => all resolved
    // ---------------------------------------------------
    // => satisfiable, now let's check the assignments:

    int* a, b;
    // default initialization: a = b = null
    // a: [a] := [static]    => OK
    // b: []  := [static]    => OK
    {
        int x;
        a = &x;    // [a] := [x]    => BAD
        b = &x;    // []  := [x]    => OK
    }
    writeln(*a);
    // deref: [] := [a] => OK
    // => note how the dead value in `b` is ignored
    //    this allows slightly more flexibility and avoids
    //    a few false positives
}