| copyright |
|---|
Copyright (c) Runtime Verification, Inc. All Rights Reserved. |
A major piece of the K prelude consists of a series of modules that contain
implementations of basic data types and language features in K. You do not need
to require this file yourself; it is required automatically in every K
definition unless --no-prelude is passed to kompile. K may not work correctly
if some of these modules do not exist or do not declare certain functions.
Note that some functions in the K prelude functions are not total, that is, they are not defined on all possible input values. When you invoke such a function on an undefined input, the behavior is undefined. In particular, when this happens, interpreters generated by the K LLVM backend may crash.
requires "kast.md"
K declares certain modules that contain most of the builtins you usually want
when defining a language in K. In particular, this includes integers, booleans,
strings, identifiers, I/O, lists, maps, and sets. The DOMAINS-SYNTAX module
is designed to be imported by the syntax module of the language and contains
only the program-level syntax of identifiers, integers, booleans, and strings.
The DOMAINS module contains the rest of the syntax, including builtin
functions over those and the remaining types.
Note that not all modules are included in DOMAINS. A few less-common modules
are not, including ARRAY, COLLECTIONS, FLOAT, STRING-BUFFER, BYTES,
K-REFLECTION, MINT.
module DOMAINS-SYNTAX
imports SORT-K
imports ID-SYNTAX
imports UNSIGNED-INT-SYNTAX
imports BOOL-SYNTAX
imports STRING-SYNTAX
endmodule
module DOMAINS
imports DOMAINS-SYNTAX
imports INT
imports BOOL
imports STRING
imports BASIC-K
imports LIST
imports K-IO
imports MAP
imports SET
imports ID
imports K-EQUAL
endmodule
Provided here is an implementation for fixed-sized, contiguous maps from Int
to KItem. In some previous versions of K, the Array type was a builtin type
backed by mutable arrays of objects. However, in modern K, the Array type is
implemented by means of the List type; users should not access this interface
directly and should instead make only of the functions listed below. Users of
this module should import only the ARRAY module.
module ARRAY-SYNTAX
imports private LIST
syntax Array
You can look up an element in an Array by its index in O(log(N)) time. Note
that the base of the logarithm is a relatively high number and thus the time is
effectively constant.
syntax KItem ::= Array "[" Int "]" [function]
You can create a new Array with a new value for a key in O(log(N)) time, or
effectively constant.
syntax Array ::= Array "[" key: Int "<-" value: KItem "]" [function, symbol(_[_<-_])]
You can create a new Array where a particular key is reset to its default
value in O(log(N)) time, or effectively constant.
syntax Array ::= Array "[" Int "<-" "undef" "]" [function]
You can create a new Array from a List L of size N where the N
elements starting at index are replaced with the contents of L, in
O(N*log(K)) time (where K is the size of the array), or effectively linear.
Having index + N > K yields an exception.
syntax Array ::= updateArray(Array, index: Int, List) [function]
You can create a new Array where the length elements starting at index
are replaced with value, in O(length*log(N)) time, or effectively linear.
syntax Array ::= fillArray(Array, index: Int, length: Int, value: KItem) [function]
You can test whether an integer is within the bounds of an array in O(1) time.
syntax Bool ::= Int "in_keys" "(" Array ")" [function, total]
endmodule
module ARRAY-IN-K [private]
imports public ARRAY-SYNTAX
imports private LIST
imports private K-EQUAL
imports private INT
imports private BOOL
You can create an array with length elements where each element is
initialized to value in O(1) time. Note that the array is stored in a manner
where only the highest element that is actually modified is given a value
in its internal representation, which means that subsequent array operations
may incur a one-time O(N) resizing cost, possibly amortized across multiple
operations.
syntax Array ::= makeArray(length: Int, value: KItem) [function, public]
The remainder of this section consists of an implementation in K of the
operations listed above. Users of the ARRAY module should not make use
of any of the syntax defined in any of these modules.
syntax Array ::= arr(List, Int, KItem)
rule makeArray(I::Int, D::KItem) => arr(.List, I, D)
rule arr(L::List, _, _ ) [ IDX::Int ] => L[IDX] requires 0 <=Int IDX andBool IDX <Int size(L)
rule arr(_ , _, D::KItem) [ _ ] => D [owise]
syntax List ::= ensureOffsetList(List, Int, KItem) [function]
rule ensureOffsetList(L::List, IDX::Int, D::KItem) => L makeList(IDX +Int 1 -Int size(L), D) requires IDX >=Int size(L)
rule ensureOffsetList(L::List, IDX::Int, _::KItem) => L requires notBool IDX >=Int size(L)
rule arr(L::List, I::Int, D::KItem) [ IDX::Int <- VAL::KItem ] => arr(ensureOffsetList(L, IDX, D) [ IDX <- VAL ], I, D)
rule arr(L::List, I::Int, D::KItem) [ IDX::Int <- undef ] => arr(L, I, D) [ IDX <- D ]
rule updateArray(arr(L::List, I::Int, D::KItem), IDX::Int, L2::List) => arr(updateList(ensureOffsetList(L, IDX +Int size(L2) -Int 1, D), IDX, L2), I, D)
rule fillArray(arr(L::List, I::Int, D::KItem), IDX::Int, LEN::Int, VAL::KItem) => arr(fillList(ensureOffsetList(L, IDX +Int LEN -Int 1, D), IDX, LEN, VAL), I, D)
rule IDX::Int in_keys(arr(_, I::Int, _)) => IDX >=Int 0 andBool IDX <Int I
endmodule
module ARRAY-SYMBOLIC [symbolic]
imports ARRAY-IN-K
endmodule
module ARRAY-KORE
imports ARRAY-IN-K
endmodule
module ARRAY
imports ARRAY-SYMBOLIC
imports ARRAY-KORE
endmodule
Provided here is the syntax of an implementation of immutable, associative,
commutative maps from KItem to KItem. This type is hooked to an
implementation of maps provided by the backend. For more information on
matching on maps and allowable patterns for doing so, refer to K's
user documentation.
module MAP
imports private BOOL-SYNTAX
imports private INT-SYNTAX
imports private LIST
imports private SET
syntax Map [hook(MAP.Map)]
The Map sort represents a generalized associative array. Each key can be
paired with an arbitrary value, and can be used to reference its associated
value. Multiple bindings for the same key are not allowed.
You can construct a new Map consisting of key/value pairs of two Maps. The
result is #False if the maps have keys in common (in particular, this will
yield an exception during concrete execution). This operation is O(Nlog(M))
where N is the size of the smaller map, when it appears on the right hand side.
When it appears on the left hand side and all variables are bound, it is
O(Nlog(M)) where M is the size of the map it is matching and N is the number
of elements being matched. When it appears on the left hand side containing
variables not bound elsewhere in the term, it is O(N^K) where N is the size of
the map it is matching and K is the number of unbound keys being matched. In
other words, one unbound variable is linear, two is quadratic, three is cubic,
etc.
syntax Map ::= Map Map [left, function, hook(MAP.concat), symbol(_Map_), assoc, comm, unit(.Map), element(_|->_), index(0), format(%1%n%2)]
The map with zero elements is represented by .Map.
syntax Map ::= ".Map" [function, total, hook(MAP.unit), symbol(.Map)]
An element of a Map is constructed via the |-> operator. The key is on the
left and the value is on the right.
syntax Map ::= KItem "|->" KItem [function, total, hook(MAP.element), symbol(_|->_), injective]
syntax priority _|->_ > _Map_ .Map
syntax non-assoc _|->_
You can look up the value associated with the key of a map in O(log(N)) time.
Note that the base of the logarithm is a relatively high number and thus the
time is effectively constant. The value is #False if the key is not in the
map (in particular, this will yield an exception during concrete execution).
syntax KItem ::= Map "[" KItem "]" [function, hook(MAP.lookup), symbol(Map:lookup)]
You can also look up the value associated with the key of a map using a total function that assigns a specific default value if the key is not present in the map. This operation is also O(log(N)), or effectively constant.
syntax KItem ::= Map "[" KItem "]" "orDefault" KItem [function, total, hook(MAP.lookupOrDefault), symbol(Map:lookupOrDefault)]
You can insert a key/value pair into a map in O(log(N)) time, or effectively constant.
syntax Map ::= Map "[" key: KItem "<-" value: KItem "]" [function, total, symbol(Map:update), hook(MAP.update), prefer]
You can remove a key/value pair from a map via its key in O(log(N)) time, or effectively constant.
syntax Map ::= Map "[" KItem "<-" "undef" "]" [function, total, hook(MAP.remove), symbol(_[_<-undef])]
You can remove the key/value pairs in a map that are present in another map in
O(N*log(M)) time (where M is the size of the first map and N is the size of the
second), or effectively linear. Note that only keys whose value is the same
in both maps are removed. To remove all the keys in one map from another map,
you can say removeAll(M1, keys(M2)).
syntax Map ::= Map "-Map" Map [function, total, hook(MAP.difference)]
You can update a map by adding all the key/value pairs in the second map in O(N*log(M)) time (where M is the size of the first map and N is the size of the second map), or effectively linear. If any keys are present in both maps, the value from the second map overwrites the value in the first. This function is total, which is distinct from map concatenation, a partial function only defined on maps with disjoint keys.
syntax Map ::= updateMap(Map, Map) [function, total, hook(MAP.updateAll)]
You can remove a Set of keys from a map in O(N*log(M)) time (where M is the
size of the Map and N is the size of the Set), or effectively linear.
syntax Map ::= removeAll(Map, Set) [function, total, hook(MAP.removeAll)]
You can get a Set of all the keys in a Map in O(N) time.
syntax Set ::= keys(Map) [function, total, hook(MAP.keys)]
You can get a List of all the keys in a Map in O(N) time.
syntax List ::= "keys_list" "(" Map ")" [function, hook(MAP.keys_list)]
You can check whether a key is present in a map in O(1) time.
syntax Bool ::= KItem "in_keys" "(" Map ")" [function, total, hook(MAP.in_keys)]
You can get a List of all the values in a map in O(N) time.
syntax List ::= values(Map) [function, hook(MAP.values)]
You can get the number of key/value pairs in a map in O(1) time.
syntax Int ::= size(Map) [function, total, hook(MAP.size), symbol(sizeMap)]
You can determine whether a Map is a strict subset of another Map in O(N)
time (where N is the size of the first map). Only keys that are bound to the
same value are considered equal.
syntax Bool ::= Map "<=Map" Map [function, total, hook(MAP.inclusion)]
You can get an arbitrarily chosen key of a Map in O(1) time. The same key
will always be returned for the same map, but no guarantee is given that two
different maps will return the same element, even if they are similar.
syntax KItem ::= choice(Map) [function, hook(MAP.choice), symbol(Map:choice)]
The remainder of this section contains lemmas used by the Java and Haskell
backend to simplify expressions of sort Map. They do not affect the semantics
of maps, merely describing additional rules that the backend can use to
simplify terms.
endmodule
module MAP-KORE-SYMBOLIC [symbolic,haskell]
imports MAP
imports private K-EQUAL
imports private BOOL
rule #Ceil(@M:Map [@K:KItem]) => {(@K in_keys(@M)) #Equals true} #And #Ceil(@M) #And #Ceil(@K) [simplification]
// Symbolic update
// Adding the definedness condition `notBool (K in_keys(M))` in the ensures clause of the following rule would be redundant
// because K also appears in the rhs, preserving the case when it's #Bottom.
rule (K |-> _ M:Map) [ K <- V ] => (K |-> V M) [simplification]
rule M:Map [ K <- V ] => (K |-> V M) requires notBool (K in_keys(M)) [simplification]
rule M:Map [ K <- _ ] [ K <- V ] => M [ K <- V ] [simplification]
// Adding the definedness condition `notBool (K1 in_keys(M))` in the ensures clause of the following rule would be redundant
// because K1 also appears in the rhs, preserving the case when it's #Bottom.
rule (K1 |-> V1 M:Map) [ K2 <- V2 ] => (K1 |-> V1 (M [ K2 <- V2 ])) requires K1 =/=K K2 [simplification]
// Symbolic remove
rule (K |-> _ M:Map) [ K <- undef ] => M ensures notBool (K in_keys(M)) [simplification]
rule M:Map [ K <- undef ] => M requires notBool (K in_keys(M)) [simplification]
// Adding the definedness condition `notBool (K1 in_keys(M))` in the ensures clause of the following rule would be redundant
// because K1 also appears in the rhs, preserving the case when it's #Bottom.
rule (K1 |-> V1 M:Map) [ K2 <- undef ] => (K1 |-> V1 (M [ K2 <- undef ])) requires K1 =/=K K2 [simplification]
// Symbolic lookup
rule (K |-> V M:Map) [ K ] => V ensures notBool (K in_keys(M)) [simplification]
rule (K1 |-> _V M:Map) [ K2 ] => M [K2] requires K1 =/=K K2 ensures notBool (K1 in_keys(M)) [simplification]
rule (_MAP:Map [ K <- V1 ]) [ K ] => V1 [simplification]
rule ( MAP:Map [ K1 <- _V1 ]) [ K2 ] => MAP [ K2 ] requires K1 =/=K K2 [simplification]
rule (K |-> V M:Map) [ K ] orDefault _ => V ensures notBool (K in_keys(M)) [simplification]
rule (K1 |-> _V M:Map) [ K2 ] orDefault D => M [K2] orDefault D requires K1 =/=K K2 ensures notBool (K1 in_keys(M)) [simplification]
rule (_MAP:Map [ K <- V1 ]) [ K ] orDefault _ => V1 [simplification]
rule ( MAP:Map [ K1 <- _V1 ]) [ K2 ] orDefault D => MAP [ K2 ] orDefault D requires K1 =/=K K2 [simplification]
rule .Map [ _ ] orDefault D => D [simplification]
// Symbolic in_keys
rule K in_keys(_M [ K <- undef ]) => false [simplification]
rule K in_keys(_M [ K <- _ ]) => true [simplification]
rule K1 in_keys(M [ K2 <- _ ]) => true requires K1 ==K K2 orBool K1 in_keys(M) [simplification]
rule K1 in_keys(M [ K2 <- _ ]) => K1 in_keys(M) requires K1 =/=K K2 [simplification]
rule {false #Equals @Key in_keys(.Map)} => #Ceil(@Key) [simplification]
rule {@Key in_keys(.Map) #Equals false} => #Ceil(@Key) [simplification]
rule {false #Equals @Key in_keys(Key' |-> Val @M)} => #Ceil(@Key) #And #Ceil(Key' |-> Val @M) #And #Not({@Key #Equals Key'}) #And {false #Equals @Key in_keys(@M)} [simplification]
rule {@Key in_keys(Key' |-> Val @M) #Equals false} => #Ceil(@Key) #And #Ceil(Key' |-> Val @M) #And #Not({@Key #Equals Key'}) #And {@Key in_keys(@M) #Equals false} [simplification]
/*
// The rule below is automatically generated by the frontend for every sort
// hooked to MAP.Map. It is left here to serve as documentation.
rule #Ceil(@M:Map (@K:KItem |-> @V:KItem)) => {(@K in_keys(@M)) #Equals false} #And #Ceil(@M) #And #Ceil(@K) #And #Ceil(@V)
[simplification]
*/
endmodule
module MAP-SYMBOLIC
imports MAP-KORE-SYMBOLIC
endmodule
Provided here is the syntax of an implementation of immutable, associative,
commutative range maps from Int to KItem. This type is hooked to an
implementation of range maps provided by the LLVM backend.
Currently, this type is not supported by other backends.
Although the underlying range map data structure supports any key sort, the
current implementation by the backend only supports Int keys due to
limitations of the underlying ordering function.
module RANGEMAP
imports private BOOL-SYNTAX
imports private INT-SYNTAX
imports private LIST
imports private SET
syntax Range ::= "[" KItem "," KItem ")" [symbol(RangeMap:Range)]
syntax RangeMap [hook(RANGEMAP.RangeMap)]
The RangeMap sort represents a map whose keys are stored as ranges, bounded
inclusively below and exclusively above. Contiguous or overlapping ranges that
map to the same value are merged into a single range.
You can construct a new RangeMap consisting of range/value pairs of two
RangeMaps. If the RangeMaps have overlapping ranges an exception will be
thrown during concrete execution. This operation is O(N*log(M)) (where N is
the size of the smaller map and M is the size of the larger map).
syntax RangeMap ::= RangeMap RangeMap [left, function, hook(RANGEMAP.concat), symbol(_RangeMap_), assoc, comm, unit(.RangeMap), element(_r|->_), index(0), format(%1%n%2)]
The RangeMap with zero elements is represented by .RangeMap.
syntax RangeMap ::= ".RangeMap" [function, total, hook(RANGEMAP.unit), symbol(.RangeMap)]
An element of a RangeMap is constructed via the r|-> operator. The range
of keys is on the left, and the value is on the right.
syntax RangeMap ::= Range "r|->" KItem [function, hook(RANGEMAP.elementRng), symbol(_r|->_), injective]
syntax priority _r|->_ > _RangeMap_ .RangeMap
syntax non-assoc _r|->_
You can look up the value associated with a key of a RangeMap in O(log(N))
time (where N is the size of the RangeMap). This will yield an exception
during concrete execution if the key is not in the range map.
syntax KItem ::= RangeMap "[" KItem "]" [function, hook(RANGEMAP.lookup), symbol(RangeMap:lookup)]
You can also look up the value associated with a key of a RangeMap using a
total function that assigns a specific default value if the key is not present
in the RangeMap. This operation is also O(log(N)) (where N is the size of
the range map).
syntax KItem ::= RangeMap "[" KItem "]" "orDefault" KItem [function, total, hook(RANGEMAP.lookupOrDefault), symbol(RangeMap:lookupOrDefault)]
You can look up for the range that a key of a RangeMap is stored in in
O(log(N)) time (where N is the size of the RangeMap). This will yield an
exception during concrete execution if the key is not in the range map.
syntax Range ::= "find_range" "(" RangeMap "," KItem ")" [function, hook(RANGEMAP.find_range), symbol(RangeMap:find_range)]
You can insert a range/value pair into a RangeMap in O(log(N)) time (where N
is the size of the RangeMap). Any ranges adjacent to or overlapping with the
range to be inserted will be updated accordingly.
syntax RangeMap ::= RangeMap "[" keyRange: Range "<-" value: KItem "]" [function, symbol(RangeMap:update), hook(RANGEMAP.updateRng), prefer]
You can remove a range/value pair from a RangeMap in O(log(N)) time (where N
is the size of the RangeMap). If all or any part of the range is present in
the range map, it will be removed.
syntax RangeMap ::= RangeMap "[" Range "<-" "undef" "]" [function, hook(RANGEMAP.removeRng), symbol(_r[_<-undef])]
You can remove the range/value pairs in a RangeMap that are also present in
another RangeMap in O(max{M,N}*log(M)) time (where M is the size of the
first RangeMap and N is the size of the second RangeMap). Note that only
the parts of overlapping ranges whose value is the same in both range maps
will be removed.
syntax RangeMap ::= RangeMap "-RangeMap" RangeMap [function, total, hook(RANGEMAP.difference)]
You can update a RangeMap by adding all the range/value pairs in the second
RangeMap in O(N*log(M+N)) time (where M is the size of the first RangeMap
and N is the size of the second RangeMap). If any ranges are overlapping,
the value from the second range map overwrites the value in the first for the
parts where ranges are overlapping. This function is total, which is distinct
from range map concatenation, a partial function only defined on range maps
with non overlapping ranges.
syntax RangeMap ::= updateRangeMap(RangeMap, RangeMap) [function, total, hook(RANGEMAP.updateAll)]
You can remove a Set of ranges from a RangeMap in O(N*log(M)) time (where
M is the size of the RangeMap and N is the size of the Set). For every
range in the set, all or any part of it that is present in the range map will
be removed.
syntax RangeMap ::= removeAll(RangeMap, Set) [function, hook(RANGEMAP.removeAll)]
You can get a Set of all the ranges in a RangeMap in O(N) time (where N
is the size of the RangeMap).
syntax Set ::= keys(RangeMap) [function, total, hook(RANGEMAP.keys)]
You can get a List of all the ranges in a RangeMap in O(N) time (where N
is the size of the RangeMap).
syntax List ::= "keys_list" "(" RangeMap ")" [function, hook(RANGEMAP.keys_list)]
You can check whether a key is present in a RangeMap in O(log(N)) time (where
N is the size of the RangeMap).
syntax Bool ::= KItem "in_keys" "(" RangeMap ")" [function, total, hook(RANGEMAP.in_keys)]
You can get a List of all values in a RangeMap in O(N) time (where N is the
size of the RangeMap).
syntax List ::= values(RangeMap) [function, hook(RANGEMAP.values)]
You can get the number of range/value pairs in a RangeMap in O(1) time.
syntax Int ::= size(RangeMap) [function, total, hook(RANGEMAP.size), symbol(sizeRangeMap)]
You can determine whether a RangeMap is a strict subset of another RangeMap
in O(M+N) time (where M is the size of the first RangeMap and N is the size
of the second RangeMap). Only keys within equal or overlapping ranges that
are bound to the same value are considered equal.
syntax Bool ::= RangeMap "<=RangeMap" RangeMap [function, total, hook(RANGEMAP.inclusion)]
You can get an arbitrarily chosen key of a RangeMap in O(1) time. The same
key will always be returned for the same range map, but no guarantee is given
that two different range maps will return the same element, even if they are
similar.
syntax KItem ::= choice(RangeMap) [function, hook(RANGEMAP.choice), symbol(RangeMap:choice)]
endmodule
Provided here is the syntax of an implementation of immutable, associative,
commutative sets of KItem. This type is hooked to an implementation of sets
provided by the backend. For more information on matching on sets and allowable
patterns for doing so, refer to K's
user documentation.
module SET
imports private INT-SYNTAX
imports private BASIC-K
syntax Set [hook(SET.Set)]
The Set sort represents a mathematical set (A collection of unique items).
The sets are nilpotent, i.e., the concatenation of two sets containing elements
in common is #False (note however, this may be silently allowed during
concrete execution). If you intend to add an element to a set that might
already be present in the set, use the |Set operator instead.
The concatenation operator is O(Nlog(M)) where N is the size of the smaller set, when it appears on the right hand side. When it appears on the left hand side and all variables are bound, it is O(Nlog(M)) where M is the size of the set it is matching and N is the number of elements being matched. When it appears on the left hand side containing variables not bound elsewhere in the term, it is O(N^K) where N is the size of the set it is matching and K is the number of unbound keys being mached. In other words, one unbound variable is linear, two is quadratic, three is cubic, etc.
syntax Set ::= Set Set [left, function, hook(SET.concat), symbol(_Set_), assoc, comm, unit(.Set), idem, element(SetItem), format(%1%n%2)]
The set with zero elements is represented by .Set.
syntax Set ::= ".Set" [function, total, hook(SET.unit), symbol(.Set)]
An element of a Set is constructed via the SetItem operator.
syntax Set ::= SetItem(KItem) [function, total, hook(SET.element), symbol(SetItem), injective]
You can compute the union of two sets in O(N*log(M)) time (Where N is the size of the smaller set). Note that the base of the logarithm is a relatively high number and thus the time is effectively linear. The union consists of all the elements present in either set.
syntax Set ::= Set "|Set" Set [left, function, total, hook(SET.union), comm]
rule S1:Set |Set S2:Set => S1 (S2 -Set S1) [concrete]
You can compute the intersection of two sets in O(N*log(M)) time (where N is the size of the smaller set), or effectively linear. The intersection consists of all the elements present in both sets.
syntax Set ::= intersectSet(Set, Set) [function, total, hook(SET.intersection), comm]
You can compute the relative complement of two sets in O(N*log(M)) time (where N is the size of the second set), or effectively linear. This is the set of elements in the first set that are not present in the second set.
syntax Set ::= Set "-Set" Set [function, total, hook(SET.difference), symbol(Set:difference)]
You can compute whether an element is a member of a set in O(1) time.
syntax Bool ::= KItem "in" Set [function, total, hook(SET.in), symbol(Set:in)]
You can determine whether a Set is a strict subset of another Set in O(N)
time (where N is the size of the first set).
syntax Bool ::= Set "<=Set" Set [function, total, hook(SET.inclusion)]
You can get the number of elements (the cardinality) of a set in O(1) time.
syntax Int ::= size(Set) [function, total, hook(SET.size)]
You can get an arbitrarily chosen element of a Set in O(1) time. The same
element will always be returned for the same set, but no guarantee is given
that two different sets will return the same element, even if they are similar.
syntax KItem ::= choice(Set) [function, hook(SET.choice), symbol(Set:choice)]
endmodule
The following lemmas are simplifications that the Haskell backend can
apply to simplify expressions of sort Set.
module SET-KORE-SYMBOLIC [symbolic,haskell]
imports SET
imports private K-EQUAL
imports private BOOL
//Temporarly rule for #Ceil simplification, should be generated in front-end
// Matching for this version not implemented.
// rule #Ceil(@S1:Set @S2:Set) =>
// {intersectSet(@S1, @S2) #Equals .Set} #And #Ceil(@S1) #And #Ceil(@S2)
// [simplification]
//simpler version
rule #Ceil(@S:Set SetItem(@E:KItem)) =>
{(@E in @S) #Equals false} #And #Ceil(@S) #And #Ceil(@E)
[simplification]
// -Set simplifications
rule S -Set .Set => S [simplification]
rule .Set -Set _ => .Set [simplification]
rule SetItem(X) -Set (S SetItem(X)) => .Set
ensures notBool (X in S) [simplification]
rule S -Set (S SetItem(X)) => .Set
ensures notBool (X in S) [simplification]
rule (S SetItem(X)) -Set S => SetItem(X)
ensures notBool (X in S) [simplification]
rule (S SetItem(X)) -Set SetItem(X) => S
ensures notBool (X in S) [simplification]
// rule SetItem(X) -Set S => SetItem(X)
// requires notBool (X in S) [simplification]
// rule (S1 SetItem(X)) -Set (S2 SetItem(X)) => S1 -Set S2
// ensures notBool (X in S1)
// andBool notBool (X in S2) [simplification]
// |Set simplifications
rule S |Set .Set => S [simplification, comm]
rule S |Set S => S [simplification]
rule (S SetItem(X)) |Set SetItem(X) => S SetItem(X)
ensures notBool (X in S) [simplification, comm]
// Currently disabled, see runtimeverification/haskell-backend#3301
// rule (S SetItem(X)) |Set S => S SetItem(X)
// ensures notBool (X in S) [simplification, comm]
// intersectSet simplifications
rule intersectSet(.Set, _ ) => .Set [simplification, comm]
rule intersectSet( S , S ) => S [simplification]
rule intersectSet( S SetItem(X), SetItem(X)) => SetItem(X)
ensures notBool (X in S) [simplification, comm]
// Currently disabled, see runtimeverification/haskell-backend#3294
// rule intersectSet( S SetItem(X) , S) => S ensures notBool (X in S) [simplification, comm]
rule intersectSet( S1 SetItem(X), S2 SetItem(X)) => intersectSet(S1, S2) SetItem(X)
ensures notBool (X in S1)
andBool notBool (X in S2) [simplification]
// membership simplifications
rule _E in .Set => false [simplification]
rule E in (S SetItem(E)) => true
ensures notBool (E in S) [simplification]
// These two rules would be sound but impose a giant overhead on `in` evaluation:
// rule E1 in (S SetItem(E2)) => true requires E1 in S
// ensures notBool (E2 in S) [simplification]
// rule E1 in (S SetItem(E2)) => E1 in S requires E1 =/=K E2
// ensures notBool (E2 in S) [simplification]
rule X in ((SetItem(X) S) |Set _ ) => true
ensures notBool (X in S) [simplification]
rule X in ( _ |Set (SetItem(X) S)) => true
ensures notBool (X in S) [simplification]
endmodule
module SET-SYMBOLIC
imports SET-KORE-SYMBOLIC
endmodule
Provided here is the syntax of an implementation of immutable, associative
lists of KItem. This type is hooked to an implementation of lists provided
by the backend. For more information on matching on lists and allowable
patterns for doing so, refer to K's
user documentation.
module LIST
imports private INT-SYNTAX
imports private BASIC-K
syntax List [hook(LIST.List)]
The List sort is an ordered collection that may contain duplicate elements.
They are backed by relaxed radix balanced trees, which means that they support
efficiently adding elements to both sides of the list, concatenating two lists,
indexing, and updating elements.
The concatenation operator is O(log(N)) (where N is the size of the longer list) when it appears on the right hand side. When it appears on the left hand side, it is O(N), where N is the number of elements matched on the front and back of the list.
syntax List ::= List List [left, function, total, hook(LIST.concat), symbol(_List_), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem), update(List:set), format(%1%n%2)]
The list with zero elements is represented by .List.
syntax List ::= ".List" [function, total, hook(LIST.unit), symbol(.List), smtlib(smt_seq_nil)]
An element of a List is constucted via the ListItem operator.
syntax List ::= ListItem(KItem) [function, total, hook(LIST.element), symbol(ListItem), smtlib(smt_seq_elem)]
An element can be added to the front of a List using the pushList operator.
syntax List ::= pushList(KItem, List) [function, total, hook(LIST.push), symbol(pushList)]
rule pushList(K::KItem, L1::List) => ListItem(K) L1
You can get an element of a list by its integer offset in O(log(N)) time, or effectively constant. Positive indices are 0-indexed from the beginning of the list, and negative indices are -1-indexed from the end of the list. In other words, 0 is the first element and -1 is the last element.
syntax KItem ::= List "[" Int "]" [function, hook(LIST.get), symbol(List:get)]
You can create a new List with a new value at a particular index in
O(log(N)) time, or effectively constant.
syntax List ::= List "[" index: Int "<-" value: KItem "]" [function, hook(LIST.update), symbol(List:set)]
You can create a list with length elements, each containing value, in O(N)
time.
syntax List ::= makeList(length: Int, value: KItem) [function, hook(LIST.make)]
You can create a new List which is equal to dest except the N elements
starting at index are replaced with the contents of src in O(N*log(K)) time
(where K is the size of destand N is the size of src), or effectively linear. Having index + N > K yields an exception.
syntax List ::= updateList(dest: List, index: Int, src: List) [function, hook(LIST.updateAll)]
You can create a new List where the length elements starting at index
are replaced with value, in O(length*log(N)) time, or effectively linear.
syntax List ::= fillList(List, index: Int, length: Int, value: KItem) [function, hook(LIST.fill)]
You can compute a new List by removing fromFront elements from the front
of the list and fromBack elements from the back of the list in
O((fromFront+fromBack)*log(N)) time, or effectively linear.
syntax List ::= range(List, fromFront: Int, fromBack: Int) [function, hook(LIST.range), symbol(List:range)]
You can compute whether an element is in a list in O(N) time. For repeated
comparisons, it is much better to first convert to a set using List2Set.
syntax Bool ::= KItem "in" List [function, total, hook(LIST.in), symbol(_inList_)]
You can get the number of elements of a list in O(1) time.
syntax Int ::= size(List) [function, total, hook(LIST.size), symbol(sizeList), smtlib(smt_seq_len)]
endmodule
It is possible to convert from a List to a Set or from a Set to a list.
Converting from a List to a Set and back will not provide the same list;
duplicates will have been removed and the list may be reordered. Converting
from a Set to a List and back will generate the same set.
Note that because sets are unordered and lists are ordered, converting from a Set to a List will generate some arbitrary ordering of elements, which may be different from the natural ordering you might assume, or may not. Two equal sets are guaranteed to generate the same ordering, but no guarantee is otherwise provided about what the ordering will be. In particular, adding an element to a set may completely reorder the elements already in the set, when it is converted to a list.
module COLLECTIONS
imports LIST
imports SET
imports MAP
syntax List ::= Set2List(Set) [function, total, hook(SET.set2list)]
syntax Set ::= List2Set(List) [function, total, hook(SET.list2set)]
endmodule
Provided here is the syntax of an implementation of boolean algebra in K.
This type is hooked to an implementation of booleans provided by the backend.
Note that this algebra is different from the builtin truth in matching logic.
You can, however, convert from the truth of the Bool sort to the truth in
matching logic via the expression {B #Equals true}.
The boolean values are true and false.
module SORT-BOOL
syntax Bool [hook(BOOL.Bool)]
endmodule
module BOOL-SYNTAX
imports SORT-BOOL
syntax Bool ::= "true" [token]
syntax Bool ::= "false" [token]
endmodule
module BOOL-COMMON
imports private BASIC-K
imports BOOL-SYNTAX
You can:
- Negate a boolean value.
- AND two boolean values.
- XOR two boolean values.
- OR two boolean values.
- IMPLIES two boolean values (i.e.,
P impliesBool Qis the same asnotBool P orBool Q) - Check equality of two boolean values.
- Check inequality of two boolean values.
Note that only andThenBool and orElseBool are short-circuiting. andBool
and orBool may be short-circuited in concrete backends, but in symbolic
backends, both arguments will be evaluated.
syntax Bool ::= "notBool" Bool [function, total, symbol(notBool_), smt-hook(not), group(boolOperation), hook(BOOL.not)]
> Bool "andBool" Bool [function, total, symbol(_andBool_), left, smt-hook(and), group(boolOperation), hook(BOOL.and)]
| Bool "andThenBool" Bool [function, total, symbol(_andThenBool_), left, smt-hook(and), group(boolOperation), hook(BOOL.andThen)]
| Bool "xorBool" Bool [function, total, symbol(_xorBool_), left, smt-hook(xor), group(boolOperation), hook(BOOL.xor)]
| Bool "orBool" Bool [function, total, symbol(_orBool_), left, smt-hook(or), group(boolOperation), hook(BOOL.or)]
| Bool "orElseBool" Bool [function, total, symbol(_orElseBool_), left, smt-hook(or), group(boolOperation), hook(BOOL.orElse)]
| Bool "impliesBool" Bool [function, total, symbol(_impliesBool_), left, smt-hook(=>), group(boolOperation), hook(BOOL.implies)]
> left:
Bool "==Bool" Bool [function, total, symbol(_==Bool_), left, comm, smt-hook(=), hook(BOOL.eq)]
| Bool "=/=Bool" Bool [function, total, symbol(_=/=Bool_), left, comm, smt-hook(distinct), hook(BOOL.ne)]
The remainder of this section consists of an implementation in K of the operations listed above.
rule notBool true => false
rule notBool false => true
rule true andBool B:Bool => B:Bool
rule B:Bool andBool true => B:Bool [simplification]
rule false andBool _:Bool => false
rule _:Bool andBool false => false [simplification]
rule true andThenBool K::Bool => K
rule K::Bool andThenBool true => K [simplification]
rule false andThenBool _ => false
rule _ andThenBool false => false [simplification]
rule false xorBool B:Bool => B:Bool
rule B:Bool xorBool false => B:Bool [simplification]
rule B:Bool xorBool B:Bool => false
rule true orBool _:Bool => true
rule _:Bool orBool true => true [simplification]
rule false orBool B:Bool => B
rule B:Bool orBool false => B [simplification]
rule true orElseBool _ => true
rule _ orElseBool true => true [simplification]
rule false orElseBool K::Bool => K
rule K::Bool orElseBool false => K [simplification]
rule true impliesBool B:Bool => B
rule false impliesBool _:Bool => true
rule _:Bool impliesBool true => true [simplification]
rule B:Bool impliesBool false => notBool B [simplification]
rule B1:Bool =/=Bool B2:Bool => notBool (B1 ==Bool B2)
endmodule
module BOOL-KORE [symbolic]
imports BOOL-COMMON
rule {true #Equals notBool @B} => {false #Equals @B} [simplification]
rule {notBool @B #Equals true} => {@B #Equals false} [simplification]
rule {false #Equals notBool @B} => {true #Equals @B} [simplification]
rule {notBool @B #Equals false} => {@B #Equals true} [simplification]
rule {true #Equals @B1 andBool @B2} => {true #Equals @B1} #And {true #Equals @B2} [simplification]
rule {@B1 andBool @B2 #Equals true} => {@B1 #Equals true} #And {@B2 #Equals true} [simplification]
rule {false #Equals @B1 orBool @B2} => {false #Equals @B1} #And {false #Equals @B2} [simplification]
rule {@B1 orBool @B2 #Equals false} => {@B1 #Equals false} #And {@B2 #Equals false} [simplification]
endmodule
module BOOL
imports BOOL-COMMON
imports BOOL-KORE
endmodule
Provided here is the syntax of an implementation of arbitrary-precision
integer arithmetic in K. This type is hooked to an implementation of integers
provided by the backend. For a fixed-width integer type, see the MINT module
below.
The UNSIGNED-INT-SYNTAX module provides a syntax of whole numbers in K.
This is useful because often programming languages implement the sign of an
integer as a unary operator rather than part of the lexical syntax of integers.
However, you can also directly reference integers with a sign using the
INT-SYNTAX module.
module UNSIGNED-INT-SYNTAX
syntax Int [hook(INT.Int)]
syntax Int ::= r"[0-9]+" [prefer, token, prec(2)]
endmodule
module INT-SYNTAX
imports UNSIGNED-INT-SYNTAX
syntax Int ::= r"[\\+\\-]?[0-9]+" [prefer, token, prec(2)]
endmodule
module INT-COMMON
imports INT-SYNTAX
imports private BOOL
You can:
- Compute the bitwise complement
~Intof an integer value in twos-complement. - Compute the exponentiation
^Intof two integers. - Compute the exponentiation of two integers modulo another integer (
^%Int).A ^%Int B Cis equal in value to(A ^Int B) %Int C, but has a better asymptotic complexity. - Compute the product
*Intof two integers. - Compute the quotient
/Intor modulus%Intof two integers using t-division, which rounds towards zero. Division by zero is#False. - Compute the quotient
divIntor modulusmodIntof two integers using Euclidean division, in which the remainder is always non-negative. Division by zero is#False. - Compute the sum
+Intor difference-Intof two integers. - Compute the arithmetic right shift
>>Intof two integers. Shifting by a negative quantity is#False. - Compute the left shift of two integers. Shifting by a negative quantity is
#False. - Compute the bitwise and of two integers in twos-complement.
- Compute the bitwise xor of two integers in twos-complement.
- Compute the bitwise inclusive-or of two integers in twos-complement.
syntax Int ::= "~Int" Int [function, symbol(~Int_), total, hook(INT.not), smtlib(notInt)]
> left:
Int "^Int" Int [function, symbol(_^Int_), left, smt-hook(^), hook(INT.pow)]
| Int "^%Int" Int Int [function, symbol(_^%Int__), left, smt-hook((mod (^ #1 #2) #3)), hook(INT.powmod)]
> left:
Int "*Int" Int [function, total, symbol(_*Int_), left, comm, smt-hook(*), hook(INT.mul)]
/* FIXME: translate /Int and %Int into smtlib */
/* /Int and %Int implement t-division, which rounds towards 0. SMT hooks need to convert from Euclidian division operations */
| Int "/Int" Int [function, symbol(_/Int_), left,
smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (div #1 #2) (ite (> #2 0) (+ (div #1 #2) 1) (- (div #1 #2) 1)))),
hook(INT.tdiv)]
| Int "%Int" Int [function, symbol(_%Int_), left,
smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (mod #1 #2) (ite (> #2 0) (- (mod #1 #2) #2) (+ (mod #1 #2) #2)))),
hook(INT.tmod)]
/* divInt and modInt implement e-division according to the Euclidean division theorem, therefore the remainder is always positive */
| Int "divInt" Int [function, symbol(_divInt_), left, smt-hook(div), hook(INT.ediv)]
| Int "modInt" Int [function, symbol(_modInt_), left, smt-hook(mod), hook(INT.emod)]
> left:
Int "+Int" Int [function, total, symbol(_+Int_), left, comm, smt-hook(+), hook(INT.add)]
| Int "-Int" Int [function, total, symbol(_-Int_), left, smt-hook(-), hook(INT.sub)]
> left:
Int ">>Int" Int [function, symbol(_>>Int_), left, hook(INT.shr), smtlib(shrInt)]
| Int "<<Int" Int [function, symbol(_<<Int_), left, hook(INT.shl), smtlib(shlInt)]
> left:
Int "&Int" Int [function, total, symbol(_&Int_), left, comm, hook(INT.and), smtlib(andInt)]
> left:
Int "xorInt" Int [function, total, symbol(_xorInt_), left, comm, hook(INT.xor), smtlib(xorInt)]
> left:
Int "|Int" Int [function, total, symbol(_|Int_), left, comm, hook(INT.or), smtlib(orInt)]
You can compute the minimum and maximum minInt and maxInt of two integers.
syntax Int ::= "minInt" "(" Int "," Int ")" [function, total, smt-hook((ite (< #1 #2) #1 #2)), hook(INT.min)]
| "maxInt" "(" Int "," Int ")" [function, total, smt-hook((ite (< #1 #2) #2 #1)), hook(INT.max)]
You can compute the absolute value absInt of an integer.
syntax Int ::= absInt ( Int ) [function, total, smt-hook((ite (< #1 0) (- 0 #1) #1)), hook(INT.abs)]
You can compute the log base 2, rounded towards zero, of an integer. The log
base 2 of an integer is equal to the index of the highest bit set in the
representation of a positive integer. Log base 2 of zero or a negative number
is #False.
syntax Int ::= log2Int ( Int ) [function, hook(INT.log2)]
You can compute the value of a range of bits in the twos-complement
representation of an integer, as interpeted either unsigned or signed, of an
integer. index is offset from 0 and length is the number of bits, starting
with index, that should be read. The number is assumed to be represented
in little endian notation with each byte going from least significant to
most significant. In other words, 0 is the least-significant bit, and each
successive bit is more significant than the last.
syntax Int ::= bitRangeInt ( Int, index: Int, length: Int ) [function, hook(INT.bitRange)]
| signExtendBitRangeInt ( Int, index: Int, length: Int ) [function, hook(INT.signExtendBitRange)]
You can compute whether two integers are less than or equal to, less than, greater than or equal to, greater than, equal, or unequal to another integer.
syntax Bool ::= Int "<=Int" Int [function, total, symbol(_<=Int_), smt-hook(<=), hook(INT.le)]
| Int "<Int" Int [function, total, symbol(_<Int_), smt-hook(<), hook(INT.lt)]
| Int ">=Int" Int [function, total, symbol(_>=Int_), smt-hook(>=), hook(INT.ge)]
| Int ">Int" Int [function, total, symbol(_>Int_), smt-hook(>), hook(INT.gt)]
| Int "==Int" Int [function, total, symbol(_==Int_), comm, smt-hook(=), hook(INT.eq)]
| Int "=/=Int" Int [function, total, symbol(_=/=Int_), comm, smt-hook(distinct), hook(INT.ne)]
You can compute whether one integer evenly divides another. This is the case when the second integer modulo the first integer is equal to zero.
syntax Bool ::= Int "dividesInt" Int [function]
You can, on concrete backends, compute a pseudorandom integer, or seed the pseudorandom number generator. These operations are represented as uninterpreted functions on symbolic backends.
syntax Int ::= randInt(Int) [function, hook(INT.rand), impure]
syntax K ::= srandInt(Int) [function, hook(INT.srand), impure]
The remainder of this section consists of an implementation in K of some
of the operators above, as well as lemmas used by the Java and Haskell backend
to simplify expressions of sort Int. They do not affect the semantics of
integers, merely describing additional rules that the backend can use to
simplify terms.
endmodule
module INT-SYMBOLIC [symbolic]
imports INT-COMMON
imports INT-SYMBOLIC-KORE
imports private BOOL
// Arithmetic Normalization
rule I +Int 0 => I [simplification]
rule I -Int 0 => I [simplification]
rule X modInt N => X requires 0 <=Int X andBool X <Int N [simplification]
rule X %Int N => X requires 0 <=Int X andBool X <Int N [simplification]
// Bit-shifts
rule X <<Int 0 => X [simplification, preserves-definedness]
rule 0 <<Int Y => 0 requires 0 <=Int Y [simplification, preserves-definedness]
rule X >>Int 0 => X [simplification, preserves-definedness]
rule 0 >>Int Y => 0 requires 0 <=Int Y [simplification, preserves-definedness]
endmodule
module INT-SYMBOLIC-KORE [symbolic, haskell]
imports INT-COMMON
imports ML-SYNTAX
imports private BOOL
// Definability Conditions
rule #Ceil(@I1:Int /Int @I2:Int) => {(@I2 =/=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2) [simplification]
rule #Ceil(@I1:Int %Int @I2:Int) => {(@I2 =/=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2) [simplification]
rule #Ceil(@I1:Int modInt @I2:Int) => {(@I2 =/=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2) [simplification]
rule #Ceil(@I1:Int >>Int @I2:Int) => {(@I2 >=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2) [simplification]
rule #Ceil(@I1:Int <<Int @I2:Int) => {(@I2 >=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2) [simplification]
endmodule
module INT-KORE [symbolic]
imports private K-EQUAL
imports private BOOL
imports INT-COMMON
rule [eq-k-to-eq-int] : I1:Int ==K I2:Int => I1 ==Int I2 [simplification]
rule [eq-int-true-left] : {K1 ==Int K2 #Equals true} => {K1 #Equals K2} [simplification]
rule [eq-int-true-rigth] : {true #Equals K1 ==Int K2} => {K1 #Equals K2} [simplification]
rule [eq-int-false-left] : {K1 ==Int K2 #Equals false} => #Not({K1 #Equals K2}) [simplification]
rule [eq-int-false-rigth] : {false #Equals K1 ==Int K2} => #Not({K1 #Equals K2}) [simplification]
rule [neq-int-true-left] : {K1 =/=Int K2 #Equals true} => #Not({K1 #Equals K2}) [simplification]
rule [neq-int-true-right] : {true #Equals K1 =/=Int K2} => #Not({K1 #Equals K2}) [simplification]
rule [neq-int-false-left] : {K1 =/=Int K2 #Equals false} => {K1 #Equals K2} [simplification]
rule [neq-int-false-right]: {false #Equals K1 =/=Int K2} => {K1 #Equals K2} [simplification]
// Arithmetic Normalization
rule I +Int B => B +Int I [concrete(I), symbolic(B), simplification(51)]
rule A -Int I => A +Int (0 -Int I) [concrete(I), symbolic(A), simplification(51)]
rule (A +Int I2) +Int I3 => A +Int (I2 +Int I3) [concrete(I2, I3), symbolic(A), simplification]
rule I1 +Int (B +Int I3) => B +Int (I1 +Int I3) [concrete(I1, I3), symbolic(B), simplification]
rule I1 -Int (B +Int I3) => (I1 -Int I3) -Int B [concrete(I1, I3), symbolic(B), simplification]
rule I1 +Int (I2 +Int C) => (I1 +Int I2) +Int C [concrete(I1, I2), symbolic(C), simplification]
rule I1 +Int (I2 -Int C) => (I1 +Int I2) -Int C [concrete(I1, I2), symbolic(C), simplification]
rule (I1 -Int B) +Int I3 => (I1 +Int I3) -Int B [concrete(I1, I3), symbolic(B), simplification]
rule I1 -Int (I2 +Int C) => (I1 -Int I2) -Int C [concrete(I1, I2), symbolic(C), simplification]
rule I1 -Int (I2 -Int C) => (I1 -Int I2) +Int C [concrete(I1, I2), symbolic(C), simplification]
rule (C -Int I2) -Int I3 => C -Int (I2 +Int I3) [concrete(I2, I3), symbolic(C), simplification]
rule I1 &Int (I2 &Int C) => (I1 &Int I2) &Int C [concrete(I1, I2), symbolic(C), simplification]
endmodule
module INT
imports INT-COMMON
imports INT-SYMBOLIC
imports INT-KORE
imports private K-EQUAL
imports private BOOL
rule bitRangeInt(I::Int, IDX::Int, LEN::Int) => (I >>Int IDX) modInt (1 <<Int LEN)
rule signExtendBitRangeInt(I::Int, IDX::Int, LEN::Int) => (bitRangeInt(I, IDX, LEN) +Int (1 <<Int (LEN -Int 1))) modInt (1 <<Int LEN) -Int (1 <<Int (LEN -Int 1))
rule I1:Int divInt I2:Int => (I1 -Int (I1 modInt I2)) /Int I2
requires I2 =/=Int 0
rule
I1:Int modInt I2:Int
=>
((I1 %Int absInt(I2)) +Int absInt(I2)) %Int absInt(I2)
requires I2 =/=Int 0 [concrete, simplification]
rule minInt(I1:Int, I2:Int) => I1 requires I1 <Int I2
rule minInt(I1:Int, I2:Int) => I2 requires I1 >=Int I2
rule I1:Int =/=Int I2:Int => notBool (I1 ==Int I2)
rule (I1:Int dividesInt I2:Int) => (I2 %Int I1) ==Int 0
syntax Int ::= freshInt(Int) [freshGenerator, function, total, private]
rule freshInt(I:Int) => I
endmodule
Provided here is the syntax of an implementation of arbitrary-precision floating-point arithmetic in K based on a generalization of the IEEE 754 standard. This type is hooked to an implementation of floats provided by the backend.
The syntax of ordinary floating-point values in K consists of an optional sign
(+ or -) followed by an optional integer part, followed by a decimal point,
followed by an optional fractional part. Either the integer part or the
fractional part must be specified. The mantissa is followed by an optional
exponent part, which consists of an e or E, an optional sign (+ or -),
and an integer. The expoennt is followed by an optional suffix, which can be
either f, F, d, D, or pNxM where N and M are positive integers.
p and x can be either upper or lowercase.
The value of a floating-point literal is computed as follows: First the
mantissa is read as a rational number. Then it is multiplied by 10 to the
power of the exponent, which is interpreted as an integer, and defaults to
zero if it is not present. Finally, it is rounded to the nearest possible
value in a floating-point type represented like an IEEE754 floating-point type,
with the number of bits of precision and exponent specified by the suffix.
A suffix of f or f represents the IEEE binary32 format. A suffix of d
or D, or no suffix, represents the IEEE binary64 format. A suffix of
pNxM (either upper or lowercase) specifies exactly N bits of precision and
M bits of exponent. The number of bits of precision is assumed to include
any optional 1 that precedes the IEEE 754 mantissa. In other words, p24x8
is equal to the IEEE binary32 format, and p53x11 is equal to the IEEE
binary64 format.
module FLOAT-SYNTAX
syntax Float [hook(FLOAT.Float)]
syntax Float ::= r"([\\+\\-]?[0-9]+(\\.[0-9]*)?|\\.[0-9]+)([eE][\\+\\-]?[0-9]+)?([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token, prec(1)]
syntax Float ::= r"[\\+\\-]?Infinity([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token, prec(3)]
syntax Float ::= r"NaN([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token, prec(3)]
endmodule
module FLOAT
imports FLOAT-SYNTAX
imports private BOOL
imports private INT-SYNTAX
You can retrieve the number of bits of precision in a Float.
syntax Int ::= precisionFloat(Float) [function, total, hook(FLOAT.precision)]
You can retrieve the number of bits of exponent range in a Float.
syntax Int ::= exponentBitsFloat(Float) [function, total, hook(FLOAT.exponentBits)]
You can retrieve the value of the exponent bits of a Float as an integer.
syntax Int ::= exponentFloat(Float) [function, total, hook(FLOAT.exponent)]
You can retrieve the value of the sign bit of a Float as a boolean. True
means the sign bit is set.
syntax Bool ::= signFloat(Float) [function, total, hook(FLOAT.sign)]
You can check whether a Float value is infinite or Not-a-Number.
syntax Bool ::= isNaN(Float) [function, total, smt-hook(fp.isNaN), hook(FLOAT.isNaN)]
| isInfinite(Float) [function, total]
You can:
- Compute the unary negation
--Floatof a float.--Float Xis distinct from0.0 -Float X. For example,0.0 -Float 0.0is positive zero.--Float 0.0is negative zero. - Compute the exponentation
^Floatof two floats. - Compute the product
*Float, quotient/Float, or remainder%Floatof two floats. The remainder is computed based on rounding the quotient of the two floats to the nearest integer. - Compute the sum
+Floator difference-Floatof two floats.
syntax Float ::= "--Float" Float [function, total, smt-hook(fp.neg), hook(FLOAT.neg)]
> Float "^Float" Float [function, left, hook(FLOAT.pow)]
> left:
Float "*Float" Float [function, left, smt-hook((fp.mul roundNearestTiesToEven #1 #2)), hook(FLOAT.mul)]
| Float "/Float" Float [function, left, smt-hook((fp.div roundNearestTiesToEven #1 #2)), hook(FLOAT.div)]
| Float "%Float" Float [function, left, smt-hook((fp.rem roundNearestTiesToEven #1 #2)), hook(FLOAT.rem)]
> left:
Float "+Float" Float [function, left, smt-hook((fp.add roundNearestTiesToEven #1 #2)), hook(FLOAT.add)]
| Float "-Float" Float [function, left, smt-hook((fp.sub roundNearestTiesToEven #1 #2)), hook(FLOAT.sub)]
You can:
- Compute the Nth integer root
rootFloatof a float. - Compute the absolute value
absFloatof a float. - Round a floating-point number to a specified precision and exponent
range (
roundFloat). The resultingFloatwill yield the specified values when callingprecisionFloatandexponentBitsFloatand when performing further computation. - Round a float to the next lowest floating-point value which is an integer
(
floorFloat). - Round a float to the next highest floating-point value which is an integer
(
ceilFloat). - Round a float to the next closest floating-point value which is an integer, in
the direction of zero (
truncFloat). - Compute the natural exponential
expFloatof a float (i.e. e^x). - Compute the natural logarithm
logFloatof a float. - Compute the sine
sinFloatof a float. - Compute the cosine
cosFloatof a float. - Compute the tangent
tanFlooatof a float. - Compute the arcsine
asinFloatof a float. - Compute the arccosine
acosFloatof a float. - Compute the arctangent
atanFloatof a float. - Compute the arctangent
atan2Floatof two floats. - Compute the maximum
maxFloatof two floats. - Compute the minimum
minFloatof two floats. - Compute the square root
sqrtFloatof a float. - Compute the largest finite value expressible in a specified precision and
exponent range (
maxValueFloat). - Compute the smallest positive finite value expressible in a specified
precision and exponent range (
minValueFloat).
syntax Float ::= rootFloat(Float, Int) [function, hook(FLOAT.root)]
| absFloat(Float) [function, total, smt-hook(fp.abs), hook(FLOAT.abs)]
| roundFloat(Float, precision: Int, exponentBits: Int) [function, hook(FLOAT.round)]
| floorFloat(Float) [function, total, hook(FLOAT.floor)]
| ceilFloat(Float) [function, total, hook(FLOAT.ceil)]
| truncFloat(Float) [function, total, hook(FLOAT.trunc)]
| expFloat(Float) [function, total, hook(FLOAT.exp)]
| logFloat(Float) [function, hook(FLOAT.log)]
| sinFloat(Float) [function, total, hook(FLOAT.sin)]
| cosFloat(Float) [function, total, hook(FLOAT.cos)]
| tanFloat(Float) [function, hook(FLOAT.tan)]
| asinFloat(Float) [function, hook(FLOAT.asin)]
| acosFloat(Float) [function, hook(FLOAT.acos)]
| atanFloat(Float) [function, total, hook(FLOAT.atan)]
| atan2Float(Float, Float) [function, hook(FLOAT.atan2)]
| maxFloat(Float, Float) [function, smt-hook(fp.max), hook(FLOAT.max)]
| minFloat(Float, Float) [function, smt-hook(fp.min), hook(FLOAT.min)]
| sqrtFloat(Float) [function]
| maxValueFloat(precision: Int, exponentBits: Int) [function, hook(FLOAT.maxValue)]
| minValueFloat(precision: Int, exponentBits: Int) [function, hook(FLOAT.minValue)]
Compute whether a float is less than or equasl to, less than, greater than or
equal to, greater than, equal, or unequal to another float. Note that
X ==Float Y and X ==K Y might yield different values. The latter should be
used in cases where you want to compare whether two values of sort Float
contain the same term. The former should be used when you want to implement
the == operator of a programming language. In particular, NaN =/=Float NaN
is true, because NaN compares unequal to all values, including itself, in
IEEE 754 arithmetic. 0.0 ==Float -0.0 is also true.
syntax Bool ::= Float "<=Float" Float [function, smt-hook(fp.leq), hook(FLOAT.le)]
| Float "<Float" Float [function, smt-hook(fp.lt), hook(FLOAT.lt)]
| Float ">=Float" Float [function, smt-hook(fp.geq), hook(FLOAT.ge)]
| Float ">Float" Float [function, smt-hook(fg.gt), hook(FLOAT.gt)]
| Float "==Float" Float [function, comm, smt-hook(fp.eq), hook(FLOAT.eq), symbol(_==Float_)]
| Float "=/=Float" Float [function, comm, smt-hook((not (fp.eq #1 #2)))]
rule F1:Float =/=Float F2:Float => notBool (F1 ==Float F2)
You can convert an integer to a floating-point number with the specified
precision and exponent range. You can also convert a floating-point number
to the nearest integer. This operation rounds to the nearest integer, but it
also avoids the double-rounding that is present in ceilFloat and floorFloat
if the nearest integer is not representable in the specified floating-point
type.
syntax Float ::= Int2Float(Int, precision: Int, exponentBits: Int) [function, hook(FLOAT.int2float)]
syntax Int ::= Float2Int(Float) [function, total, hook(FLOAT.float2int)]
The remainder of this section consists of an implementation in K of some of the operators above.
rule sqrtFloat(F:Float) => rootFloat(F, 2)
rule isInfinite(F:Float) => F >Float maxValueFloat(precisionFloat(F), exponentBitsFloat(F)) orBool F <Float --Float maxValueFloat(precisionFloat(F), exponentBitsFloat(F))
endmodule
Provided here is the syntax of an implementation of Unicode strings in K. This type is hooked to an implementation of strings provided by the backend. The implementation is currently incomplete and does not fully support encodings and code points beyond the initial 256 code points of the Basic Latin and Latin-1 Supplement blocks. In the future, there may be breaking changes to the semantics of this module in order to support this functionality.
The syntax of strings in K is delineated by double quotes. Inside the double quotes, any character can appear verbatim except double quotes, backslash, newline, and carriage return. K also supports the following escape sequences:
- " - the " character
- \ - the \ character
- \n - newline character
- \r - carriage return character
- \t - tab character
- \f - form feed character
- \xFF - \x followed by two hexadecimal characters indicates a code point between 0x00 and 0xff
- \uFFFF - \u followed by four hexadecimal characters indicates a code point between 0x0000 and 0xffff
- \UFFFFFFFF - \U followed by eight hexadecimal characters indicates a code point between 0x000000 and 0x10ffff
module STRING-SYNTAX
syntax String [hook(STRING.String)]
syntax String ::= r"[\\\"](([^\\\"\\n\\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]" [token]
endmodule
module STRING-COMMON
imports STRING-SYNTAX
imports private INT
imports private FLOAT-SYNTAX
imports private K-EQUAL
imports private BOOL
You can concatenate two strings in O(N) time. For successive concatenation
operations, it may be better to use the STRING-BUFFER module.
syntax String ::= String "+String" String [function, total, left, hook(STRING.concat)]
You can get the length of a string in O(1) time.
syntax Int ::= lengthString ( String ) [function, total, hook(STRING.length)]
You can convert between a character (as represented by a string containing a single code point) and an integer in O(1) time.
syntax String ::= chrChar ( Int ) [function, hook(STRING.chr)]
syntax Int ::= ordChar ( String ) [function, hook(STRING.ord)]
You can compute a substring of a string in O(N) time (where N is the length of the substring). There are two important facts to note:
- the range generated includes the character at
startIndexbut excludes the character atendIndex, i.e., the range is[startIndex..endIndex). - this function is only defined on valid indices (i.e., it is defined when
startIndex < endIndexandendIndexis less than or equal to the string length).
syntax String ::= substrString ( String , startIndex: Int , endIndex: Int ) [function, total, hook(STRING.substr)]
You can find the first (respectively, last) occurrence of a substring, starting
at a certain index, in another string in O(N*M) time.
Returns -1 if the substring is not found.
syntax Int ::= findString ( haystack: String , needle: String , index: Int ) [function, hook(STRING.find)]
syntax Int ::= rfindString ( haystack: String , needle: String , index: Int ) [function, hook(STRING.rfind)]
You can find the first (respectively, last) occurrence of one of the characters
of the search string, starting at a certain index, in another string in
O(N*M) time.
syntax Int ::= findChar ( haystack: String , needles: String , index: Int ) [function, hook(STRING.findChar)]
syntax Int ::= rfindChar ( haystack: String , needles: String , index: Int ) [function, hook(STRING.rfindChar)]
syntax String ::= Bool2String(Bool) [function, total]
rule Bool2String(true) => "true"
rule Bool2String(false) => "false"
syntax Bool ::= String2Bool(String) [function]
rule String2Bool("true") => true
rule String2Bool("false") => false
You can convert between a String and a Float. The String will be
represented in the syntax of the Float sort (see the section on the FLOAT
module above for details of that syntax). Which particular string is returned
by Float2String is determined by the backend, but the same Float is
guaranteed to return the same String, and converting that String back to a
Float is guaranteed to return the original Float.
You can also convert a Float to a string in a particular syntax using the
variant of Float2String with a format. In this case, the resulting string
is one which results directly from passing that format to mpfr_printf. This
functionality may not be supported on backends that do not use Gnu MPFR to
implement floating-point numbers.
syntax String ::= Float2String ( Float ) [function, total, hook(STRING.float2string)]
syntax String ::= Float2String ( Float , format: String ) [function, symbol(FloatFormat), hook(STRING.floatFormat)]
syntax Float ::= String2Float ( String ) [function, hook(STRING.string2float)]
You can convert between a String and an Int. The String will be represented
in the syntax of the INT module (i.e., a nonempty sequence of digits
optionally prefixed by a sign). When converting from an Int to a String,
the sign will not be present unless the integer is negative.
You can also convert between a String and an Int in a particular radix.
This radix can be anywhere between 2 and 36. For a radix 2 <= N <= 10, the
digits 0 to N-1 will be used. For a radix 11 <= N <= 36, the digits 0 to 9
and the first N-10 letters of the Latin alphabet will be used. Both uppercase
and lowercase letters are supported by String2Base. Whether the letters
returned by Base2String are upper or lowercase is determined by the backend,
but the backend will consistently choose one or the other.
syntax Int ::= String2Int ( String ) [function, hook(STRING.string2int)]
syntax String ::= Int2String ( Int ) [function, total, hook(STRING.int2string)]
syntax String ::= Base2String ( Int , base: Int ) [function, hook(STRING.base2string)]
syntax Int ::= String2Base ( String , base: Int ) [function, hook(STRING.string2base)]
You can replace one, some, or all occurrences of a string within another
string in O(N*M) time. The replaceAll, replace, and replaceFirst methods
are identical, except replaceFirst replaces exactly one ocurrence of the
string, the first occurrence. replace replaces the first times occurrences.
And replaceAll replaces every occurrence.
You can also count the number of times a string occurs within another string
using countAllOccurrences.
syntax String ::= "replaceAll" "(" haystack: String "," needle: String "," replacement: String ")" [function, total, hook(STRING.replaceAll)]
syntax String ::= "replace" "(" haystack: String "," needle: String "," replacement: String "," times: Int ")" [function, hook(STRING.replace)]
syntax String ::= "replaceFirst" "(" haystack: String "," needle: String "," replacement: String ")" [function, total, hook(STRING.replaceFirst)]
syntax Int ::= "countAllOccurrences" "(" haystack: String "," needle: String ")" [function, total, hook(STRING.countAllOccurrences)]
You can compare whether two strings are equal or unequal, or whether one string is less than, less than or equal to, greater than, or greater than or equal to another according to the natural lexicographic ordering of strings.
syntax Bool ::= String "==String" String [function, total, comm, hook(STRING.eq)]
| String "=/=String" String [function, total, comm, hook(STRING.ne)]
rule S1:String =/=String S2:String => notBool (S1 ==String S2)
syntax Bool ::= String "<String" String [function, total, hook(STRING.lt)]
| String "<=String" String [function, total, hook(STRING.le)]
| String ">String" String [function, total, hook(STRING.gt)]
| String ">=String" String [function, total, hook(STRING.ge)]
What follows is a few String hooks which are deprecated and only are supported on certain outdated backends of K, as well as an implementation of several of the above operations in K.
syntax String ::= categoryChar(String) [function, hook(STRING.category)]
| directionalityChar(String) [function, hook(STRING.directionality)]
syntax String ::= "newUUID" [function, hook(STRING.uuid), impure]
rule S1:String <=String S2:String => notBool (S2 <String S1)
rule S1:String >String S2:String => S2 <String S1
rule S1:String >=String S2:String => notBool (S1 <String S2)
rule findChar(S1:String, S2:String, I:Int) => #if findString(S1, substrString(S2, 0, 1), I) ==Int -1 #then findChar(S1, substrString(S2, 1, lengthString(S2)), I) #else #if findChar(S1, substrString(S2, 1, lengthString(S2)), I) ==Int -1 #then findString(S1, substrString(S2, 0, 1), I) #else minInt(findString(S1, substrString(S2, 0, 1), I), findChar(S1, substrString(S2, 1, lengthString(S2)), I)) #fi #fi requires S2 =/=String ""
rule findChar(_, "", _) => -1
rule rfindChar(S1:String, S2:String, I:Int) => maxInt(rfindString(S1, substrString(S2, 0, 1), I), rfindChar(S1, substrString(S2, 1, lengthString(S2)), I)) requires S2 =/=String ""
rule rfindChar(_, "", _) => -1
rule countAllOccurrences(Source:String, ToCount:String) => 0
requires findString(Source, ToCount, 0) <Int 0
rule countAllOccurrences(Source:String, ToCount:String) => 1 +Int countAllOccurrences(substrString(Source, findString(Source, ToCount, 0) +Int lengthString(ToCount), lengthString(Source)), ToCount)
requires findString(Source, ToCount, 0) >=Int 0
rule replaceFirst(Source:String, ToReplace:String, Replacement:String) => substrString(Source, 0, findString(Source, ToReplace, 0))
+String Replacement +String substrString(Source, findString(Source, ToReplace, 0) +Int lengthString(ToReplace), lengthString(Source))
requires findString(Source, ToReplace, 0) >=Int 0
rule replaceFirst(Source:String, ToReplace:String, _:String) => Source
requires findString(Source, ToReplace, 0) <Int 0
// Note that the replace function is undefined when Count < 0. This allows different backends to
// implement their own behavior without contradicting these semantics. For instance, a symbolic
// backend can return #Bottom for that case, while a concrete backend can throw an exception.
rule replace(Source:String, ToReplace:String, Replacement:String, Count:Int) =>
substrString(Source, 0, findString(Source, ToReplace, 0)) +String Replacement +String
replace(substrString(Source, findString(Source, ToReplace, 0) +Int lengthString(ToReplace), lengthString(Source)), ToReplace, Replacement, Count -Int 1)
requires Count >Int 0 andBool findString(Source, ToReplace, 0) >=Int 0
rule replace(Source:String, _, _, Count) => Source
requires Count >=Int 0 [owise]
rule replaceAll(Source:String, ToReplace:String, Replacement:String) => replace(Source, ToReplace, Replacement, countAllOccurrences(Source, ToReplace))
endmodule
module STRING-KORE [symbolic]
imports private K-EQUAL
imports STRING-COMMON
rule S1:String ==K S2:String => S1 ==String S2 [simplification]
endmodule
module STRING
imports STRING-COMMON
imports STRING-KORE
endmodule
It is a well known fact that repeated string concatenations are quadratic
in performance whereas use of an efficient mutable representation of arrays
can yield linear performance. We thus provide such a sort, the StringBuffer
sort. Axiomatically, it is implemented below on symbolic backends using the
String module. However, on concrete backends it provides an efficient
implementation of string concatenation. There are three operations:
.StringBuffercreates a newStringBufferwith current content equal to the empty string.+Stringtakes aStringBufferand aStringand appends theStringto the end of theStringBufferStringBuffer2Stringconverts aStringBufferto aString. This operation copies the string so that subsequent modifications to theStringBufferwill not change the value of theStringreturned by this function.
module STRING-BUFFER-IN-K [symbolic]
imports private BASIC-K
imports STRING
syntax StringBuffer ::= ".StringBuffer" [function, total]
syntax StringBuffer ::= StringBuffer "+String" String [function, total, avoid]
syntax StringBuffer ::= String
syntax String ::= StringBuffer2String ( StringBuffer ) [function, total]
rule {SB:String +String S:String}::StringBuffer => (SB +String S)::String
rule .StringBuffer => ""
rule StringBuffer2String(S:String) => S
endmodule
module STRING-BUFFER-HOOKED [concrete]
imports private BASIC-K
imports STRING
syntax StringBuffer [hook(BUFFER.StringBuffer)]
syntax StringBuffer ::= ".StringBuffer" [function, total, hook(BUFFER.empty), impure]
syntax StringBuffer ::= StringBuffer "+String" String [function, total, hook(BUFFER.concat), avoid]
syntax String ::= StringBuffer2String ( StringBuffer ) [function, total, hook(BUFFER.toString)]
endmodule
module STRING-BUFFER
imports STRING-BUFFER-HOOKED
imports STRING-BUFFER-IN-K
endmodule
Provided here is the syntax of an implementation of fixed-width arrays of Bytes
in K. This type is hooked to an implementation of bytes provided by the backend.
On the LLVM backend, it is possible to opt in to a faster, mutable
representation (using the --llvm-mutable-bytes flag to kompile) where
multiple references can occur to the same Bytes object and when one is
modified, the others are also modified. Care should be taken when using this
feature, however, as it is possible to experience divergent behavior with
symbolic backends unless the Bytes type is used in a manner that preserves
consistency.
module BYTES-SYNTAX
imports private STRING-SYNTAX
syntax Bytes [hook(BYTES.Bytes)]
syntax Bytes ::= r"b[\\\"](([ !#-\\[\\]-~])|([\\\\][tnfr\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2}))*[\\\"]" [token]
endmodule
module BYTES-STRING-ENCODE [symbolic]
imports BYTES-SYNTAX
You can encode/decode between Bytes and String using UTF-8, UTF-16LE, UTF-16BE, UTF-32LE, and UTF-32BE
syntax String ::= decodeBytes ( encoding: String , contents: Bytes ) [function, hook(BYTES.decodeBytes)]
syntax Bytes ::= encodeBytes ( encoding: String , contents: String ) [function, hook(BYTES.encodeBytes)]
endmodule
module BYTES-HOOKED
imports STRING-SYNTAX
imports BYTES-SYNTAX
imports BYTES-STRING-ENCODE
The byte array of length zero is represented by .Bytes.
syntax Bytes ::= ".Bytes" [function, total, hook(BYTES.empty)]
When converting to/from an integer, byte arrays can be treated as either little endian (ie, least significant byte first) or big endian (ie, most significant byte first).
syntax Endianness ::= "LE" [symbol(littleEndianBytes)]
| "BE" [symbol(bigEndianBytes)]
When converting to/from an integer, byte arrays can be treated as either signed or unsigned.
syntax Signedness ::= "Signed" [symbol(signedBytes)]
| "Unsigned" [symbol(unsignedBytes)]
You can convert from a Bytes to an Int. In order to do this, the endianness
and signedness of the Bytes must be provided. The resulting integer is
created by means of interpreting the Bytes as either a twos-complement
representation, or an unsigned representation, of an integer, in the specified
byte order.
You can also convert from an Int to a Bytes. This comes in two variants.
In the first, the length of the resulting Bytes in bytes is explicitly
specified. If the length is greater than the highest set bit in the magnitude
of the integer, the result is padded with 0 bits if the number is positive
and 1 bits if the number is negative. If the length is less than the highest
bit set in the magnitude of the integer, the most-significant bits of the
integer will be truncated. The endianness of the resulting Bytes object
is as specified.
In the second variant, both endianness and signedness are specified, and
the resulting Bytes object will be the smallest number of bytes necessary
for the resulting Bytes object to be convertible back to the original integer
via Bytes2Int. In other words, if the highest bit set in the magnitude of the
integer is N, then the byte array will be at least N+1 bits long, rounded up
to the nearest byte.
syntax Int ::= Bytes2Int(Bytes, Endianness, Signedness) [function, total, hook(BYTES.bytes2int)]
syntax Bytes ::= Int2Bytes(length: Int, Int, Endianness) [function, total, hook(BYTES.int2bytes)]
| Int2Bytes(Int, Endianness, Signedness) [function, total, symbol(Int2BytesNoLen)]
You can convert between a Bytes and a String in O(N) time. The resulting
value is a copy of the original and will not be affected by subsequent
mutations of the input or output value.
syntax String ::= Bytes2String(Bytes) [function, total, hook(BYTES.bytes2string)]
syntax Bytes ::= String2Bytes(String) [function, total, hook(BYTES.string2bytes)]
You can set the value of a particular byte in a Bytes object in O(1) time.
The result is #False if value is not in the range [0..255] or if index
is not a valid index (ie, less than zero or greater than or equal to the length
of the Bytes term).
syntax Bytes ::= Bytes "[" index: Int "<-" value: Int "]" [function, hook(BYTES.update)]
You can get the value of a particular byte in a Bytes object in O(1) time.
The result is #False if index is not a valid index (see above).
syntax Int ::= Bytes "[" Int "]" [function, hook(BYTES.get)]
You can get a new Bytes object containing a range of bytes from the input
Bytes in O(N) time (where N is the length of the substring). The range
of bytes included is [startIndex..endIndex). The resulting Bytes is
a copy and mutations to it do not affect mutations to the original Bytes.
The result is #False if startIndex or endIndex are not valid.
syntax Bytes ::= substrBytes(Bytes, startIndex: Int, endIndex: Int) [function, hook(BYTES.substr)]
You can modify a Bytes to return a Bytes which is equal to dest except the
N elements starting at index are replaced with the contents of src in O(N)
time. If --llvm-mutable-bytes is active, this will not create a new Bytes
object and will instead modify the original on concrete backends. The result is
#False if index + N is not a valid index.
syntax Bytes ::= replaceAtBytes(dest: Bytes, index: Int, src: Bytes) [function, hook(BYTES.replaceAt)]
You can modify a Bytes to return a Bytes which is equal to dest except the
count bytes starting at index are replaced with count bytes of value
Int2Bytes(1, v, LE/BE) in O(count) time. This does not create a new Bytes
object and will instead modify the original if --llvm-mutable-bytes is active.
This will throw an exception if index + count is not a valid index. The
acceptable range of values for v is -128 to 127. This will throw an exception
if v is outside of this range. This is implemented only for the LLVM backend.
syntax Bytes ::= memsetBytes(dest: Bytes, index: Int, count: Int, v: Int) [function, hook(BYTES.memset)]
You can create a new Bytes object which is at least length bytes long by
taking the input sequence and padding it on the right (respectively, on the
left) with the specified value. If --llvm-mutable-bytes is active, this does
not create a new Bytes object if the input is already at least length bytes
long, and will instead return the input unchanged. The result is #False if
value is not in the range [0..255], or if the length is negative.
syntax Bytes ::= padRightBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padRight)]
| padLeftBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padLeft)]
You can reverse a Bytes object in O(N) time. If --llvm-mutable-bytes is
active, this will not create a new Bytes object and will instead modify the
original.
syntax Bytes ::= reverseBytes(Bytes) [function, total, hook(BYTES.reverse)]
You can get the length of a Bytes term in O(1) time.
syntax Int ::= lengthBytes(Bytes) [function, total, hook(BYTES.length), smtlib(lengthBytes)]
You can create a new Bytes object by concatenating two Bytes objects
together in O(N) time.
syntax Bytes ::= Bytes "+Bytes" Bytes [function, total, hook(BYTES.concat), right]
endmodule
The remainder of this module consists of an implementation of some of the operators listed above in K.
module BYTES-CONCRETE [concrete]
imports BYTES-HOOKED
endmodule
module BYTES-KORE
imports BYTES-HOOKED
imports BYTES-SYMBOLIC-CEIL
endmodule
module BYTES-SYMBOLIC-CEIL [symbolic]
imports BYTES-HOOKED
imports private INT
imports private BOOL
rule #Ceil(padRightBytes(_, LEN, VAL)) => {(0 <=Int LEN andBool 0 <=Int VAL andBool VAL <Int 256) #Equals true} [simplification]
rule #Ceil(padLeftBytes(_, LEN, VAL)) => {(0 <=Int LEN andBool 0 <=Int VAL andBool VAL <Int 256) #Equals true} [simplification]
endmodule
module BYTES
imports BYTES-CONCRETE
imports BYTES-KORE
imports private INT
rule Int2Bytes(I::Int, _::Endianness, _) => .Bytes
requires I ==Int 0
rule Int2Bytes(I::Int, E::Endianness, Unsigned) => Int2Bytes((log2Int(I) +Int 8) /Int 8, I, E)
requires I >Int 0 [preserves-definedness]
rule Int2Bytes(I::Int, E::Endianness, Signed ) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E)
requires I >Int 0 [preserves-definedness]
rule Int2Bytes(I::Int, E::Endianness, Signed ) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E)
requires I <Int -1 [preserves-definedness]
rule Int2Bytes(I::Int, E::Endianness, Signed ) => Int2Bytes(1, -1, E)
requires I ==Int -1 [preserves-definedness]
endmodule
Provided here is an implementation for program identifiers in K. Developers of semantics for a particular language may wish to use their own implementation instead of the one provided here if their syntax differs from the syntax defined below. However, this is provided for convenience for developers who do not care about the lexical syntax of identifiers.
Provided are the following pieces of functionality:
Id2String- Convert anIdto aStringcontaining its nameString2Id- Convert aStringto anIdwith the specified name- !X:Id - You can get a fresh identifier distinct from any previous identifier generated by this syntax.
module ID-SYNTAX-PROGRAM-PARSING
imports BUILTIN-ID-TOKENS
syntax Id ::= r"[A-Za-z\\_][A-Za-z0-9\\_]*" [prec(1), token]
| #LowerId [token]
| #UpperId [token]
endmodule
module ID-SYNTAX
syntax Id [token]
endmodule
module ID-COMMON
imports ID-SYNTAX
imports private STRING
syntax String ::= Id2String ( Id ) [function, total, hook(STRING.token2string)]
syntax Id ::= String2Id (String) [function, total, hook(STRING.string2token)]
syntax Id ::= freshId(Int) [freshGenerator, function, total, private]
rule freshId(I:Int) => String2Id("_" +String Int2String(I))
endmodule
module ID
imports ID-COMMON
endmodule
Provided here are implementations of two important primitives in K:
==K- the equality between two terms. Returnstrueif they are equal andfalseif they are not equal.#if #then #else #fi- polymorphic conditional function. If the first argument evaluates totrue, the second argument is returned. Otherwise, the third argument is returned. Note that this does not short-circuit on symbolic backends.
module K-EQUAL-SYNTAX
imports private BOOL
imports private BASIC-K
syntax Bool ::= left:
K "==K" K [function, total, comm, smt-hook(=), hook(KEQUAL.eq), symbol(_==K_), group(equalEqualK)]
| K "=/=K" K [function, total, comm, smt-hook(distinct), hook(KEQUAL.ne), symbol(_=/=K_), group(notEqualEqualK)]
syntax priority equalEqualK notEqualEqualK > boolOperation mlOp
syntax {Sort} Sort ::= "#if" Bool "#then" Sort "#else" Sort "#fi" [function, total, symbol(ite), smt-hook(ite), hook(KEQUAL.ite)]
endmodule
module K-EQUAL-KORE [symbolic]
imports private BOOL
imports K-EQUAL-SYNTAX
rule K1:Bool ==K K2:Bool => K1 ==Bool K2 [simplification]
rule {K1 ==K K2 #Equals true} => {K1 #Equals K2} [simplification]
rule {true #Equals K1 ==K K2} => {K1 #Equals K2} [simplification]
rule {K1 ==K K2 #Equals false} => #Not({K1 #Equals K2}) [simplification]
rule {false #Equals K1 ==K K2} => #Not({K1 #Equals K2}) [simplification]
rule {K1 =/=K K2 #Equals true} => #Not({K1 #Equals K2}) [simplification]
rule {true #Equals K1 =/=K K2} => #Not({K1 #Equals K2}) [simplification]
rule {K1 =/=K K2 #Equals false} => {K1 #Equals K2} [simplification]
rule {false #Equals K1 =/=K K2} => {K1 #Equals K2} [simplification]
endmodule
module K-EQUAL
imports private BOOL
imports K-EQUAL-SYNTAX
imports K-EQUAL-KORE
rule K1:K =/=K K2:K => notBool (K1 ==K K2)
rule #if C:Bool #then B1::K #else _ #fi => B1 requires C
rule #if C:Bool #then _ #else B2::K #fi => B2 requires notBool C
endmodule
Provided below are a few miscellaneous, mostly deprecated functions in K. It is not recommended to use any of them directly as they are largely unsupported in modern K. There are a few exceptions:
#getenv- Returns the value of an environment variable#kompiledDirectory- Returns the path to the current compiled K definition directory.#unparseKORE- Takes a K term and converts it to a string.
module K-REFLECTION
imports BASIC-K
imports STRING
syntax K ::= "#configuration" [function, impure, hook(KREFLECTION.configuration)]
syntax String ::= #sort(K) [function, hook(KREFLECTION.sort)]
syntax KItem ::= #fresh(String) [function, hook(KREFLECTION.fresh), impure]
syntax KItem ::= getsymbol(K) [function, hook(KREFLECTION.getKLabel)]
syntax K ::= #getenv(String) [function, impure, hook(KREFLECTION.getenv)]
syntax String ::= #kompiledDirectory() [function, hook(KREFLECTION.kompiledDir)]
// meaningful only for the purposes of compilation to a binary, otherwise
// undefined
syntax List ::= #argv() [function, hook(KREFLECTION.argv)]
syntax {Sort} String ::= #unparseKORE(Sort) [function, hook(KREFLECTION.printKORE)]
syntax IOError ::= "#noParse" "(" String ")" [symbol(#noParse)]
endmodule
Concrete execution in K supports I/O operations. This functionality is not supported during symbolic execution, because symbolic execution must exist completely free of side-effects, and I/O is an irreducible type of side effect. However, it is useful in many cases when defining concrete execution to be able to make reference to I/O operations.
The design of these I/O operations is based on the POSIX standard, for the most
part. For example, the #read K function maps to the read POSIX function. We
do not at this time have a higher-level API for I/O, but this may be
implemented at some point in the future.
I/O operations generally return either their result, or an IOError term
corresponding to the errno returned by the underlying system call.
module K-IO
imports private LIST
imports private STRING
imports private INT
Aside from EOF, which is returned by #getc if the file is at end-of-file, all
of the below I/O errors correspond to possible values for errno after calling
a library function. If the errno returned is not one of the below errnos
known to K, #unknownIOError is returned along with the integer errno value.
syntax IOError ::= "#EOF" [symbol(#EOF)]
| #unknownIOError(errno: Int) [symbol(#unknownIOError)]
| "#E2BIG" [symbol(#E2BIG)]
| "#EACCES" [symbol(#EACCES)]
| "#EAGAIN" [symbol(#EAGAIN)]
| "#EBADF" [symbol(#EBADF)]
| "#EBUSY" [symbol(#EBUSY)]
| "#ECHILD" [symbol(#ECHILD)]
| "#EDEADLK" [symbol(#EDEADLK)]
| "#EDOM" [symbol(#EDOM)]
| "#EEXIST" [symbol(#EEXIST)]
| "#EFAULT" [symbol(#EFAULT)]
| "#EFBIG" [symbol(#EFBIG)]
| "#EINTR" [symbol(#EINTR)]
| "#EINVAL" [symbol(#EINVAL)]
| "#EIO" [symbol(#EIO)]
| "#EISDIR" [symbol(#EISDIR)]
| "#EMFILE" [symbol(#EMFILE)]
| "#EMLINK" [symbol(#EMLINK)]
| "#ENAMETOOLONG" [symbol(#ENAMETOOLONG)]
| "#ENFILE" [symbol(#ENFILE)]
| "#ENODEV" [symbol(#ENODEV)]
| "#ENOENT" [symbol(#ENOENT)]
| "#ENOEXEC" [symbol(#ENOEXEC)]
| "#ENOLCK" [symbol(#ENOLCK)]
| "#ENOMEM" [symbol(#ENOMEM)]
| "#ENOSPC" [symbol(#ENOSPC)]
| "#ENOSYS" [symbol(#ENOSYS)]
| "#ENOTDIR" [symbol(#ENOTDIR)]
| "#ENOTEMPTY" [symbol(#ENOTEMPTY)]
| "#ENOTTY" [symbol(#ENOTTY)]
| "#ENXIO" [symbol(#ENXIO)]
| "#EPERM" [symbol(#EPERM)]
| "#EPIPE" [symbol(#EPIPE)]
| "#ERANGE" [symbol(#ERANGE)]
| "#EROFS" [symbol(#EROFS)]
| "#ESPIPE" [symbol(#ESPIPE)]
| "#ESRCH" [symbol(#ESRCH)]
| "#EXDEV" [symbol(#EXDEV)]
| "#EWOULDBLOCK" [symbol(#EWOULDBLOCK)]
| "#EINPROGRESS" [symbol(#EINPROGRESS)]
| "#EALREADY" [symbol(#EALREADY)]
| "#ENOTSOCK" [symbol(#ENOTSOCK)]
| "#EDESTADDRREQ" [symbol(#EDESTADDRREQ)]
| "#EMSGSIZE" [symbol(#EMSGSIZE)]
| "#EPROTOTYPE" [symbol(#EPROTOTYPE)]
| "#ENOPROTOOPT" [symbol(#ENOPROTOOPT)]
| "#EPROTONOSUPPORT" [symbol(#EPROTONOSUPPORT)]
| "#ESOCKTNOSUPPORT" [symbol(#ESOCKTNOSUPPORT)]
| "#EOPNOTSUPP" [symbol(#EOPNOTSUPP)]
| "#EPFNOSUPPORT" [symbol(#EPFNOSUPPORT)]
| "#EAFNOSUPPORT" [symbol(#EAFNOSUPPORT)]
| "#EADDRINUSE" [symbol(#EADDRINUSE)]
| "#EADDRNOTAVAIL" [symbol(#EADDRNOTAVAIL)]
| "#ENETDOWN" [symbol(#ENETDOWN)]
| "#ENETUNREACH" [symbol(#ENETUNREACH)]
| "#ENETRESET" [symbol(#ENETRESET)]
| "#ECONNABORTED" [symbol(#ECONNABORTED)]
| "#ECONNRESET" [symbol(#ECONNRESET)]
| "#ENOBUFS" [symbol(#ENOBUFS)]
| "#EISCONN" [symbol(#EISCONN)]
| "#ENOTCONN" [symbol(#ENOTCONN)]
| "#ESHUTDOWN" [symbol(#ESHUTDOWN)]
| "#ETOOMANYREFS" [symbol(#ETOOMANYREFS)]
| "#ETIMEDOUT" [symbol(#ETIMEDOUT)]
| "#ECONNREFUSED" [symbol(#ECONNREFUSED)]
| "#EHOSTDOWN" [symbol(#EHOSTDOWN)]
| "#EHOSTUNREACH" [symbol(#EHOSTUNREACH)]
| "#ELOOP" [symbol(#ELOOP)]
| "#EOVERFLOW" [symbol(#EOVERFLOW)]
Here we see sorts defined to contain either an Int or an IOError, or
either a String or an IOError. These sorts are used to implement the
return sort of functions that may succeed, in which case they return a value,
or may fail, in which case their return value indicates an error and the
error indicated is returned via errno.
syntax IOInt ::= Int | IOError
syntax IOString ::= String | IOError
You can open a file in K using #open. An optional mode indicates the file
open mode, which can have any value allowed by the fopen function in C.
The returned value is the file descriptor that was opened, or an error.
syntax IOInt ::= "#open" "(" path: String ")" [function]
| "#open" "(" path: String "," mode: String ")" [function, hook(IO.open), impure]
rule #open(S:String) => #open(S:String, "r+")
You can get the current offset in a file using #tell. You can also seek
to a particular offset using #seek or #seekEnd. #seek is implemented via
a call to lseek with the SEEK_SET whence. #seekEnd is implemented via a
call to lseek with the SEEK_END whence. You can emulate the SEEK_CUR
whence by means of #seek(FD, #tell(FD) +Int Offset).
syntax IOInt ::= "#tell" "(" fd: Int ")" [function, hook(IO.tell), impure]
syntax K ::= "#seek" "(" fd: Int "," index: Int ")" [function, hook(IO.seek), impure]
| "#seekEnd" "(" fd: Int "," fromEnd: Int ")" [function, hook(IO.seekEnd), impure]
You can read a single character from a file using #getc. #EOF is returned
if you are at end-of-fie.
You can also read up to length characters in a file using #read. The
resulting read characters are returned, which may be fewer characters than
requested. A string of zero length being returned indicates end-of-file.
syntax IOInt ::= "#getc" "(" fd: Int ")" [function, hook(IO.getc), impure]
syntax IOString ::= "#read" "(" fd: Int "," length: Int ")" [function, hook(IO.read), impure]
You can write a single character to a file using #putc. You can also write
a string to a file using #write. The returned value on success is .K.
syntax K ::= "#putc" "(" fd: Int "," value: Int ")" [function, hook(IO.putc), impure]
| "#write" "(" fd: Int "," value: String ")" [function, hook(IO.write), impure]
You can close a file using #close. The returned value on success is .K.
syntax K ::= "#close" "(" fd: Int ")" [function, hook(IO.close), impure]
You can lock or unlock parts of a file using the #lock and #unlock
functions. The lock starts at the beginning of the file and continues for
endIndex bytes. Note that Unix systems do not actually prevent locked files
from being read and modified; you will have to lock both sides of a concurrent
access to guarantee exclusivity.
syntax K ::= "#lock" "(" fd: Int "," endIndex: Int ")" [function, hook(IO.lock), impure]
| "#unlock" "(" fd: Int "," endIndex: Int ")" [function, hook(IO.unlock), impure]
You can accept a connection on a socket using #accept, or shut down the
write end of a socket with #shutdownWrite. Note that facility is not provided
for opening, binding, and listening on sockets. These functions are implemented
in order to support creating stateful request/response servers where the
request loop is implemented using rewriting in K, but the connection
initialization is written in native code and linked into the LLVM backend.
syntax IOInt ::= "#accept" "(" fd: Int ")" [function, hook(IO.accept), impure]
syntax K ::= "#shutdownWrite" "(" fd: Int ")" [function, hook(IO.shutdownWrite), impure]
You can get the current time in seconds since midnight UTC on January 1, 1970
using #time.
syntax Int ::= "#time" "(" ")" [function, hook(IO.time), impure]
Provided here are functions that return the file descriptor for standard input, standard output, and standard error.
syntax Int ::= "#stdin" [function, total]
| "#stdout" [function, total]
| "#stderr" [function, total]
rule #stdin => 0
rule #stdout => 1
rule #stderr => 2
You can execute a command using the shell using the #system operator. Care
must be taken to sanitize inputs to this function or security issues may
result. Note that K has no facility for reasoning about logic that happens
outside its process, so any functionality that you wish to be able to formally
reason about in K should not be implemented via the #system operator.
syntax KItem ::= #system ( String ) [function, hook(IO.system), impure]
| "#systemResult" "(" Int /* exit code */ "," String /* stdout */ "," String /* stderr */ ")" [symbol(#systemResult)]
You can get a temporary file and open it atomically using the #mkstemp
operator. The resulting file will be closed and deleted when K rewriting ends.
For more info on the argument to #mkstemp, see man mkstemp.
syntax IOFile ::= #mkstemp(template: String) [function, hook(IO.mkstemp), impure]
syntax IOFile ::= IOError
| "#tempFile" "(" path: String "," fd: Int ")" [symbol(#tempFile)]
You can delete a file using its absolute or relative path using the #remove
operator. It returns .K on success or an IOError on failure.
syntax K ::= #remove(path: String) [function, total, hook(IO.remove), impure]
You can log information to disk using the #logToFile operator. Semantically,
this operator returns .K. However, it has a side effect that is not reasoned
about which is that value will be written to a uniquely-identified file
containing name in its name. The file is only flushed to disk when rewriting
finishes.
syntax K ::= #logToFile(name: String, value: String) [function, total, hook(IO.log), impure, returnsUnit, symbol(#logToFile)]
Strings can also be logged via the logging mechanisms available to the backend. On the LLVM backend, this just means logging the text to standard error. On the Haskell backend, a log message of type InfoUserLog is created with the specified text.
syntax K ::= #log(value: String) [function, total, hook(IO.logString), impure, returnsUnit, symbol(#log)]
Terms can also be logged to standard error in surface syntax, rather than as
KORE using #trace. This operator has similar semantics to #logToFile (i.e.
it returns .K, but prints as an impure side effect). Note that calling
#trace is equivalent to invoking the kprint tool for the first term that is
logged, which requires re-parsing the underlying K definition. Subsequent calls
do not incur this overhead again; the definition is cached.
syntax K ::= #trace(value: KItem) [function, total, hook(IO.traceTerm), impure, returnsUnit, symbol(#trace)]
| #traceK(value: K) [function, total, hook(IO.traceTerm), impure, returnsUnit, symbol(#traceK)]
Below is an implementation of the stream="stdin" and stream="stdout"
cell attributes in K. You should not refer to these symbols or modules directly
in your definition. It is provided only so that the K compiler can make use of
it. For more information on how to use this feature, refer to IMP++ in the K
tutorial.
syntax Stream ::= #buffer(K)
| #istream(Int)
| #parseInput(String, String)
| #ostream(Int)
endmodule
// NOTE: DO NOT DIRECTLY IMPORT *-STREAM MODULES
// These stream modules will be automatically instantiated and implicitly imported
// into the main module when `stream` attributes appear in configuration cells.
// Only `Stream` productions and `[stream]` rules will be imported.
// The cell name will be replaced with the one of the main configuration.
module STDIN-STREAM
imports K-IO
imports K-REFLECTION
imports LIST
imports INT
imports BOOL
configuration <stdin> ListItem(#buffer($STDIN:String)) ListItem($IO:String) ListItem(#istream(#stdin)) </stdin>
// read one character at a time until we read whitespace
rule [stdinGetc]:
<stdin>
ListItem(#parseInput(_:String, Delimiters:String))
ListItem(#buffer(S:String => S +String chrChar({#getc(N)}:>Int)))
ListItem("on")
ListItem(#istream(N:Int))
</stdin>
requires findChar(S, Delimiters, 0) ==Int -1 // [stdin]
[stream, priority(200)]
// when we reach whitespace, if it parses create a ListItem
rule [stdinParseString]:
<stdin>
(ListItem(#parseInput("String", Delimiters:String)) => ListItem(S))
ListItem(#buffer(S:String => ""))
_:List
</stdin>
requires findChar(S, Delimiters, 0) =/=Int -1 // [stdin]
[stream]
// a hack: handle the case when we read integers without the help of the IO server
rule [stdinParseInt]:
<stdin>
(ListItem(#parseInput("Int", Delimiters:String))
=> ListItem(String2Int(substrString(S, 0, findChar(S, Delimiters, 0)))))
ListItem(#buffer(S:String => substrString(S,findChar(S, Delimiters, 0) +Int 1, lengthString(S))))
_:List
</stdin>
requires findChar(S, Delimiters, 0) =/=Int -1
andBool lengthString(S) >Int 1 // [stdin]
[stream]
rule [stdinTrim]:
<stdin>
ListItem(#parseInput(Sort:String, Delimiters:String))
ListItem(#buffer(S:String => substrString(S, 1, lengthString(S))))
_:List
</stdin>
requires findChar(S, Delimiters, 0) =/=Int -1
andBool Sort =/=String "String"
andBool lengthString(S) <=Int 1 // [stdin]
[stream]
// NOTE: This unblocking rule will be instantiated and inserted carefully
// when necessary according to user-defined rules, since otherwise it will
// lead to a diverging (i.e., non-terminating) transition system definition.
// Currently, it supports only a simple pattern matching on the top of the
// input stream cell, e.g.,
// rule <k> read() => V ... </k> <in> ListItem(V:Int) => .List ... </in>
// Non-supported rules that refer to the input stream cell in a sophisticated
// way will get stuck in concrete execution mode with real IO enabled (i.e.,
// under `--io on` option), while they will still work in symbolic execution
// mode or concrete execution mode with real IO disabled (i.e., under `--io
// off`, `--search`, or `--debug` options).
//
// TODO: More patterns need to be supported as well. In that case, we need to
// have a way to specify such patterns.
rule [stdinUnblock]:
<stdin>
(.List => ListItem(#parseInput(?Sort:String, ?Delimiters:String)))
ListItem(#buffer(_:String))
...
</stdin>
/*
syntax Stream ::= "#noIO"
rule ListItem(#buffer(_))
(ListItem(#noIO) ListItem(#istream(_:Int)) => .List) [stdin]
*/
endmodule
module STDOUT-STREAM
imports K-IO
imports LIST
imports STRING
configuration <stdout> ListItem(#ostream(#stdout)) ListItem($IO:String) ListItem(#buffer("")) </stdout>
//configuration <stderr> ListItem(#ostream(#stderr)) ListItem($IO:String) ListItem(#buffer("")) </stderr>
rule [stdoutBufferFloat]:
<stdout>
ListItem(#ostream(_))
ListItem(_)
ListItem(#buffer(Buffer:String => Buffer +String Float2String(F)))
(ListItem(F:Float) => .List)
_:List
</stdout>
// [stdout, stderr]
[stream, priority(25)]
rule [stdoutBufferInt]:
<stdout>
ListItem(#ostream(_))
ListItem(_)
ListItem(#buffer(Buffer:String => Buffer +String Int2String(I)))
(ListItem(I:Int) => .List)
_:List
</stdout>
// [stdout, stderr]
[stream, priority(25)]
rule [stdoutBufferString]:
<stdout>
ListItem(#ostream(_))
ListItem(_)
ListItem(#buffer(Buffer:String => Buffer +String S))
(ListItem(S:String) => .List)
_:List
</stdout>
// [stdout, stderr]
[stream, priority(25)]
// Send first char from the buffer to the server
rule [stdoutWrite]:
<stdout>
ListItem(#ostream(N:Int => {#write(N, S) ~> N:Int}:>Int))
ListItem("on")
ListItem(#buffer(S:String => ""))
_:List
</stdout>
requires S =/=String "" // [stdout, stderr]
[stream, priority(30)]
/*
syntax Stream ::= "#noIO"
rule ListItem(#buffer(Buffer:String => Buffer +String Float2String(F)))
(ListItem(F:Float) => .List)
_:List [stdout, stderr]
rule ListItem(#buffer(Buffer:String => Buffer +String Int2String(I)))
(ListItem(I:Int) => .List)
_:List [stdout, stderr]
rule ListItem(#buffer(Buffer:String => Buffer +String S))
(ListItem(S:String) => .List)
_:List [stdout, stderr]
rule (ListItem(#ostream(_:Int)) ListItem(#noIO) => .List)
ListItem(#buffer(_))
_:List [stdout, stderr]
*/
endmodule
Provided here is an implementation of arbitrarily large fixed-precision binary
integers in K. This type is hooked to an implementation of integers provided
by the backend, and in particular makes use of native machine integers for
certain sizes of integer. For arbitrary-precision integers, see the INT
module above.
The syntax of machine integers in K is the same as arbitrary-precision integers
(i.e., an optional sign followed by a sequence of digits) except that machine
integers always end in a suffix pN where N is an integer indicating the
width in bits of the integer. The MInt sort is parametric, and this is
reflected in the literals. For example, the sort of 0p8 is MInt{8}.
module MINT-SYNTAX
/*@\section{Description} The MInt implements machine integers of arbitrary
* bit width represented in 2's complement. */
syntax {Width} MInt{Width} [hook(MINT.MInt)]
/*@ Machine integer of bit width and value. */
syntax {Width} MInt{Width} ::= r"[\\+\\-]?[0-9]+[pP][0-9]+" [token, prec(2), hook(MINT.literal)]
endmodule
module MINT
imports MINT-SYNTAX
imports private INT
imports private BOOL
You can get the number of bits of width in an MInt using bitwidthMInt.
syntax {Width} Int ::= bitwidthMInt(MInt{Width}) [function, total, hook(MINT.bitwidth)]
You can convert from an MInt to an Int using the MInt2Signed and
MInt2Unsigned functions. an MInt does not have a sign; its sign is instead
reflected in how operators interpret its value either as a signed integer or as
an unsigned integer. Thus, you can interpret a MInt as a signed integer witth
MInt2Signed, or as an unsigned integer respectively using MInt2Unsigned.
You can also convert from an Int to an MInt using Int2MInt. Care must
be given to ensure that the sort context where the Int2MInt operator appears
has the correct bitwidth, as this will influence the width of the resulting
MInt.
syntax {Width} Int ::= MInt2Signed(MInt{Width}) [function, total, hook(MINT.svalue)]
| MInt2Unsigned(MInt{Width}) [function, total, hook(MINT.uvalue), smt-hook(bv2int)]
syntax {Width} MInt{Width} ::= Int2MInt(Int) [function, total, hook(MINT.integer), smt-hook(int2bv)]
You can get the minimum and maximum values of a signed or unsigned MInt
with az specified bit width using sminMInt, smaxMInt, uminMInt, and
umaxMInt.
syntax Int ::= sminMInt(Int) [function]
| smaxMInt(Int) [function]
| uminMInt(Int) [function]
| umaxMInt(Int) [function]
rule sminMInt(N:Int) => 0 -Int (1 <<Int (N -Int 1))
rule smaxMInt(N:Int) => (1 <<Int (N -Int 1)) -Int 1
rule uminMInt(_:Int) => 0
rule umaxMInt(N:Int) => (1 <<Int N) -Int 1
You can check whether a specified Int will be represented in an MInt
with a specified width without any loss of precision when interpreted as
a signed or unsigned integer using soverflowMInt and uoverflowMInt.
syntax Bool ::= soverflowMInt(width: Int, Int) [function]
| uoverflowMInt(width: Int, Int) [function]
rule
soverflowMInt(N:Int, I:Int)
=>
I <Int sminMInt(N) orBool I >Int smaxMInt(N)
rule
uoverflowMInt(N:Int, I:Int)
=>
I <Int uminMInt(N) orBool I >Int umaxMInt(N)
You can:
- Compute the bitwise complement
~MIntof anMInt. - Compute the unary negation
--MIntof anMInt. - Compute the product
*MIntof twoMInts. - Compute the quotient
/sMIntof twoMInts interpreted as signed integers. - Compute the modulus
%sMIntof twoMInts interpreted as signed integers. - Compute the quotient
/uMIntof twoMInts interpreted as unsigned integers. - Compute the modulus
%uMIntof twoMInts interpreted as unsigned integers. - Compute the sum
+MIntof twoMInts. - Compute the difference
-MIntof twoMInts. - Compute the left shift
<<MIntof twoMInts. The secondMIntis always interpreted as positive. - Compute the arithmetic right shift
>>aMIntof twoMInts. The secondMIntis always interpreted as positve. - Compute the logical right shift
>>lMIntof twoMInts. The secondMIntis always interpreted as positive. - Compute the bitwise and
&MIntof twoMInts. - Compute the bitwise xor
xorMIntof twoMInts. - Compute the bitwise inclusive or
|MIntof twoMInts.
syntax {Width} MInt{Width} ::= "~MInt" MInt{Width} [function, total, hook(MINT.not), smt-hook(bvnot)]
| "--MInt" MInt{Width} [function, total, hook(MINT.neg), smt-hook(bvuminus)]
> left:
MInt{Width} "*MInt" MInt{Width} [function, total, hook(MINT.mul), smt-hook(bvmul)]
| MInt{Width} "/sMInt" MInt{Width} [function, hook(MINT.sdiv), smt-hook(bvsdiv)]
| MInt{Width} "%sMInt" MInt{Width} [function, hook(MINT.srem), smt-hook(bvsrem)]
| MInt{Width} "/uMInt" MInt{Width} [function, hook(MINT.udiv), smt-hook(bvudiv)]
| MInt{Width} "%uMInt" MInt{Width} [function, hook(MINT.urem), smt-hook(bvurem)]
> left:
MInt{Width} "+MInt" MInt{Width} [function, total, hook(MINT.add), smt-hook(bvadd)]
| MInt{Width} "-MInt" MInt{Width} [function, total, hook(MINT.sub), smt-hook(bvsub)]
> left:
MInt{Width} "<<MInt" MInt{Width} [function, hook(MINT.shl), smt-hook(bvshl)]
| MInt{Width} ">>aMInt" MInt{Width} [function, hook(MINT.ashr), smt-hook(bvashr)]
| MInt{Width} ">>lMInt" MInt{Width} [function, hook(MINT.lshr), smt-hook(bvlshr)]
> left:
MInt{Width} "&MInt" MInt{Width} [function, total, hook(MINT.and), smt-hook(bvand)]
> left:
MInt{Width} "xorMInt" MInt{Width} [function, total, hook(MINT.xor), smt-hook(bvxor)]
> left:
MInt{Width} "|MInt" MInt{Width} [function, total, hook(MINT.or), smt-hook(bvor)]
You can compute whether one MInt is less than, less than or equal to, greater
than, or greater than or equal to another MInt when interpreted as signed
or unsigned integers. You can also compute whether one MInt is equal to or
unequal to another MInt.
syntax {Width} Bool ::= MInt{Width} "<sMInt" MInt{Width} [function, total, hook(MINT.slt), smt-hook(bvslt)]
| MInt{Width} "<uMInt" MInt{Width} [function, total, hook(MINT.ult), smt-hook(bvult)]
| MInt{Width} "<=sMInt" MInt{Width} [function, total, hook(MINT.sle), smt-hook(bvsle)]
| MInt{Width} "<=uMInt" MInt{Width} [function, total, hook(MINT.ule), smt-hook(bvule)]
| MInt{Width} ">sMInt" MInt{Width} [function, total, hook(MINT.sgt), smt-hook(bvsgt)]
| MInt{Width} ">uMInt" MInt{Width} [function, total, hook(MINT.ugt), smt-hook(bvugt)]
| MInt{Width} ">=sMInt" MInt{Width} [function, total, hook(MINT.sge), smt-hook(bvsge)]
| MInt{Width} ">=uMInt" MInt{Width} [function, total, hook(MINT.uge), smt-hook(bvuge)]
| MInt{Width} "==MInt" MInt{Width} [function, total, hook(MINT.eq), smt-hook(=)]
| MInt{Width} "=/=MInt" MInt{Width} [function, total, hook(MINT.ne), smt-hook(distinct)]
You can compute the signed minimum sMinMInt, the signed maximum sMaxMInt,
the unsigned minimum uMinMInt, and the unsigned maximum uMaxMInt of two
MInts.
syntax {Width} MInt{Width} ::= sMaxMInt(MInt{Width}, MInt{Width}) [function, total, hook(MINT.smax), smt-hook((ite (bvslt #1 #2) #2 #1))]
| sMinMInt(MInt{Width}, MInt{Width}) [function, total, hook(MINT.smin), smt-hook((ite (bvslt #1 #2) #1 #2))]
| uMaxMInt(MInt{Width}, MInt{Width}) [function, total, hook(MINT.umax), smt-hook((ite (bvult #1 #2) #2 #1))]
| uMinMInt(MInt{Width}, MInt{Width}) [function, total, hook(MINT.umin), smt-hook((ite (bvult #1 #2) #1 #2))]
You can convert an MInt of one width to another width with roundMInt.
The resulting MInt will be truncated starting from the most significant bit
if the resulting width is smaller than the input. The resulting MInt will be
zero-extended with the same low-order bits if the resulting width is larger
than the input.
syntax {Width1, Width2} MInt{Width1} ::= roundMInt(MInt{Width2}) [function, total, hook(MINT.round)]
syntax {Width1, Width2} MInt{Width1} ::= signExtendMInt(MInt{Width2}) [function, total, hook(MINT.sext)]
endmodule