String analysis -- Let's take a review
Hey, I think I have pretty good idea how the other works deal with string analysis. Let's take a brief review:
For the same example:
x = “a”; while (cond) do x = “0“ + x; x = x + “1”; print x;
We are expected to get {0^na1^n | n>=0}.
Statically analyze the program and determine a context-free grammar G which represents the values of a variable, x at the hot spot.
So the G is equivalent to the reference grammar: S -> "a" | "0" S "1"
The problem of the research:
Checking a context-free grammar is included in antoher context-free grammar is "undecidable".
Regular expresssion approximation: Moler
CFG Regular expression X0 -> "a" X0 -> "a" X1 -> X0\|X3 X1 -> X0 X2\|X3 X2 -> "0" X1 X3 -> "0"X3 \| eps X3 -> X2"1" X2 -> "1"X2 \| eps X4-> X1 X4 -> X1
The string values represented by RG include the string values represented by the refernece grammar.
The Shortcoming: Not clear how to deal with other string ops! print replace("00", "0",x)] at the end of the example, there will be X4->X1
Context-free: Minamide
CFG Regular grammar transformed from reference grammar X0 -> "a" S0 -> "a" X1 -> X0\|X3 S1 -> "0" S0 "1" X2 -> "0" X1 S2 -> "0"S1 "1" X3 -> X2"1" … X4-> X1 Si -> "0" Si-1 "1"
Advantage: Improvement in dealing with string operators. For example, the replace operation, its image can be mapped under transdurcer.
Abstract interpretation
(1) A string value is abstracted as a "regular string" which is the same as regular expression except that a consecutive repetition is not allowed, i.e. 01 => {0,1}* (2) Abstract interpretation of a program on the abstract domain of regular strings.
So the walk through of the example using this approach is: a -- a -- 0a1
a -- a widening 0a1 = 0\*a1\* --00\*a1\*1
a -- 0\*a1\* widening 00\*a1\*1 = 0\*a1\* -- 00\*a1\*1
fixed point reached: 0\*a1\*
The last result include the string values represented by the refernce gramamr.
Abstract parsing & Analysis
to be continued...
