Re: [Caja] Functional auditor for Cajita

David-Sarah Hopwood wrote:
> David-Sarah Hopwood wrote:
>> It would be possible to make the argument and result checks optional
>> depending on the function annotation: say, /*@pure*/ includes them but
>> /*@functional*/ doesn't. (The environment checks would be the same,
>> and both /*@pure*/ and /*@functional*/ would mark instances as
>> copacetic.)
>>
>> In that case, /*@pure*/ would imply unconditional determinism
>> (referential transparency), whereas /*@functional*/ would only imply
>> determinism for calls for which all arguments are copacetic.
> 
> In fact I'm wrong here, as shown by this example:
> 
>   /*@pure*/ function f() { return cajita.deepFreeze({}); }
> 
>   const a = f();
>   const b = f();
> 
>   /*@pure*/ function g(x) { return x === a; }
> 
>   g(a); // true
>   g(b); // false
> 
> Since a and b are observably different, either f or g must not
> be referentially transparent.
> 
> A Cajita that only exposed an egal operator, as defined in
> 
>   Henry Baker,
>   "Equal Rights for Functional Objects, or The More Things Change,
>    The More They Are the Same"
>   <http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.9999>
> 
> would solve this problem. (It might be difficult to tame away all
> indirect access to ===, though.)

A more lenient option is to prohibit access to === and !== only to
copacetic functions. So, the above code would be invalid because
g is annotated as @pure, therefore required to be copacetic.
This would transitively deny access to === and !== as long as no
tamed objects are incorrectly marked as being copacetic.
(The fact that some code has access to === and !== precludes the
optimizations I referred to in my previous post, but those optimizations
would not be available in an ECMAScript implementation anyway.)

@pure and @functional functions would still be able to use egal,
if its implementation were "deemed" copacetic (exempted from the
restriction on === and !==).

From now on, I'll rename copacetic to deep-frozen, since it is close
enough to the E concept that I don't think there will be any confusion.
(Bye bye, copacetic. We'll miss you.)
I'll also rename the @functional annotation to @deepFrozen.

I'll write out the differences between the auditing in E, Joe-E, and
my proposal for Cajita in a separate post. In the meantime, here is most
of the run-time support that could be used to implement deep-frozen
auditing in Cajita:


// Using <http://wiki.ecmascript.org/doku.php?id=strawman:weak_references>.
function makeWeakTable() { return new EphemeronTable(true); }

/**
 * An auditDeepFrozen entry has the value:
 *   false or a sour pumpkin, if the key is known not to be deepFrozen
 *   true or a tasty pumpkin, if the key is known to be deepFrozen.
 *
 * The objects traversed in a given checkDeepFrozen run are set
 * to a unique pumpkin object, which is used to detect loops.
 * A "tasty pumpkin" is an object with a 'tasty' field set to
 * true, indicating that its run succeeded. A "sour pumpkin" has
 * its 'tasty' field set to false. If a run fails, the entries
 * pointing to its pumpkin (which has no 'tasty' field) are left
 * in the table but are ignored, i.e. treated as equivalent to a
 * missing entry, on subsequent runs.
 */
/*const*/ var auditDeepFrozen = makeWeakTable();

/*const*/ var tastyPumpkin = Object.freeze({ tasty: true });
/*const*/ var sourPumpkin = Object.freeze({ tasty: false });

/**
 * A functionMarks entry has the value:
 *   'deepFrozen', if marked as @deepFrozen
 *   'pure',       if marked as @pure.
 */
/*const*/ var functionMarks = makeWeakTable();

/**
 * Check that obj satisfies the conditions to be deepFrozen, and throw
 * AuditError if not. Memoize any results for non-primitive objects in
 * the auditDeepFrozen table.
 */
function checkDeepFrozen(obj) {
  if (isPrimitive(obj)) return;

  /*const*/ var pumpkin = {};
  if (isDeepFrozen(obj, pumpkin)) {
    // Mark all visited objects that participated in a loop as deepFrozen.
    pumpkin.tasty = true;
    Object.freeze(pumpkin);
    return;
  }
  Object.freeze(pumpkin);
  throw new AuditError();
}

/**
 * Return true if obj is definitely deepFrozen, false if it definitely
 * isn't, and pumpkin if we encountered a loop.
 */
function isDeepFrozen(obj, pumpkin) {
  var t = auditDeepFrozen.get(obj);
  if (t) {
    /*const*/ var tasty = t.tasty;
    if (tasty !== undefined) return tasty;
    if (t === pumpkin) return t;
  }

  test: {
    // Function instances must be marked in order to be deepFrozen.
    if (typeof obj === 'function' && !functionMarks.get(obj))
      break test;

    // Mark that we are checking obj, to avoid infinite loops.
    // Progress depends on single-threadedness; multiple threads
    // could livelock by treading on each other's pumpkins.
    auditDeepFrozen.put(obj, pumpkin);

    t = isDeepFrozen(Object.getPrototypeOf(obj), pumpkin);
    var loopy = t === pumpkin;
    if (!t || !Object.isFrozen(obj)) break test;

    /*const*/ var ownprops = Object.getOwnPropertyNames(obj);
    for (var i = 0; i < ownprops.length; i++) {
      /*const*/ var prop = ownprops[i];
      /*const*/ var desc = Object.getOwnPropertyDescriptor(obj, prop);

      if ('value' in desc) {
        t = isDeepFrozen(desc.value, pumpkin);
        loopy = loopy || t === pumpkin;
        if (!t) break test;
      } else {
        t = isDeepFrozen(desc.get, pumpkin);
        loopy = loopy || t === pumpkin;

        // It would be sufficient to check that the setter is deepFrozen,
        // but a setter that doesn't actually set anything is misleading.
        if (!t || desc.set !== null) break test;
      }
    }

    // If the traversal from this object did not hit a loop, then we can
    // memoize it as deepFrozen even if the overall checkDeepFrozen run
    // fails.
    if (loopy) return pumpkin;
    auditDeepFrozen.put(obj, tastyPumpkin);
    return true;
  }

  // break test:
  auditDeepFrozen.put(obj, sourPumpkin);
  return false;
}

/**
 * Check that a chain of property accesses starting from obj, and
 * using property names given by subsequent arguments, is guaranteed
 * to give a constant result. No getters are invoked during the check.
 *
 * This can be used to relax the condition that all accesses to captured
 * variables of a deepFrozen function are deepFrozen. For instance,
 * if a @deepFrozen function uses foo only by accessing foo.bar.baz,
 * then rather than requiring foo to be deepFrozen, we can require
 * just that foo.bar.baz gives a constant result.
 * I.e. we verify that foo is statically const, and generate a call to
 * checkConstant(foo, 'bar', 'baz') for each scope in which foo
 * might be different.
 */
function checkConstant(obj /*, ...*/) {
  var i = 1;
  test: while (true) {
    if (i >= arguments.length) return;

    /*const*/ var t = auditDeepFrozen.get(obj);
    if (t && t.tasty) return;  // optimization

    /*const*/ var prop = arguments[i];

    var desc;
    try {
      desc = Object.getOwnPropertyDescriptor(obj, prop);
    } catch (e) {
      // getOwnPropertyDescriptor *should* only throw if Type(obj) is not
      // Object. However the ES5 spec doesn't explicitly say that
      // [[GetOwnProperty]] for a host object can't throw (even though
      // that would break stuff).

      if (isPrimitive(obj)) return;
      break test;
    }

    if (desc === undefined) {
      // If prop doesn't exist as an own-property, then the object must be
      // non-Extensible, and we continue using the object's prototype.
      // If the property doesn't exist in the prototype chain and all
      // objects in the chain are non-Extensible, then obj will eventually
      // be null, which is allowed by the primitive case above.

      if (Object.isExtensible(obj)) break test;
      obj = Object.getPrototypeOf(obj);
      continue;
    }

    // The property must be non-Configurable. If it is a data property,
    // it must also be non-Writable, and we continue checking that
    // subsequent property accesses on the value are constant. If it
    // is an accessor property, we conservatively require its getter
    // to be deepFrozen (note that the getter may be null).

    if (desc.configurable !== false) break test;
    if ('value' in desc) {
      if (desc.writable !== false) break test;
      obj = desc.value;
      i++;  // next access
      continue;
    } else {
      checkDeepFrozen(desc.get);

      // Since the getter is deepFrozen, there is no need to check
      // subsequent properties in the chain (which is lucky, because
      // we can't).
      return;
    }
  }

  // break test:
  auditDeepFrozen.put(obj, sourPumpkin);
  throw new AuditError();
}

function isPrimitive(obj) {
  if (obj == null) return true;  // null and undefined
  /*const*/ var t = typeof obj;
  return t === 'number' || t === 'string' || t === 'boolean';
}

/**
 * This would be called by the rewritten code that instantiates an
 * annotated function.
 */
function markFunc(mark, obj) {
  if (typeof obj !== 'function' || functionMarks.get(obj) !== undefined)
    throw new TypeError();

  Object.freeze(obj);
  functionMarks.put(obj, mark);
  checkDeepFrozen(obj);
}

-- 
David-Sarah Hopwood  ⚥  http://davidsarah.livejournal.com

_______________________________________________
e-lang mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/e-lang

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.12 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iF4EAREIAAYFAkshlnQACgkQWUc8YzyzqAfm9AEAirRy2t03jyEtp/mNkMHrn03I
sHC4S0kdwqst+mXXzHYA/3Mm9GgFQQnahS+53EhZZeS9bb/gyw/ePguoP5S6vjaY
=EtkN
-----END PGP SIGNATURE-----