kframework/c-semantics — pull request #8 by liyili2 (2014-05-31 22:56:07+00:00)
Title: fix processGoto list problem

I change the following rules:

```

// as long as there are entries in the actual block history that differ
// from the target block history, we need to pop
rule [processGoto-pop-differing-1]:
(. => popBlock)
~> processGoto(gotoObject(
_:Int, TargetBlockHistory:List, _, _, _))
...

ListItem(BlockNum:Int) _:List

when notBool BlockNum in TargetBlockHistory
[structural]

// same
rule [processGoto-pop-differing-2]:
(. => popBlock)
~> processGoto(gotoObject(_:Int,
_:List ListItem(BlockNum:Int)
TargetBlockHistory:List, _, _, _))
...

ListItem(BlockNum:Int) ActualHistory:List

when TargetBlockHistory =/=List ActualHistory
[structural]

// once we share a history, we start to push
rule processGoto(gotoObject(TargetDepth:Int,
(Prefix:List ListItem(_:Int) ActualHistory:List),
K:K, LoopStack:List, DeclStack:List))
=> addVariablesForBlock(CurrentBlock, DeclStack)
~> processGotoDown(gotoObject(TargetDepth,
(Prefix ListItem(CurrentBlock) ActualHistory),
K, LoopStack, DeclStack))
...
ActualDepth:Int

ListItem(CurrentBlock:Int) ActualHistory:List

when ActualDepth +Int 1 =/=Int TargetDepth
[structural]
```

To this set:
```
syntax List ::= searchInGotoObjectList(Int,List,List,List,List) [function]
| resultInGotoObjectList(List,List)

rule searchInGotoObjectList(BlockNum:Int,.List,Prefix:List,Actual:List,Store:List)
=> resultInGotoObjectList(.List,Store)
rule searchInGotoObjectList(BlockNum:Int, ListItem(Current:Int) BlockHistory:List,
Prefix:List,Actual:List,Store:List)
=> resultInGotoObjectList(ListItem(BlockNum),Prefix)
when BlockHistory ==List Actual
rule searchInGotoObjectList(BlockNum:Int,ListItem(Current:Int) BlockHistory:List,
Prefix:List,Actual:List,Store:List)
=> searchInGotoObjectList(BlockNum,BlockHistory,
Prefix ListItem(Current),Actual,Store)
when BlockHistory =/=List Actual orBool BlockNum =/=Int Current

rule processGoto(gotoObject(SIntDepth:Int,
((ListItem(CurrentBlock:Int) BlockHistory:List)
=> searchInGotoObjectList(BlockNum,
ListItem(CurrentBlock) BlockHistory,.List,
ActualHistory,ListItem(CurrentBlock) BlockHistory)),
_, _, _))
...
Depth:Int
ListItem(BlockNum:Int) ActualHistory:List
when (SIntDepth =/=Int Depth
orBool (ListItem(CurrentBlock) BlockHistory)
=/=List (ListItem(BlockNum) ActualHistory))
andBool (SIntDepth =/=Int Depth +Int 1
orBool BlockHistory =/=List (ListItem(BlockNum) ActualHistory))
[structural]

// as long as there are entries in the actual block history that differ
// from the target block history, we need to pop
rule [processGoto-pop-differing]:
(. => popBlock)
~> processGoto(gotoObject(_,
(resultInGotoObjectList(.List, Store:List)
=> Store), _, _, _))
...
[structural]

// once we share a history, we start to push
rule processGoto(gotoObject(TargetDepth:Int,
resultInGotoObjectList(ListItem(_:Int),Prefix:List),
K:K, LoopStack:List, DeclStack:List))
=> addVariablesForBlock(CurrentBlock, DeclStack)
~> processGotoDown(gotoObject(TargetDepth,
(Prefix ListItem(CurrentBlock) ActualHistory),
K, LoopStack, DeclStack))
...
ActualDepth:Int

ListItem(CurrentBlock:Int) ActualHistory:List

when ActualDepth +Int 1 =/=Int TargetDepth
[structural]

```

I am not sure if it is correct. I wonder if you think the original rules have non-determinism, such as:
```
// same
rule [processGoto-pop-differing-2]:
(. => popBlock)
~> processGoto(gotoObject(_:Int,
_:List ListItem(BlockNum:Int)
TargetBlockHistory:List, _, _, _))
...

ListItem(BlockNum:Int) ActualHistory:List

when TargetBlockHistory =/=List ActualHistory
[structural]

// once we share a history, we start to push
rule processGoto(gotoObject(TargetDepth:Int,
(Prefix:List ListItem(_:Int) ActualHistory:List),
K:K, LoopStack:List, DeclStack:List))
=> addVariablesForBlock(CurrentBlock, DeclStack)
~> processGotoDown(gotoObject(TargetDepth,
(Prefix ListItem(CurrentBlock) ActualHistory),
K, LoopStack, DeclStack))
...
ActualDepth:Int

ListItem(CurrentBlock:Int) ActualHistory:List

when ActualDepth +Int 1 =/=Int TargetDepth
[structural]
```