K-user mailing list

[Daniele Filaretti <dfilaretti AT gmail.com>]

Brandon, 
thanks for your reply.

On 8 Jul 2014, at 17:15, Moore, Brandon Michael 
<bmmoore AT illinois.edu>
 wrote:

> You can define a new kind of item to put in the K cell to hold and use the 
> result, like this:
> 
>  rule [assign-create]:
>             <k> X = V:Int; => do_alloc(X
>            
> alloc(Bag(<k>KRest</k><env>M</env><store>S</store><nextAttr>I</nextAddr>),V)
>  KRest </k>
>             <env>M</env>
>             <store>S</store>
>             <nextAddr>I</nextAddr>
>         when notBool (X in keys(M))
> 
> (I changed "I" to "V" in the assignment, assuming you didn't mean the rule 
> to apply only when you were asigning a value that happened to match 
> nextAddr).
> 
> then you give do_alloc semantics with a rule like
>  rule [do-alloc]:
>             <k> do_alloc(X,Loc,V) => . ...</k>
>             <env>M => M[Loc/X]</env>
>             <store>... . => Loc |-> V ...</store>
>             <nextAddr> I => I+Int 1 </nextAddr>

I’m playing with the solution you suggested and it works (and yes, there were 
a few typos in my rules, sorry). I modified it a bit so that I also don’t 
need to name every single cell (since if/when moving to a real-world language 
there will be lot more cells!):

     rule [assign-create]:
          <T>
              <k> X = I:Int; => do_alloc(
                      X, 
                      alloc(<T> <k> X = I; </k> <env> M </env> BRest </T>),
                      I) ... </k> 
              <env> M:Map </env>
              BRest:Bag
          </T>
          when notBool (X in keys(M))

This actually achieves the goal. However... 

> We've thought a little bit about whether there is some way to give rules 
> read-only access to the whole configuration (or maybe cell completion style 
> access to cells near the call?), but don't have any concrete design or 
> plans for it.

I would be in favour of allowing rules to grab the whole configuration (as 
you said you discussed it before but still have no plans for it). I cannot 
remember exactly when/why, but I had a similar need in the past. I guess - 
provided it doesn’t break other things - that might be a useful feature. 

> Maybe you could say a little more about how your alloc works, and which 
> information it needs.

I’m just experimenting with the ideas in the Abstracting Abstract Machines 
paper (http://matt.might.net/papers/vanhorn2010abstract.pdf). 

The main idea is that (after recursion is removed from the state definition 
by refactoring the machine as shown in the paper) one can obtain a static 
analysis by essentially bounding the store, allowing locations to hold sets 
of values and allowing non-deterministic choices (e.g. for variable lookup).

In this setting, the particular choice of allocation function and set of 
addresses determines the kind of analysis. For example, if the set of 
addresses is Int and the allocation function returns a fresh one every time, 
we get our initial language (and the allocation function is equivalent to K’s 
builtin “fresh”). But one can also choose to use variable names as addresses, 
or any arbitrary set. (see e.g. the examples on the paper). 

So I guess that in the most general case the “alloc” function will need 
access to the whole configuration. I don’t have very complicated allocation 
functions in mind right now,  just wanted to set-up things in a general way.

Regards,

Daniele


> Brandon
> ________________________________________
> From: 
> k-user-bounces AT cs.uiuc.edu
>  
> [k-user-bounces AT cs.uiuc.edu]
>  on behalf of Daniele Filaretti 
> [dfilaretti AT gmail.com]
> Sent: Tuesday, July 08, 2014 10:30 AM
> To: 
> k-user AT cs.uiuc.edu
> Subject: [K-user] matching entire configuration while also matching its 
> components
> 
> Hi All,
> little technical question, in an IMP++ setting (actually only IMP, but with 
> environment + store).
> 
> The following is a variable assignment rule that, in case the variable 
> doesn’t exists, it creates it. In order to do this, it does the standard 
> things - adding an entry in the environment and in the store, using a fresh 
> allocated address.
> 
> However, I’m not using K’s builtin “fresh” predicate but I’d like to use my 
> own allocation function “alloc” which takes the whole configuration as an 
> input:
> 
>  rule [assign-create]:
>             <k> X = I:Int; => . ... </k>
>             <env> M:Map => M[alloc(State)/X] </env>
>             <store> ... . => alloc(State) |-> I ... </store>
>             <nextAddr> I:Int => I +Int 1 </nextAddr>)
>         when notBool (X in keys(M))
> 
> As you can see, I use “alloc(State)”, where I would like “State” to match 
> the entire configuration. Is that even possible?
> I’ve tried with
> 
>  rule [assign-create]:
>             State:Bag(
>                        <k> X = I:Int; => . ... </k>
>                        <env> M:Map => M[alloc(State)/X] </env>
>                        <store> ... . => alloc(State) |-> I ... </store>
>                        <nextAddr> I:Int => I +Int 1 </nextAddr>)
>                )
>         when notBool (X in keys(M))
> 
> but in this case “State” matches the empty bag (I guess) as it’s parsed as 
> (Config1 Config2). Is there a way to match entire configuration (simply 
> “give it a name”) and at the same time, match part of its content - all in 
> one rule?
> 
> Thank you very much!
> 
> Regards,
> 
> Daniele
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user