K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

Hey Daniel,

The current backend is focused on supporting symbolic execution, so the
called-out data-structures (eg. `Set`, `List`, and `Map`) are `kompile`d
specially to make reasoning with them more efficient. Specifically, choice 
keys
in a `Map` are not supported (`choice` meaning non-determinism from `_`), and
the rule `<a> ... _ |-> (0 => 1) ... </a>` isn't compiled how you expect.

One alternative way to accomplish this is a bit more "manually":

```k
module ISSUE-SYNTAX
 imports SET
 syntax K ::= "init" | "zerosToOne" | "#zerosToOne" "(" Set ")" | 
"##zerosToOne" "(" Int ")"
endmodule

module ISSUE
 import ISSUE-SYNTAX
 configuration <k> $PGM:K </k>
               <a> .Map </a>

 rule <k> init => zerosToOne ... </k>
      <a> .Map => 0 |-> 0  1 |-> 3  2 |-> 0 </a>

 // COLLECT KEYS IN MAP
 // -------------------
 rule <k> zerosToOne => #zerosToOne(keys(AMap)) ... </k>
      <a> AMap:Map </a>

 // SPLIT UP SET OF KEYS INTO INDIVIDUAL CHECKS
 // -------------------------------------------
 rule <k> #zerosToOne(.Set) => .K ... </k>
 rule <k> (. => ##zerosToOne(X)) ~> #zerosToOne((SetItem(X:Int) => .Set) 
XS:Set) ... </k>

 // FOR EACH INDIVIDUAL CHECK, IF THE VALUE IS 0, SET TO 1, ELSE LEAVE ALONE
 // ------------------------------------------------------------------------
 rule <k> ##zerosToOne(X:Int) => . ... </k>
      <a> ... (X |-> (0 => 1)) ... </a>

 rule <k> ##zerosToOne(X:Int) => . ... </k>
      <a> ... X |-> N:Int ... </a>
      requires N =/=Int 0
endmodule
```

This collects the keys in the map using `#zerosToOne(keys(AMap))`, then splits
the resulting set up into several individual map updates `##zerosToOne(key)`,
then for each one it updates the map appropriately.

Will this work for what you need?

Everett H.

On Mon, Mar 06, 2017 at 12:38:41PM +0000, Daniel Schnetzer Fava wrote:
> Hi,
> 
> I would like to encode a rule that replaces, for example, all Map values of 
> 0 by 1 (regardless of their key).  I suppose there are many ways of doing 
> this.  Perhaps one of them is something like:
> 
>   <a> ... _ |-> (0 => 1) ... </a>
> 
> that assume that <a> contains some map, for example: <a> AMap: Map </a>
> 
> 
> I've encoded such a rule, and what I've observed is that K matches on one 
> value of the map (apparently the first that was added), but does not match 
> the rest.  I feel like the rule should have applied to all 0 values.
> 
> Here is a full example:
> 
> $ cat issue.k
> module ISSUE-SYNTAX
>   syntax K ::= "init" | continue(Int)
> endmodule
> 
> module ISSUE
>   import ISSUE-SYNTAX
>   configuration <k> $PGM:K </k> <a> .Map </a>
> 
>   rule <k> init => continue(0) </k>
>        <a> AMap:Map => ((AMap[ 0 <- 0 ])[ 1 <- 0])[ 2 <- 0 ] </a> // A Map 
> of 0 to 0, 1 to 0, and 2 to 0
> 
>   rule <k> continue(C:Int => C +Int 1) </k>
>        <a> ... _ |-> (0 => 1) ... </a>  // Replace all values of 0 by 1
> endmodule
> 
> The program simply contains the string "init"
> 
> $ cat test.issue
> init
> 
> This is the output produced showing that the rule matches one of the values 
> in the Map, but not the others:
> 
> $ krun --debug test.issue | pprint
> <generatedTop>
>       <k> continue ( 1 ) </k>
>       <a> 0 |-> 1 1 |-> 0 2 |-> 0 </a>
> </generatedTop>
> 
> The output I was expecting is something more like:
> <generatedTop>
>       <k> continue ( 3 ) </k>
>       <a> 0 |-> 1 1 |-> 1 2 |-> 1 </a>
> </generatedTop>
> 
> Note that I am using git commit 35df078e85e83f23d1b45e7eee5481a8cb9e8939, 
> which I believe is the top of tree.
> 
> Could this be an issue?
> 
> Thank you,
> 
> Daniel Fava