Global variable initialization

[panagosg7]

This addresses #65 and adds support for tests like:

https://github.com/UCSD-PL/RefScript/blob/ssajoin/tests/pos/scope/init-04.ts https://github.com/UCSD-PL/RefScript/blob/ssajoin/tests/pos/scope/init-05.ts

https://github.com/UCSD-PL/RefScript/blob/ssajoin/tests/neg/scope/init-05.ts

New additions:

• The notions of Initialization, which is now used in all SSA, TC and LQ, and refers to the state of WriteGlobal variables. There are two cases: Initialized and Uninitialized and the modifier propagates locally as a "must" fact:

var r; // global
if (...) { r = 1; }

Then r is conservatively considered uninitialized in the end.

• Variables that are still int he Uninitialized state the type used at USES is the "un-Kvared" type enhanced with a " + TUndef" -- a type system embedding of the fact that the variable "may" be undefined. So envFinTy gets two flavors, depending on whether we are writing to or reading an uninitialized variable.
• Every sight that initializes a global variable gets a new K-var. (I tried using the same K-var, but I was getting unsoundness -- which I was having trouble debugging). At join points the same trick with local SSAed variables is used. This means that we need to keep track of global-phi vars (this is done separately -but alongside- local var SSA tracking).
• Assigning to an Uninitialized global variable changes it's state to Initialized-duh-
• Ambient variables (those declared elsewhere and just imported) are considered Initialized. So a trick to avoid having uninitialized globs for which we don't want to give an initial value is to consider them as ambient vars (by prefixing their declaration with declared).

[ranjitjhala]

Nice! Assuming that all tests pass?

[panagosg7]

Yes. All regression tests pass. Haven't checked d3 yet.

[ranjitjhala]

Did that todo/createElt also work btw?

On Oct 15, 2014, at 7:42 AM, Panagiotis Vekris notifications@github.com wrote:

Yes. All regression tests pass. Haven't checked d3 yet.

— Reply to this email directly or view it on GitHub.

[panagosg7]

There's a classes/createElts.

That one works.

[panagosg7]

I'm afraid I haven't checked the fb/ folder. (It's not in the regression script)

[ranjitjhala]

Thanks Panos!

[ranjitjhala]

Added the other folder and merged the pr thanks!

On Oct 15, 2014, at 8:13 AM, Panagiotis Vekris notifications@github.com wrote:

I'm afraid I haven't checked the fb/ folder. (It's not in the regression script)

— Reply to this email directly or view it on GitHub.