K-user mailing list

[Daniel Schnetzer Fava <danielsf AT ifi.uio.no>]

Hi Everett,

Thanks for the proposed solution.  I understood it and I thought the rules 
were clever.  They illustrated the use of ~> quite well.

I still need to think a bit more about whether the solution will fit into the 
project I am working on.

On the mean time, I had a reaction and another example that I wanted to share:

> 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.


I am no expert in rewriting logic, but it sounds a bit scary.  The write-up 
of the semantics becomes less intuitive for the sake of making it run faster. 
 Seems like a fair trade-off, but I wonder whether it can lead to counter 
intuitive behavior.  Here is an example.  Its similar to the previous one, 
but this time with sets.  The rules are quite simple and have a straight 
forward intuition.  Yet, when we run this on krun, it doesn’t terminate.  
Instead, it prints messages like these until I kill the process:

(error "line 6 column 20: unknown sort 'IntSeq'")
(error "line 7 column 39: unknown function/constant smt_seq_elem")
(error "line 4 column 21: unknown sort 'IntSeq'")

$ cat issue.k
module ISSUE-SYNTAX
  syntax K ::= "init" | continue(Int)
endmodule

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

  rule <k> init => continue(0) </k>
       <a> ASet:Set => SetItem( ListItem(0) ListItem(0) ) SetItem( 
ListItem(1) ListItem(0)) SetItem(ListItem(2) ListItem(0)) </a>

  rule <k> continue(C:Int => C +Int 1) </k> // Replace me
       <a> ... SetItem( ListItem(_) ListItem(0 => 1) ) ... </a>

endmodule

The example above starts a set with items (0 0) (1 0) and (2 0), and has a 
rewrite rule to transform them into (0 1) (1 1) and (2 1).
There is a finite number of elements in the set. So I would expect K to 
terminate.

When I make the following small modification to the program, I see what is 
happening:

replace line:
  rule <k> continue(C:Int => C +Int 1) </k>  // Replace me
by:
  rule <k> continue(C:Int) => . </k>

and we get:

$ cat test.issue
init
$ krun test.issue
<generatedTop> <k> . </k> <a> SetItem ( ListItem ( 2 ) ListItem ( 0 ) ) 
SetItem ( ListItem ( V0 ) ListItem ( 1 ) ) SetItem ( ListItem ( 0 ) ListItem 
( 0 ) ) SetItem ( ListItem ( 1 ) ListItem ( 0 ) ) </a> </generatedTop>
[Warning] Critical: failed to translate smtlib expression:
(declare-sort K)
(declare-fun R__35 () K)
(declare-fun _92 () K)
(declare-fun _93 () K)
(declare-fun _94 () Bool)
(declare-fun _95 () IntSeq)
(assert (and (= _92 (smt_seq_elem R__35)) (= _93 (smt_seq_elem 0)) (= _94 
true)
(= smt_seq_nil _95)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort K)
(declare-fun _100 () K)
(declare-fun _104 () Bool)
(declare-fun _102 () IntSeq)
(declare-fun _101 () K)
(declare-fun _103 () K)
(assert (and (= _101 (smt_seq_elem 0)) (= smt_seq_nil _102) (= _103
(smt_seq_elem _100)) (= _104 true)))

What happens is that K adds a new set item everytime it goes through the 
"continue” rule as opposed to changing the existing items.  So the program 
doesn't terminate.
The behavior seems quite counter intuitive.  I wonder if there is something 
you guys could do different...

In either case, thanks again for your help!

Daniel Fava


> On 6 Mar 2017, at 20:58, Everett Hildenbrandt 
> <hildenb2 AT illinois.edu>
>  wrote:
> 
> 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