K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

Hey Daniel,

Sorry for the late reply.

The core problem here is that general matching modulo axioms is not supported.

The rule:

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

gets `kompile`d to something like:

```k
rule <k> continue(C:Int) => continue(C +Int 1) </k>
     <a> A => SetItem( ListItem(X) ListItem(1) ) A' </a>
     requires
                 A' ==K A -Set SetItem( ListItem(X) ListItem(0) )
         andBool (ListItem(X) ListItem(0)) in A
```

So the matching is delegated to a `requires` clause, which then calls z3 (the
SMT solver we use) to check feasibility. With proper associative-commutative
pattern matching, the compilation step wouldn't be necessary and the SMT 
solver
wouldn't be invoked.

Because there isn't general support for theory of Sets in z3, we have to 
encode
queries about Set satisfiability as a query of arrays. That encoding is not
working in your case, which outputs the errors you see.

So in general, I wouldn't lean too heavily on matching modulo structural 
axioms
(like assoc-comm), as the current implementation of K will turn that into a
query to z3, which may or may not work as anticipated.

Everett H.

On Tue, Mar 07, 2017 at 01:05:39PM +0000, Daniel Schnetzer Fava wrote:
> 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
>