Basic Builtin Types in K

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.

k
requires "kast.md"

Default Modules

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.

k
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

Arrays

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.

k
module ARRAY-SYNTAX
  imports private LIST

  syntax Array

Array lookup

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.

k
  syntax KItem ::= Array "[" Int "]" [function]

Array update

You can create a new Array with a new value for a key in O(log(N)) time, or effectively constant.

k
  syntax Array ::= Array "[" key: Int "<-" value: KItem "]" [function, symbol(_[_<-_])]

Array reset

You can create a new Array where a particular key is reset to its default value in O(log(N)) time, or effectively constant.

k
  syntax Array ::= Array "[" Int "<-" "undef" "]" [function]

Multiple array update

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.

k
  syntax Array ::= updateArray(Array, index: Int, List) [function]

Array fill

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.

k
  syntax Array ::= fillArray(Array, index: Int, length: Int, value: KItem) [function]

Array range check

You can test whether an integer is within the bounds of an array in O(1) time.

k
  syntax Bool ::= Int "in_keys" "(" Array ")" [function, total]

k
endmodule

module ARRAY-IN-K [private]
  imports public ARRAY-SYNTAX
  imports private LIST
  imports private K-EQUAL
  imports private INT
  imports private BOOL

Array creation

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.

k
  syntax Array ::= makeArray(length: Int, value: KItem) [function, public]

Implementation of Arrays

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.

k
  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

Maps

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.

k
module MAP
  imports private BOOL-SYNTAX
  imports private INT-SYNTAX
  imports private LIST
  imports private SET

  syntax Map [hook(MAP.Map)]

Map concatenation

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.

k
  syntax Map ::= Map Map                        [left, function, hook(MAP.concat), symbol(_Map_), assoc, comm, unit(.Map), element(_|->_), index(0), format(%1%n%2)]

Map unit

The map with zero elements is represented by .Map.

k
  syntax Map ::= ".Map"                         [function, total, hook(MAP.unit), symbol(.Map)]

Map elements

An element of a Map is constructed via the |-> operator. The key is on the left and the value is on the right.

k
  syntax Map ::= KItem "|->" KItem                      [function, total, hook(MAP.element), symbol(_|->_), injective]

  syntax priority _|->_ > _Map_ .Map
  syntax non-assoc _|->_

Map lookup

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

k
  syntax KItem ::= Map "[" KItem "]"                    [function, hook(MAP.lookup), symbol(Map:lookup)]

Map lookup with default

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.

k
  syntax KItem ::= Map "[" KItem "]" "orDefault" KItem      [function, total, hook(MAP.lookupOrDefault), symbol(Map:lookupOrDefault)]

Map update

You can insert a key/value pair into a map in O(log(N)) time, or effectively constant.

k
  syntax Map ::= Map "[" key: KItem "<-" value: KItem "]"           [function, total, symbol(Map:update), hook(MAP.update), prefer]

Map delete

You can remove a key/value pair from a map via its key in O(log(N)) time, or effectively constant.

k
  syntax Map ::= Map "[" KItem "<-" "undef" "]"     [function, total, hook(MAP.remove), symbol(_[_<-undef])]

Map difference

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

k
  syntax Map ::= Map "-Map" Map                 [function, total, hook(MAP.difference)]

Multiple map update

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.

k
  syntax Map ::= updateMap(Map, Map)            [function, total, hook(MAP.updateAll)]

Multiple map removal

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.

k
  syntax Map ::= removeAll(Map, Set)            [function, total, hook(MAP.removeAll)]

Map keys (as Set)

You can get a Set of all the keys in a Map in O(N) time.

k
  syntax Set ::= keys(Map)                      [function, total, hook(MAP.keys)]

Map keys (as List)

You can get a List of all the keys in a Map in O(N) time.

k
  syntax List ::= "keys_list" "(" Map ")"       [function, hook(MAP.keys_list)]

Map key membership

You can check whether a key is present in a map in O(1) time.

k
  syntax Bool ::= KItem "in_keys" "(" Map ")"       [function, total, hook(MAP.in_keys)]

Map values (as List)

You can get a List of all the values in a map in O(N) time.

k
  syntax List ::= values(Map)                   [function, hook(MAP.values)]

Map size

You can get the number of key/value pairs in a map in O(1) time.

k
  syntax Int ::= size(Map)                      [function, total, hook(MAP.size), symbol(sizeMap)]

Map inclusion

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.

k
  syntax Bool ::= Map "<=Map" Map               [function, total, hook(MAP.inclusion)]

Map choice

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.

k
  syntax KItem ::= choice(Map)                      [function, hook(MAP.choice), symbol(Map:choice)]

Implementation of Maps

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.

k
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

Range Maps

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.

k
module RANGEMAP
  imports private BOOL-SYNTAX
  imports private INT-SYNTAX
  imports private LIST
  imports private SET

Range, bounded inclusively below and exclusively above.

k
  syntax Range ::= "[" KItem "," KItem ")"    [symbol(RangeMap:Range)]

  syntax RangeMap [hook(RANGEMAP.RangeMap)]

Range map concatenation

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

k
  syntax RangeMap ::= RangeMap RangeMap                        [left, function, hook(RANGEMAP.concat), symbol(_RangeMap_), assoc, comm, unit(.RangeMap), element(_r|->_), index(0), format(%1%n%2)]

Range map unit

The RangeMap with zero elements is represented by .RangeMap.

k
  syntax RangeMap ::= ".RangeMap"                         [function, total, hook(RANGEMAP.unit), symbol(.RangeMap)]

Range map elements

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.

k
  syntax RangeMap ::= Range "r|->" KItem                      [function, hook(RANGEMAP.elementRng), symbol(_r|->_), injective]

  syntax priority _r|->_ > _RangeMap_ .RangeMap
  syntax non-assoc _r|->_

Range map lookup

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.

k
  syntax KItem ::= RangeMap "[" KItem "]"                    [function, hook(RANGEMAP.lookup), symbol(RangeMap:lookup)]

Range map lookup with default

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

k
  syntax KItem ::= RangeMap "[" KItem "]" "orDefault" KItem      [function, total, hook(RANGEMAP.lookupOrDefault), symbol(RangeMap:lookupOrDefault)]

Range map lookup for range of key

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.

k
  syntax Range ::= "find_range" "(" RangeMap "," KItem ")"                    [function, hook(RANGEMAP.find_range), symbol(RangeMap:find_range)]

Range map update

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.

k
  syntax RangeMap ::= RangeMap "[" keyRange: Range "<-" value: KItem "]"           [function, symbol(RangeMap:update), hook(RANGEMAP.updateRng), prefer]

Range map delete

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.

k
  syntax RangeMap ::= RangeMap "[" Range "<-" "undef" "]"     [function, hook(RANGEMAP.removeRng), symbol(_r[_<-undef])]

Range map difference

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.

k
  syntax RangeMap ::= RangeMap "-RangeMap" RangeMap                 [function, total, hook(RANGEMAP.difference)]

Multiple range map update

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.

k
  syntax RangeMap ::= updateRangeMap(RangeMap, RangeMap)            [function, total, hook(RANGEMAP.updateAll)]

Multiple range map removal

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.

k
  syntax RangeMap ::= removeAll(RangeMap, Set)            [function, hook(RANGEMAP.removeAll)]

Range map keys (as Set)

You can get a Set of all the ranges in a RangeMap in O(N) time (where N is the size of the RangeMap).

k
  syntax Set ::= keys(RangeMap)                      [function, total, hook(RANGEMAP.keys)]

Range map keys (as List)

You can get a List of all the ranges in a RangeMap in O(N) time (where N is the size of the RangeMap).

k
  syntax List ::= "keys_list" "(" RangeMap ")"       [function, hook(RANGEMAP.keys_list)]

Range map key membership

You can check whether a key is present in a RangeMap in O(log(N)) time (where N is the size of the RangeMap).

k
  syntax Bool ::= KItem "in_keys" "(" RangeMap ")"       [function, total, hook(RANGEMAP.in_keys)]

Range map values (as List)

You can get a List of all values in a RangeMap in O(N) time (where N is the size of the RangeMap).

k
  syntax List ::= values(RangeMap)                   [function, hook(RANGEMAP.values)]

Range map size

You can get the number of range/value pairs in a RangeMap in O(1) time.

k
  syntax Int ::= size(RangeMap)                      [function, total, hook(RANGEMAP.size), symbol(sizeRangeMap)]

Range map inclusion

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.

k
  syntax Bool ::= RangeMap "<=RangeMap" RangeMap               [function, total, hook(RANGEMAP.inclusion)]

Range map choice

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.

k
  syntax KItem ::= choice(RangeMap)                      [function, hook(RANGEMAP.choice), symbol(RangeMap:choice)]
endmodule

Sets

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.

k
module SET
  imports private INT-SYNTAX
  imports private BASIC-K

  syntax Set [hook(SET.Set)]

Set concatenation

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.

k
  syntax Set ::= Set Set                  [left, function, hook(SET.concat), symbol(_Set_), assoc, comm, unit(.Set), idem, element(SetItem), format(%1%n%2)]

Set unit

The set with zero elements is represented by .Set.

k
  syntax Set ::= ".Set"                   [function, total, hook(SET.unit), symbol(.Set)]

Set elements

An element of a Set is constructed via the SetItem operator.

k
  syntax Set ::= SetItem(KItem)               [function, total, hook(SET.element), symbol(SetItem), injective]

Set union

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.

k
  syntax Set ::= Set "|Set" Set              [left, function, total, hook(SET.union), comm]
  rule S1:Set |Set S2:Set => S1 (S2 -Set S1) [concrete]

Set intersection

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.

k
  syntax Set ::= intersectSet(Set, Set)   [function, total, hook(SET.intersection), comm]

Set complement

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.

k
  syntax Set ::= Set "-Set" Set           [function, total, hook(SET.difference), symbol(Set:difference)]

Set membership

You can compute whether an element is a member of a set in O(1) time.

k
  syntax Bool ::= KItem "in" Set              [function, total, hook(SET.in), symbol(Set:in)]

Set inclusion

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

k
  syntax Bool ::= Set "<=Set" Set         [function, total, hook(SET.inclusion)]

Set size

You can get the number of elements (the cardinality) of a set in O(1) time.

k
  syntax Int ::= size(Set)                [function, total, hook(SET.size)]

Set choice

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.

k
  syntax KItem ::= choice(Set)                [function, hook(SET.choice), symbol(Set:choice)]

k
endmodule

Implementation of Sets

The following lemmas are simplifications that the Haskell backend can apply to simplify expressions of sort Set.

k
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

Lists

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.

k
module LIST
  imports private INT-SYNTAX
  imports private BASIC-K

  syntax List [hook(LIST.List)]

List concatenation

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.

k
  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)]

List unit

The list with zero elements is represented by .List.

k
  syntax List ::= ".List"                 [function, total, hook(LIST.unit), symbol(.List), smtlib(smt_seq_nil)]

List elements

An element of a List is constucted via the ListItem operator.

k
  syntax List ::= ListItem(KItem)             [function, total, hook(LIST.element), symbol(ListItem), smtlib(smt_seq_elem)]

List prepend

An element can be added to the front of a List using the pushList operator.

k
  syntax List ::= pushList(KItem, List)       [function, total, hook(LIST.push), symbol(pushList)]
  rule pushList(K::KItem, L1::List) => ListItem(K) L1

List indexing

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.

k
  syntax KItem ::= List "[" Int "]"           [function, hook(LIST.get), symbol(List:get)]

List update

You can create a new List with a new value at a particular index in O(log(N)) time, or effectively constant.

k
  syntax List ::= List "[" index: Int "<-" value: KItem "]" [function, hook(LIST.update), symbol(List:set)]

List of identical elements

You can create a list with length elements, each containing value, in O(N) time.

k
  syntax List ::= makeList(length: Int, value: KItem) [function, hook(LIST.make)]

Multiple list update

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.

k
  syntax List ::= updateList(dest: List, index: Int, src: List) [function, hook(LIST.updateAll)]

List fill

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.

k
  syntax List ::= fillList(List, index: Int, length: Int, value: KItem) [function, hook(LIST.fill)]

List slicing

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.

k
  syntax List ::= range(List, fromFront: Int, fromBack: Int)   [function, hook(LIST.range), symbol(List:range)]

List membership

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.

k
  syntax Bool ::= KItem "in" List             [function, total, hook(LIST.in), symbol(_inList_)]

List size

You can get the number of elements of a list in O(1) time.

k
  syntax Int ::= size(List)               [function, total, hook(LIST.size), symbol(sizeList), smtlib(smt_seq_len)]

k
endmodule

Collection Conversions

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.

k
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

Booleans

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.

k
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

Basic boolean arithmetic

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 Q is the same as notBool 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.

k
  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)]

Implementation of Booleans

The remainder of this section consists of an implementation in K of the operations listed above.

k
  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

Integers

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.

k
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

Integer arithmetic

You can:

• Compute the bitwise complement ~Int of an integer value in twos-complement.
• Compute the exponentiation ^Int of two integers.
• Compute the exponentiation of two integers modulo another integer (^%Int). A ^%Int B C is equal in value to (A ^Int B) %Int C, but has a better asymptotic complexity.
• Compute the product *Int of two integers.
• Compute the quotient /Int or modulus %Int of two integers using t-division, which rounds towards zero. Division by zero is #False.
• Compute the quotient divInt or modulus modInt of two integers using Euclidean division, in which the remainder is always non-negative. Division by zero is #False.
• Compute the sum +Int or difference -Int of two integers.
• Compute the arithmetic right shift >>Int of 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.

k
  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)]

Integer minimum and maximum

You can compute the minimum and maximum minInt and maxInt of two integers.

k
  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)]

Absolute value

You can compute the absolute value absInt of an integer.

k
  syntax Int ::= absInt ( Int )                 [function, total, smt-hook((ite (< #1 0) (- 0 #1) #1)), hook(INT.abs)]

Log base 2

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.

k
  syntax Int ::= log2Int ( Int )                [function, hook(INT.log2)]

Bit slicing

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.

k
  syntax Int ::= bitRangeInt           ( Int, index: Int, length: Int ) [function, hook(INT.bitRange)]
               | signExtendBitRangeInt ( Int, index: Int, length: Int ) [function, hook(INT.signExtendBitRange)]

Integer comparisons

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.

k
  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)]

Divides

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.

k
  syntax Bool ::= Int "dividesInt" Int    [function]

Random integers

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.

k
  syntax Int ::= randInt(Int) [function, hook(INT.rand), impure]
  syntax K ::= srandInt(Int) [function, hook(INT.srand), impure]

Implementation of Integers

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.

k
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

IEEE 754 Floating-point Numbers

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.

k
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

Float precision

You can retrieve the number of bits of precision in a Float.

k
  syntax Int ::= precisionFloat(Float) [function, total, hook(FLOAT.precision)]

Float exponent bits

You can retrieve the number of bits of exponent range in a Float.

k
  syntax Int ::= exponentBitsFloat(Float) [function, total, hook(FLOAT.exponentBits)]

Float exponent

You can retrieve the value of the exponent bits of a Float as an integer.

k
  syntax Int ::= exponentFloat(Float) [function, total, hook(FLOAT.exponent)]

Float sign

You can retrieve the value of the sign bit of a Float as a boolean. True means the sign bit is set.

k
  syntax Bool ::= signFloat(Float)      [function, total, hook(FLOAT.sign)]

Float special values

You can check whether a Float value is infinite or Not-a-Number.

k
  syntax Bool ::= isNaN(Float)          [function, total, smt-hook(fp.isNaN), hook(FLOAT.isNaN)]
                | isInfinite(Float)     [function, total]

Float arithmetic

You can:

• Compute the unary negation --Float of a float. --Float X is distinct from 0.0 -Float X. For example, 0.0 -Float 0.0 is positive zero. --Float 0.0 is negative zero.
• Compute the exponentation ^Float of two floats.
• Compute the product *Float, quotient /Float, or remainder %Float of two floats. The remainder is computed based on rounding the quotient of the two floats to the nearest integer.
• Compute the sum +Float or difference -Float of two floats.

k
  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)]

Floating-point mathematics

You can:

• Compute the Nth integer root rootFloat of a float.
• Compute the absolute value absFloat of a float.
• Round a floating-point number to a specified precision and exponent range (roundFloat). The resulting Float will yield the specified values when calling precisionFloat and exponentBitsFloat and 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 expFloat of a float (i.e. e^x).
• Compute the natural logarithm logFloat of a float.
• Compute the sine sinFloat of a float.
• Compute the cosine cosFloat of a float.
• Compute the tangent tanFlooat of a float.
• Compute the arcsine asinFloat of a float.
• Compute the arccosine acosFloat of a float.
• Compute the arctangent atanFloat of a float.
• Compute the arctangent atan2Float of two floats.
• Compute the maximum maxFloat of two floats.
• Compute the minimum minFloat of two floats.
• Compute the square root sqrtFloat of 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).

k
  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)]

Floating-point comparisons

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.

k
  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)

Conversion between integer and float

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.

k
  syntax Float ::= Int2Float(Int, precision: Int, exponentBits: Int)    [function, hook(FLOAT.int2float)]
  syntax Int ::= Float2Int(Float)    [function, total, hook(FLOAT.float2int)]

Implementation of Floats

The remainder of this section consists of an implementation in K of some of the operators above.

k
  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

Strings

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

k
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

String concatenation

You can concatenate two strings in O(N) time. For successive concatenation operations, it may be better to use the STRING-BUFFER module.

k
  syntax String ::= String "+String" String    [function, total, left, hook(STRING.concat)]

String length

You can get the length of a string in O(1) time.

k
  syntax Int ::= lengthString ( String ) [function, total, hook(STRING.length)]

Character and integer conversion

You can convert between a character (as represented by a string containing a single code point) and an integer in O(1) time.

k
  syntax String ::= chrChar ( Int )      [function, hook(STRING.chr)]
  syntax Int ::= ordChar ( String )      [function, hook(STRING.ord)]

String substring

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:

1. the range generated includes the character at startIndex but excludes the character at endIndex, i.e., the range is [startIndex..endIndex).
2. this function is only defined on valid indices (i.e., it is defined when startIndex < endIndex and endIndex is less than or equal to the string length).

k
  syntax String ::= substrString ( String , startIndex: Int , endIndex: Int ) [function, total, hook(STRING.substr)]

String search

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.

k
  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)]

String character search

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.

k
  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)]

String and Bool conversion

k
  syntax String ::= Bool2String(Bool) [function, total]
  rule Bool2String(true)  => "true"
  rule Bool2String(false) => "false"

k
  syntax Bool ::= String2Bool(String) [function]
  rule String2Bool("true")  => true
  rule String2Bool("false") => false

String and float conversion

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.

k
  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)]

String and integer conversions

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.

k
  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)]

String count and replace

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.

k
  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)]

String equality and lexicographic comparison

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.

k
  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)]

Implementation of Strings

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.

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

String Buffers

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:

• .StringBuffer creates a new StringBuffer with current content equal to the empty string.
• +String takes a StringBuffer and a String and appends the String to the end of the StringBuffer
• StringBuffer2String converts a StringBuffer to a String. This operation copies the string so that subsequent modifications to the StringBuffer will not change the value of the String returned by this function.

k
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

Byte Arrays

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.

k
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

k
module BYTES-STRING-ENCODE [symbolic]
  imports BYTES-SYNTAX

Encoding/decoding between Bytes and String

You can encode/decode between Bytes and String using UTF-8, UTF-16LE, UTF-16BE, UTF-32LE, and UTF-32BE

k
    syntax String ::= decodeBytes ( encoding: String , contents: Bytes ) [function, hook(BYTES.decodeBytes)]
    syntax Bytes ::= encodeBytes ( encoding: String , contents: String ) [function, hook(BYTES.encodeBytes)]
endmodule

k
module BYTES-HOOKED
  imports STRING-SYNTAX
  imports BYTES-SYNTAX
  imports BYTES-STRING-ENCODE

Empty byte array

The byte array of length zero is represented by .Bytes.

k
  syntax Bytes ::= ".Bytes" [function, total, hook(BYTES.empty)]

Endianness

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

k
  syntax Endianness ::= "LE" [symbol(littleEndianBytes)]
                      | "BE" [symbol(bigEndianBytes)]

Signedness

When converting to/from an integer, byte arrays can be treated as either signed or unsigned.

k
  syntax Signedness ::= "Signed" [symbol(signedBytes)]
                      | "Unsigned" [symbol(unsignedBytes)]

Integer and Bytes conversion

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.

k
  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)]

String and Bytes conversion

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.

k
  syntax String ::= Bytes2String(Bytes) [function, total, hook(BYTES.bytes2string)]
  syntax Bytes ::= String2Bytes(String) [function, total, hook(BYTES.string2bytes)]

Bytes update

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

k
  syntax Bytes ::= Bytes "[" index: Int "<-" value: Int "]" [function, hook(BYTES.update)]

Bytes lookup

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

k
  syntax Int ::= Bytes "[" Int "]" [function, hook(BYTES.get)]

Bytes substring

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.

k
  syntax Bytes ::= substrBytes(Bytes, startIndex: Int, endIndex: Int) [function, hook(BYTES.substr)]

Multiple bytes update

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.

k
  syntax Bytes ::= replaceAtBytes(dest: Bytes, index: Int, src: Bytes) [function, hook(BYTES.replaceAt)]

Multiple bytes update

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.

k
  syntax Bytes ::= memsetBytes(dest: Bytes, index: Int, count: Int, v: Int) [function, hook(BYTES.memset)]

Bytes padding

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.

k
  syntax Bytes ::= padRightBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padRight)]
                 | padLeftBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padLeft)]

Bytes reverse

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.

k
  syntax Bytes ::= reverseBytes(Bytes) [function, total, hook(BYTES.reverse)]

Bytes length

You can get the length of a Bytes term in O(1) time.

k
  syntax Int ::= lengthBytes(Bytes) [function, total, hook(BYTES.length), smtlib(lengthBytes)]

Bytes concatenation

You can create a new Bytes object by concatenating two Bytes objects together in O(N) time.

k
  syntax Bytes ::= Bytes "+Bytes" Bytes [function, total, hook(BYTES.concat), right]

endmodule

Implementation of Bytes

The remainder of this module consists of an implementation of some of the operators listed above in K.

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

Program identifiers

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 an Id to a String containing its name
• String2Id - Convert a String to an Id with the specified name
• !X:Id - You can get a fresh identifier distinct from any previous identifier generated by this syntax.

k
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

Equality and conditionals

Provided here are implementations of two important primitives in K:

• ==K - the equality between two terms. Returns true if they are equal and false if they are not equal.
• #if #then #else #fi - polymorphic conditional function. If the first argument evaluates to true, the second argument is returned. Otherwise, the third argument is returned. Note that this does not short-circuit on symbolic backends.

k
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

Meta operations

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.

k
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

I/O in K

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.

k
module K-IO
  imports private LIST
  imports private STRING
  imports private INT

I/O errors

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.

k
  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)]

I/O result sorts

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.

k
  syntax IOInt ::= Int | IOError
  syntax IOString ::= String | IOError

Opening a file

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.

k
  syntax IOInt ::= "#open" "(" path: String ")" [function]
               | "#open" "(" path: String "," mode: String ")" [function, hook(IO.open), impure]

  rule #open(S:String) => #open(S:String, "r+")

Get/set position in file

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

k
  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]

Read from file

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.

k
  syntax IOInt ::= "#getc" "(" fd: Int ")"             [function, hook(IO.getc), impure]
  syntax IOString ::= "#read" "(" fd: Int "," length: Int ")"    [function, hook(IO.read), impure]

Write to file

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.

k
  syntax K ::= "#putc" "(" fd: Int "," value: Int ")"      [function, hook(IO.putc), impure]
             | "#write" "(" fd: Int "," value: String ")" [function, hook(IO.write), impure]

Closing a file

You can close a file using #close. The returned value on success is .K.

k
  syntax K ::= "#close" "(" fd: Int ")" [function, hook(IO.close), impure]

Locking/unlocking a file

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.

k
  syntax K ::= "#lock" "(" fd: Int "," endIndex: Int ")" [function, hook(IO.lock), impure]
             | "#unlock" "(" fd: Int "," endIndex: Int ")" [function, hook(IO.unlock), impure]

Networking

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.

k
  syntax IOInt ::= "#accept" "(" fd: Int ")" [function, hook(IO.accept), impure]
  syntax K ::= "#shutdownWrite" "(" fd: Int ")" [function, hook(IO.shutdownWrite), impure]

Time

You can get the current time in seconds since midnight UTC on January 1, 1970 using #time.

k
  syntax Int ::= "#time" "(" ")" [function, hook(IO.time), impure]

Builtin file descriptors

Provided here are functions that return the file descriptor for standard input, standard output, and standard error.

k
  syntax Int ::= "#stdin"   [function, total]
                | "#stdout" [function, total]
                | "#stderr" [function, total]

  rule #stdin => 0
  rule #stdout => 1
  rule #stderr => 2

Shell access

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.

k
  syntax KItem ::= #system ( String ) [function, hook(IO.system), impure]
                 | "#systemResult" "(" Int /* exit code */ "," String /* stdout */ "," String /* stderr */ ")" [symbol(#systemResult)]

Temporary files

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.

k
  syntax IOFile ::= #mkstemp(template: String) [function, hook(IO.mkstemp), impure]
  syntax IOFile ::= IOError
                  | "#tempFile" "(" path: String "," fd: Int ")" [symbol(#tempFile)]

Deleting a file

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.

k
  syntax K ::= #remove(path: String) [function, total, hook(IO.remove), impure]

Logging

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.

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

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

k
  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)]

Implementation of high-level I/O streams in K

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.

k
  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

Machine Integers

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

k
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

Bitwidth of MInt

You can get the number of bits of width in an MInt using bitwidthMInt.

k
  syntax {Width} Int ::= bitwidthMInt(MInt{Width})   [function, total, hook(MINT.bitwidth)]

Int and MInt conversions

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.

k
  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)]

MInt min and max values

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.

k
  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

MInt bounds checking

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.

k
  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)

MInt arithmetic

You can:

• Compute the bitwise complement ~MInt of an MInt.
• Compute the unary negation --MInt of an MInt.
• Compute the product *MInt of two MInts.
• Compute the quotient /sMInt of two MInts interpreted as signed integers.
• Compute the modulus %sMInt of two MInts interpreted as signed integers.
• Compute the quotient /uMInt of two MInts interpreted as unsigned integers.
• Compute the modulus %uMInt of two MInts interpreted as unsigned integers.
• Compute the sum +MInt of two MInts.
• Compute the difference -MInt of two MInts.
• Compute the left shift <<MInt of two MInts. The second MInt is always interpreted as positive.
• Compute the arithmetic right shift >>aMInt of two MInts. The second MInt is always interpreted as positve.
• Compute the logical right shift >>lMInt of two MInts. The second MInt is always interpreted as positive.
• Compute the bitwise and &MInt of two MInts.
• Compute the bitwise xor xorMInt of two MInts.
• Compute the bitwise inclusive or |MInt of two MInts.

k
  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)]

MInt comparison

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.

k
  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)]

MInt min/max

You can compute the signed minimum sMinMInt, the signed maximum sMaxMInt, the unsigned minimum uMinMInt, and the unsigned maximum uMaxMInt of two MInts.

k
  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))]

MInt to MInt conversion

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.

k
  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)]

k
endmodule