-
Notifications
You must be signed in to change notification settings - Fork 0
Builtins
- summary Design for Builtins
Just use the "builtin" attribute to KTokenSorts/sorts and to KLabels/productions, telling what builtin types or operations these are linked to. When kompiling things to backends, these tokens and labels are statically replaced by their corresponding builtin values and operations called on corresponding arguments. If that is not possible to be done statically, then at this stage we can simply reject the K definition. Later we will improve on this by providing constructors and destructors for builtin datatypes.
To make the transition to different backends simple and uniform, the K tool will probably export an "interface for builtins", consisting of builtin type names and builtin operation names. The user of K will only refer to these names provided by the interface when hooking elements to builtins, but each backend added to the tool will need its own mechanism to implement the interface in its own way. From now on, when I say "builtin" type or operation I mean its name provided by the interface, not its implementation in the backend. The linking of the backend to the interface can be designed when we are done with the user interface.
You may also need to refer to the syntax of KAST and Kore: http://code.google.com/p/k-framework/wiki/KastAndKore
For the syntax of sorts in the concrete syntax I would prefer some notation as simple as the one below:
syntax Sort1 ::= Token{...} [builtin(BuiltinSort1)]
...
syntax SortN ::= Token{...} [builtin(BuiltinSortN)]where BuiltinSortI are builtin types corresponding to the builtin values.
When converted to Kore, or if one prefers to write definitions directly in Kore, then the above become:
syntax KTokenSort ::= "Sort1" [builtin(BuiltinSort1)] ... syntax KTokenSort ::= "SortN" [builtin(BuiltinSortN)]
Now each token of the form #token("whatever",SortI) will be converted by kompile or krun into the specific backend value corresponding to "whatever".
For attaching builtin functions to productions or KLabels, I'd prefer something which notationally is equally simple (I only show the Kore version; the builtin attribute stays exactly the same when we work with concrete syntax):
syntax KLabel ::= "myKLabel1" [builtin(BuiltinOperation1)] ... syntax KLabel ::= "myKLabelN" [builtin(BuiltinOperationN)]
where BuiltinOperationI are builtin operation names (as given by the interface to the builtins). The particular way builtin element names are linked to backend-specific elements is irrelevant here (and will be designed later). However, one thing to keep in mind is that it is the user's responsibility to only pass "expected" K terms to the KLabel constants that are linked to library operations, because the backend is free to "pass" K1 and K2 that appear in a term '_+MyInt_(K1,K2) immediately to the library; if the library crashes then so does krun.
Each backend should provide support for two operations:
1) Converting KToken terms corresponding to builtin sort BuiltinSortN into its own internal values of its internal type of choice associated to BuiltinSortN; and
2) The reverse, that is, to take internal values into KToken terms.
The backend is free to choose whatever semantics it wants for the builtins. We are not going to check any semantic consistency for the builtins (at least not at this stage).
For example we could have:
syntax KTokenSort ::= "Int" [builtin(ArbitraryPrecisionInteger)]
which in Maude would create the operations:
op KToken2ArbitraryPrecisionInteger : KToken -> #Int . op ArbitraryPrecisionInteger2KToken : #Int -> KToken .
and in Java would create:
BigInteger KItem2ArbitraryPrecisionInteger(Term k) KToken ArbitraryPrecisionInteger2KItem(BigInteger b)
and in Coq might create something having to do with sort Z.
The exact way we map the builtin sort in the interface (Int here) to the backend type (#Int in Maude, BigInteger in Java here) is something we still need to design.
The two operations above will need to be called by krun when going from KAST/KIL to corresponding structures in the backend when generating tasks for the backend, and respectively when taking the results produced by the backend and putting them back into KAST/KIL for further uses (debugging, search, displaying, etc.).
As an optimization, to avoid converting values back-and-forth to tokens when checking sort membership side-conditions to rules, the builtins' interface will probably also include builtin membership functions/predicates of the form isBuiltinSortI, which will be implemented by each backend appropriately. Then the membership predicates isSortI can be kompiled to make internal use of isBuiltinSortI in the backend.
To see why the above works, let me dwell a bit into the theory of builtins. Until now, we tended to assume that a "builtin domain" is an algebra that comes with a sort, values of that sort, and operations on those values. While this is OK for starters, the situation is more complex. For example, we want maps, sets, lists, etc., all over any domains, to also be builtins. Thus, we need to take a broader view of builtins. First, we should regard all builtins together, not separately, because they are inter-related; for example, "_ >Int _" takes integer values and returns Boolean values, or maps may be defined from Int to Strings, or multisets can contain maps, etc. Here is a simple and uniform way to look at builtins: as an unsorted algebra over K terms. That is, a set of specific values (possibly grouped in different "sorts" and injected into K by means of the #token construct), plus a set of operations over K terms that return K terms. Note the generic "K terms" above, as opposed to "its specific values"! It is the user's full responsibility to make sure that appropriate K terms are being passed to the K labels that are linked to library operations.
{{{ syntax MyInt ::= Token{"[1-9][0-9]*"} [builtin(MyBuiltinInteger)] syntax MyInt ::= MyInt "+MyInt" MyInt [builtin(MyBuiltinIntegerPlus)] syntax Bool ::= MyInt "<MyInt" MyInt [builtin(MyBuiltinIntegerLeq)] ... }}}
Then, kompile takes a rule of the form (I write it in Kore, to avoid syntactic confusion, but I exclude the rest of the configuration):
rule '_<_(K1,K2) => '_<MyInt_(K1,K2) when isMyInt(K1) andBool isMyInt(K2)
and converts it into its internal representation of a rule whose LHS is its K term representation of the LHS of the rule above, whose side condition is its internal representation of the two memberships, and whose RHS is the call MyBuiltinIntegerLeq(K1,K2), where by K1 and K2 here I assume the internal representation of K1 and K2, which I assume it is exactly the builtin values corresponding to these. If this optimization is not possible in some backends, then we can assume corresponding getters, for example
{{{ MyBuiltinInteger getMyBuiltinInteger(BackendInternalKterm K) }}}
But then we may also need reverse functions, which wrap builtin values into the internal representation of K terms. Anyway, this is the sort of thing which gets clearer as you do it, so I will not dwell on it.
{{{ syntax MySet [builtin(MyBuiltinSet)] Note that this has no production, so we will have to extend the parser to allow this syntax MySet ::= ".MySet" [builtin(MyBuiltinSetEmpty)] syntax MySet ::= MySet "U" MySet [builtin(MyBuiltinSetUnion)] syntax MySet ::= K "in" MySet [builtin(MyBuiltinSetMembership)] ... }}}
Then a rule of the form
rule <k> acq(L) => . ....</k> <locks> Ls => Ls U L </locks> when notBool(L in Ls)
kompiles into a rule (everything is now internal representation, possibly using getters or wrappers):
{{{ rule <k> acq(L) => . ....</k> <locks> Ls => MyBuiltinSetUnion(Ls,L) </locks> when notBool(L in Ls) }}}
{{{ syntax MyMap [builtin(MyBuiltinMap)] syntax MyMap ::= ".MyMap" [builtin(MyBuiltinMapEmpty)] syntax MyMap ::= K "|-> " K [builtin(MyBuiltinMapBinding)] syntax K ::= MyMap "(" K ")" [builtin(MyBuiltinMapLookup)] syntax MyMap ::= MyMap "[" K "/" K "]" [builtin(MyBuiltinMapUpdate)] }}}
Then rules like:
rule <k> ++X => I +Int 1 ...</k> <state>... X |-> (I => I +Int 1) ...</state>
need to be first translated into
rule <k> ++X => Rho(X) +Int 1 ...</k> <state> Rho => Rho[Rho(X) +Int 1 / X] </state>
and then translated into the corresponding rule in the backend which only uses calls to the fast update and lookup operations.
There are obviously lots of details that we have to talk about and eventually converge, but for now all I'm trying to propose is the following user interface notation:
- Sorts:
syntax Sort [builtin(MyBuiltinSort)] // links user-defined sort without tokens to builtin type for corresponding values; e.g., maps above
syntax Sort ::= Token{...} [builtin(MyBuiltinSort)] // links user-defined sort with tokens to builtin type for corresponding values (e.g., integers)- Labels:
syntax KLabel ::= "mylabel" [builtin(MyBuiltinOperation)]
From Radu's perspective, all we need for now is a "builtin" attribute. Personally, if enough people prefer "hook" instead, I don't mind.