search

gsdlab / clafer

Clafer is a lightweight modeling language
http://clafer.org
MIT License
45 stars 13 forks source link

Unique names #40

Closed mantkiew closed 11 years ago

mantkiew commented 11 years ago

Implementation for i275.

Implemented UID by fully qualified lookup.

JLiangWaterloo commented 11 years ago

The code looks fine. I think it's okay to merge unless there were some changes you wanted to make based on our discussion this morning. In particular, bound variables in quantifiers are not necessarily unique in the IR.

For example:

X -> int
[all x : X | some x : X | x.ref = 3]

The two "x" variables in the IR have the same identifier. The only way to see which "x" in "x.ref" is referring to is to do some form of scoping everytime. From a security standpoint, you can use this to refer to unintended variables/keywords in the backends so this is very bad design.

For example:

X -> int
[all extends : X | some extends : X | extends.ref = 3]

compiles to in Alloy

one sig c1_X
{ ref : one Int }

fact { all disj x, y : c1_X | (x.@ref) != (y.@ref) }
fact { all  extends : c1_X | some  extends : c1_X | (extends.@ref) = 3 }

Which will crash Alloy because "extends" is a reserved keyword. It is probably even worse in the Choco backend since it executes (somewhat) arbitrary javascript so the current method introduces a surface for code injection.

mantkiew commented 11 years ago

Jimmy, that's a great point about local declarations in quantified expressions. I was not aware of that. Of course, the unique IDs should be generated for these as well.