define harden rules using escape analysis?

[dckc]

I seem to recall some difficulty figuring out static rules for harden() that weren't too onerous.

After last night's exploration (#34) the idea of using escape analysis to define when harden() is required popped into my head.

Here's hoping for time to explore / explain further...

src/compiler/escape-analysis.cc - v8/v8 - Git at Google
Escape Analysis in V8 with Tobias Tebbi - YouTube
Escape-Analysis-in-V8.pdf

Go: Introduction to the Escape Analysis | by Vincent Blanchon | A Journey With Go | Medium

compilers - What data-structure is best suited for escape analysis? - Computer Science Stack Exchange

[erights]

I would love to see this!

[dckc]

reportedly...

Babel does escape analysis to detemine if there is actually a functional difference between the way var and let is used
-- javascript - Does ES6 `let` and `const` only work in compile time when compiled with babel? - Stack Overflow

should be in https://github.com/babel/babel/tree/main/packages/babel-plugin-transform-block-scoping somewhere...

p.s. oh my. let's hope we don't have to go there.

memory.ts does escape analysis, according to its readme. The code looks more reasonable, though I'm not sure which part of it is escape analysis.

[dckc]

I just re-discovered...

DoctorJS is based on Dimitris Vardoulakis‘s work this summer implementing CFA2 for JavaScript at Mozilla. -- Static Analysis FTW – Brendan Eich 2010

The DoctorJS link is dead (I haven't tried to find it elsewhere yet) but CFA2 looks interesting:

We describe CFA2, the first flow analysis with precise call/return matching in the presence of higher-order functions and tail calls.

• CFA2: a Context-Free Approach to Control-Flow Analysis Dimitrios Vardoulakis and Olin Shivers 2010

[dckc]

It occurred to me to add "coq" to my search terms for literature review of escape analysis; I haven't read these yet, but they look interesting:

• 2009: A CERTIFIED DATA RACE ANALYSIS FOR A JAVA-LIKE LANGUAGE
  • escape.v
• 2003: (18) Escape analysis for Java TM
• 2000: (18) Fast Escape Analysis and Stack Allocation for Object-Based Programs.
• 1998: Escape analysis | Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

[dckc]

bingo!

II. B. Type Analysis
JSTAR performs a type analysis with flow-sensitivity and type-sensitivity for arguments.
-- JSTAR: JavaScript Specification Type Analyzer using Refinement

[dckc]

@gibson042 presented some work on tsc extensions for static analysis of comparisons (to be sure our branded time stuff is used correctly everywhere). I asked about using a similar approach for checking correct usage of harden().

@michaelfig suggested that it's largely orthogonal to types, except that the never type might do control-flow-analysis in a way that could be relevant.

@gibson042 noted a tsc extension support library that enables advanced queries that might help too.

[dckc]

@Jake-Gillberg, you asked about ways to dig into the Agoric platform. This would be a fantastic one.

I think the rule that we're trying to enforce with static analysis is stated canonically in https://github.com/endojs/Jessie#must-freeze-api-surface-before-use :

To enable sound static reasoning, in Jessie all objects made by literal expressions (object literals, array literals, the many forms of function literals) must be tamper-proofed with harden before they can be aliased or escape from their static context of origin. Thus, direct property mutation can only be used to prepare an object for release. Use of harden then marks the object as being ready for use by its clients, who are thereby unable to mutate its properties. During an object's initialization phase, due to the lack of aliasing, each mutation can be reasoned about as-if it replaces the object in place with a derived object holding the new property.

[Jake-Gillberg]

collecting some links:

this thread proposes a "imperfect but worthwhile" linting rule that could probably be added to the jessie es-lint extension. i wonder if it got implemented - https://github.com/Agoric/agoric-sdk/pull/4553/files#r806450281

another thread on how harden should be used - Agoric/agoric-sdk#7585 (comment)

https://www.npmjs.com/package/@jessie.js/eslint-plugin - the jessie es-lint plugin doesn't seem to have a home on github?

hmm, this might be useful? https://codeql.github.com/docs/codeql-language-guides/analyzing-data-flow-in-javascript-and-typescript/#source-nodes

[dckc]

https://www.npmjs.com/package/@jessie.js/eslint-plugin - the jessie es-lint plugin doesn't seem to have a home on github?

oops... missing link. But the source is https://github.com/endojs/Jessie/tree/main/packages/eslint-plugin