Require variables be scoped from program/procedure allocators

[agle]

Introduce the type Var.generator which is a pure function of a ID.generator, and returned by procedure and program to create variables. Hides the direct constructor of Var.t.

• Helps eliminate the class of bug where an expression refers to a variable that is not declared in a procedure or program. Frankly it doesn't do a very good job of this so far.
• Makes program's declaration list more consistent in using ID.t for all identifiers rather than strings for some things and IDs for others---everything now has a scope, the ID of a type declaration and the type itself now match, similarly procedures and variables.
• Variables descendant from different generators can be made automatically non-equal now (currently I think they are only unequal if they are not both local or global). I'm unsure if this is desirable, generally it would be a bug to mix local scopes in the same procedure and doing so should raise questions.
• Systematically enforce sigils at the variable allocator level
• Refactor boogie backend prepass to generate declarations for bitvec intrinsics which are used in function application expressions - makes the backend part simpler/more consistent just naively translating the function calls.
• Simplifies the frontend (loadir.ml) slightly by factoring out the variable generation/scoping/lookup code and removing fallbacks for undeclared globals.

Todo:

• Still needs a thorough read of the diff and cleanup of the APIs
• Make sure the updated tests are sensible
• The smt translation for the strongest post was doing something odd--chucking all the local variables in the same smt problem; does this make sense?
• Add a simplified create function (Var.t, 'e) Procedure.t that uses a variable generator; the generic one is a nightmare for the formal parameter lists having to not constrain the var type to Var.t.

Nasty things:

• procedure is generic in variable type, this means we cannot just store a Var.generator in the procedure and must construct it based on an ID generator. (Although a lot of procedures function take and return (Var.t, BasilExpr.t) Procedure.t). This decision means we cannot intern variables, only IDs, though I don't think theres a huge amount of value in that. I wonder whether its worth making variables just an ID in right expressions (as the expression itself stores type now) and add a left expression type which is essentially (Var.t , Type.t).

[agle]

This happens just by declaring x, y, z even on main, not sure what is happening.

[katrinafyi]

This is just initial thoughts. The record should show that I really don't like the consequence of having to inject the ID generator everywhere. I understand the goal and I support hiding the Var constructor, but it's unpleasant to need the generator just to even mention a variable.

I'm not convinced that this is the best solution to the problem. For example, I think that there's probably a small enough set of variables which need summoning "out-of-thin-air" that it should be possible to make a big variant of all of those and keep them wholly distinct from the ID generator system - something like Aslp_lexpr.t but for all of bincaml.

But that ship has sailed so it is what it is. Just let me know what I should focus on when reviewing and how I should review it.

About the nasty thing, I am also not sure what it means. Var.generator is a concrete type so you should always be able to store it. It's just that you won't be able to put the generated vars back into the procedure. Could you work around this be having procedure store a function Var.t -> 'v?

[agle]

This is just initial thoughts. The record should show that I really don't like the consequence of having to inject the ID generator everywhere. I understand the goal and I support hiding the Var constructor, but it's unpleasant to need the generator just to even mention a variable.

I'm not convinced that this is the best solution to the problem. For example, I think that there's probably a small enough set of variables which need summoning "out-of-thin-air" that it should be possible to make a big variant of all of those and keep them wholly distinct from the ID generator system - something like Aslp_lexpr.t but for all of bincaml.

This misunderstands the goal, the goal is to create intentional friction for summoning a variable out of thin air by name as this is generally unsafe (i) because it risks creating new variables that accidentally shadow existing variables and (ii) because it is often involved in code which aims to project specific semantics onto variables with specific names which conflicts with the IR's basic semantics. I don't see why you would want to mention a specific variable with a given name otherwise (rather than getting a variable value from a static analysis) --- for any arbitrary bincaml IR program you might get as input, which might not even define that variable. Doing so generally relies on baked in assumptions which need to be concretely encoded in the IR semantics somehow.

For variables that have a specific meaning to the program, e.g. stack pointers, program counters, I would support some form of intrinsic variable which gives these a special semantics in the IR. Other cases usually correspond to a program transform that should genuinely exist in a variable generator scope.