# 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`require "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`

, and `STRATEGY`

.

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 [hook(ARRAY.Array), unit(arrayCtor), element(_[_<-_])]`

### 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, hook(ARRAY.lookup)]`

### 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, hook(ARRAY.update), klabel(_[_<-_]), 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, hook(ARRAY.remove)]`

### 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, hook(ARRAY.updateAll)]`

### 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, hook(ARRAY.fill)]`

### 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, hook(ARRAY.in_keys)]`

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, hook(ARRAY.make), 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 [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(N*log(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(N*log(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), klabel(_Map_), symbol, 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), klabel(.Map), symbol, latex(\dotCt{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), klabel(_|->_), symbol, latex({#1}\mapsto{#2}), injective] syntax priorities _|->_ > _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), klabel(Map:lookup), symbol]`

### 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), klabel(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, klabel(Map:update), symbol, 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), klabel(_[_<-undef]), symbol]`

### 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), latex({#1}-_{\it Map}{#2})]`

### 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), klabel(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), klabel(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 [kore,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`

## 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(N*log(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(N*log(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), klabel(_Set_), symbol, 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), klabel(.Set), symbol, latex(\dotCt{Set})]`

### Set elements

An element of a `Set`

is constructed via the `SetItem`

operator.

k`syntax Set ::= SetItem(KItem) [function, total, hook(SET.element), klabel(SetItem), symbol, 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), latex({#1}-_{\it Set}{#2}), klabel(Set:difference), symbol]`

### 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), klabel(Set:in), symbol]`

### 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), klabel(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 [kore,symbolic] 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), klabel(_List_), symbol, smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem), format(%1%n%2)]`

### List unit

The list with zero elements is represented by `.List`

.

k`syntax List ::= ".List" [function, total, hook(LIST.unit), klabel(.List), symbol, smtlib(smt_seq_nil), latex(\dotCt{List})]`

### List elements

An element of a `List`

is constucted via the `ListItem`

operator.

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

### 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), klabel(List:get), symbol]`

### 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), klabel(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 `dest`

and `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), klabel(List:range), symbol]`

### 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), klabel(_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), klabel (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
ackends, both arguments will be evaluated.

k`syntax Bool ::= "notBool" Bool [function, total, klabel(notBool_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Bool}{#1}), hook(BOOL.not)] > Bool "andBool" Bool [function, total, klabel(_andBool_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Bool}{#2}), hook(BOOL.and)] | Bool "andThenBool" Bool [function, total, klabel(_andThenBool_), symbol, left, smt-hook(and), group(boolOperation), hook(BOOL.andThen)] | Bool "xorBool" Bool [function, total, klabel(_xorBool_), symbol, left, smt-hook(xor), group(boolOperation), hook(BOOL.xor)] | Bool "orBool" Bool [function, total, klabel(_orBool_), symbol, left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Bool}{#2}), hook(BOOL.or)] | Bool "orElseBool" Bool [function, total, klabel(_orElseBool_), symbol, left, smt-hook(or), group(boolOperation), hook(BOOL.orElse)] | Bool "impliesBool" Bool [function, total, klabel(_impliesBool_), symbol, left, smt-hook(=>), group(boolOperation), hook(BOOL.implies)] > left: Bool "==Bool" Bool [function, total, klabel(_==Bool_), symbol, left, comm, smt-hook(=), hook(BOOL.eq)] | Bool "=/=Bool" Bool [function, total, klabel(_=/=Bool_), symbol, 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 rule false andBool _:Bool => false rule _:Bool andBool false => false rule true andThenBool K::Bool => K rule K::Bool andThenBool true => K rule false andThenBool _ => false rule _ andThenBool false => false rule false xorBool B:Bool => B:Bool rule B:Bool xorBool false => B:Bool rule B:Bool xorBool B:Bool => false rule true orBool _:Bool => true rule _:Bool orBool true => true rule false orBool B:Bool => B rule B:Bool orBool false => B rule true orElseBool _ => true rule _ orElseBool true => true rule false orElseBool K::Bool => K rule K::Bool orElseBool false => K rule true impliesBool B:Bool => B rule false impliesBool _:Bool => true rule _:Bool impliesBool true => true rule B:Bool impliesBool false => notBool B rule B1:Bool =/=Bool B2:Bool => notBool (B1 ==Bool B2) endmodule module BOOL-KORE [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, klabel(~Int_), symbol, total, latex(\mathop{\sim_{\scriptstyle\it Int}}{#1}), hook(INT.not), smtlib(notInt)] > left: Int "^Int" Int [function, klabel(_^Int_), symbol, left, smt-hook(^), latex({#1}\mathrel{{\char`\^}_{\!\scriptstyle\it Int}}{#2}), hook(INT.pow)] | Int "^%Int" Int Int [function, klabel(_^%Int__), symbol, left, smt-hook((mod (^ #1 #2) #3)), hook(INT.powmod)] > left: Int "*Int" Int [function, total, klabel(_*Int_), symbol, left, comm, smt-hook(*), latex({#1}\mathrel{\ast_{\scriptstyle\it Int}}{#2}), hook(INT.mul)] /* FIXME: translate /Int and %Int into smtlib */ /* /Int and %Int implement t-division, which rounds towards 0 */ | Int "/Int" Int [function, klabel(_/Int_), symbol, left, smt-hook(div), latex({#1}\mathrel{\div_{\scriptstyle\it Int}}{#2}), hook(INT.tdiv)] | Int "%Int" Int [function, klabel(_%Int_), symbol, left, smt-hook(mod), latex({#1}\mathrel{\%_{\scriptstyle\it Int}}{#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, klabel(_divInt_), symbol, left, smt-hook(div), hook(INT.ediv)] | Int "modInt" Int [function, klabel(_modInt_), symbol, left, smt-hook(mod), hook(INT.emod)] > left: Int "+Int" Int [function, total, klabel(_+Int_), symbol, left, comm, smt-hook(+), latex({#1}\mathrel{+_{\scriptstyle\it Int}}{#2}), hook(INT.add)] | Int "-Int" Int [function, total, klabel(_-Int_), symbol, left, smt-hook(-), latex({#1}\mathrel{-_{\scriptstyle\it Int}}{#2}), hook(INT.sub)] > left: Int ">>Int" Int [function, klabel(_>>Int_), symbol, left, latex({#1}\mathrel{\gg_{\scriptstyle\it Int}}{#2}), hook(INT.shr), smtlib(shrInt)] | Int "<<Int" Int [function, klabel(_<<Int_), symbol, left, latex({#1}\mathrel{\ll_{\scriptstyle\it Int}}{#2}), hook(INT.shl), smtlib(shlInt)] > left: Int "&Int" Int [function, total, klabel(_&Int_), symbol, left, comm, latex({#1}\mathrel{\&_{\scriptstyle\it Int}}{#2}), hook(INT.and), smtlib(andInt)] > left: Int "xorInt" Int [function, total, klabel(_xorInt_), symbol, left, comm, latex({#1}\mathrel{\oplus_{\scriptstyle\it Int}}{#2}), hook(INT.xor), smtlib(xorInt)] > left: Int "|Int" Int [function, total, klabel(_|Int_), symbol, left, comm, latex({#1}\mathrel{|_{\scriptstyle\it Int}}{#2}), 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, klabel(_<=Int_), symbol, smt-hook(<=), latex({#1}\mathrel{\leq_{\scriptstyle\it Int}}{#2}), hook(INT.le)] | Int "<Int" Int [function, total, klabel(_<Int_), symbol, smt-hook(<), latex({#1}\mathrel{<_{\scriptstyle\it Int}}{#2}), hook(INT.lt)] | Int ">=Int" Int [function, total, klabel(_>=Int_), symbol, smt-hook(>=), latex({#1}\mathrel{\geq_{\scriptstyle\it Int}}{#2}), hook(INT.ge)] | Int ">Int" Int [function, total, klabel(_>Int_), symbol, smt-hook(>), latex({#1}\mathrel{>_{\scriptstyle\it Int}}{#2}), hook(INT.gt)] | Int "==Int" Int [function, total, klabel(_==Int_), symbol, comm, smt-hook(=), latex({#1}\mathrel{{=}{=}_{\scriptstyle\it Int}}{#2}), hook(INT.eq)] | Int "=/=Int" Int [function, total, klabel(_=/=Int_), symbol, comm, smt-hook(distinct), latex({#1}\mathrel{{=}{/}{=}_{\scriptstyle\it Int}}{#2}), 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] rule 0 <<Int _ => 0 [simplification] rule X >>Int 0 => X [simplification] rule 0 >>Int _ => 0 [simplification] endmodule module INT-SYMBOLIC-KORE [symbolic, kore, 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] // 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-KORE [kore, symbolic] imports private K-EQUAL imports private BOOL imports INT-COMMON rule I1:Int ==K I2:Int => I1 ==Int I2 [simplification] rule {K1 ==Int K2 #Equals true} => {K1 #Equals K2} [simplification] rule {true #Equals K1 ==Int K2} => {K1 #Equals K2} [simplification] rule {K1 ==Int K2 #Equals false} => #Not({K1 #Equals K2}) [simplification] rule {false #Equals K1 ==Int K2} => #Not({K1 #Equals K2}) [simplification] rule {K1 =/=Int K2 #Equals true} => #Not({K1 #Equals K2}) [simplification] rule {true #Equals K1 =/=Int K2} => #Not({K1 #Equals K2}) [simplification] rule {K1 =/=Int K2 #Equals false} => {K1 #Equals K2} [simplification] rule {false #Equals K1 =/=Int K2} => {K1 #Equals K2} [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, latex({#1}^{#2}), hook(FLOAT.pow)] > left: Float "*Float" Float [function, left, smt-hook((fp.mul roundNearestTiesToEven #1 #2)), latex({#1}\mathrel{\ast_{\scriptstyle\it Float}}{#2}), hook(FLOAT.mul)] | Float "/Float" Float [function, left, smt-hook((fp.div roundNearestTiesToEven #1 #2)), latex({#1}\mathrel{\div_{\scriptstyle\it Float}}{#2}), hook(FLOAT.div)] | Float "%Float" Float [function, left, smt-hook((fp.rem roundNearestTiesToEven #1 #2)), latex({#1}\mathrel{\%_{\scriptstyle\it Float}}{#2}), hook(FLOAT.rem)] > left: Float "+Float" Float [function, left, smt-hook((fp.add roundNearestTiesToEven #1 #2)), latex({#1}\mathrel{+_{\scriptstyle\it Float}}{#2}), hook(FLOAT.add)] | Float "-Float" Float [function, left, smt-hook((fp.sub roundNearestTiesToEven #1 #2)), latex({#1}\mathrel{-_{\scriptstyle\it Float}}{#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), latex({#1}\mathrel{\leq_{\scriptstyle\it Float}}{#2}), hook(FLOAT.le)] | Float "<Float" Float [function, smt-hook(fp.lt), latex({#1}\mathrel{<_{\scriptstyle\it Float}}{#2}), hook(FLOAT.lt)] | Float ">=Float" Float [function, smt-hook(fp.geq), latex({#1}\mathrel{\geq_{\scriptstyle\it Float}}{#2}), hook(FLOAT.ge)] | Float ">Float" Float [function, smt-hook(fg.gt), latex({#1}\mathrel{>_{\scriptstyle\it Float}}{#2}), hook(FLOAT.gt)] | Float "==Float" Float [function, comm, smt-hook(fp.eq), latex({#1}\mathrel{==_{\scriptstyle\it Float}}{#2}), hook(FLOAT.eq), klabel(_==Float_)] | Float "=/=Float" Float [function, comm, smt-hook((not (fp.eq #1 #2))), latex({#1}\mathrel{\neq_{\scriptstyle\it Float}}{#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, latex({\\it{}Int2Float}), hook(FLOAT.int2float)] syntax Int ::= Float2Int(Float) [function, total, latex({\\it{}Float2Int}), 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, latex({#1}+_{\scriptstyle\it String}{#2}), 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:

- the range generated includes the character at
`startIndex`

but excludes the character at`endIndex`

, i.e., the range is`[startIndex..endIndex)`

. - 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, klabel(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 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 rule replace(Source:String, _, _, 0) => Source rule replaceAll(Source:String, ToReplace:String, Replacement:String) => replace(Source, ToReplace, Replacement, countAllOccurrences(Source, ToReplace)) endmodule module STRING-KORE [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. In concrete backends, this representation is mutable and thus multiple
references can occur to the same `Bytes`

object and when one is modified, the
others are also modified. Care should be taken not to rely on this fact however
as this is not the case in symbolic backends and thus you will experience
divergent behavior 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[\\\"](([\\x20\\x21\\x23-\\x5B\\x5D-\\x7E])|([\\\\][tnfr\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2}))*[\\\"]" [token] endmodule`

k`module BYTES-STRING-ENCODE [kore, 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" [klabel(littleEndianBytes), symbol] | "BE" [klabel(bigEndianBytes), symbol]`

### Signedness

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

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

### 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, klabel(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. This does 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)]`

### 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`

. 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. This does not create a new
`Bytes`

object and will instead modify the original on concrete backends.

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 [kore] imports BYTES-HOOKED imports BYTES-SYMBOLIC-CEIL endmodule module BYTES-SYMBOLIC-CEIL [symbolic, kore] 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, E::Endianness, Unsigned) => Int2Bytes((log2Int(I) +Int 8) /Int 8, I, E) requires I >Int 0 rule Int2Bytes(0, _::Endianness, _) => .Bytes rule Int2Bytes(I::Int, E::Endianness, Signed) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E) requires I >Int 0 rule Int2Bytes(I::Int, E::Endianness, Signed) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E) requires I <Int -1 rule Int2Bytes(-1, E::Endianness, Signed) => Int2Bytes(1, -1, E) 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-z0-9\\_])[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), klabel(_==K_), symbol, latex({#1}\mathrel{=_K}{#2}), group(equalEqualK)] | K "=/=K" K [function, total, comm, smt-hook(distinct), hook(KEQUAL.ne), klabel(_=/=K_), symbol, latex({#1}\mathrel{\neq_K}{#2}), group(notEqualEqualK)] syntax priorities equalEqualK notEqualEqualK > boolOperation mlOp syntax {Sort} Sort ::= "#if" Bool "#then" Sort "#else" Sort "#fi" [function, total, smt-hook(ite), hook(KEQUAL.ite)] endmodule module K-EQUAL-KORE [kore, symbolic] import private BOOL import 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 import private BOOL import K-EQUAL-SYNTAX import 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`#parseKORE`

- Takes a String containing a K intermediate representation of a term such as is returned by`kast -o kore`

and converts it to a term. This is NOT type-safe. The responsibility is on the user to ensure that the string they provide is a valid representation of a term of the sort*exactly*equal to the sort where the function appears.`#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 ::= getKLabel(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)] // Takes as input a string and returns a K term syntax {Sort} Sort ::= #parseKORE(String) [function, hook(KREFLECTION.parseKORE)] syntax {Sort} String ::= #unparseKORE(Sort) [function, hook(KREFLECTION.printKORE)] syntax IOError ::= "#noParse" "(" String ")" [klabel(#noParse), symbol] 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" [klabel(#EOF), symbol] | #unknownIOError(errno: Int) [symbol] | "#E2BIG" [klabel(#E2BIG), symbol] | "#EACCES" [klabel(#EACCES), symbol] | "#EAGAIN" [klabel(#EAGAIN), symbol] | "#EBADF" [klabel(#EBADF), symbol] | "#EBUSY" [klabel(#EBUSY), symbol] | "#ECHILD" [klabel(#ECHILD), symbol] | "#EDEADLK" [klabel(#EDEADLK), symbol] | "#EDOM" [klabel(#EDOM), symbol] | "#EEXIST" [klabel(#EEXIST), symbol] | "#EFAULT" [klabel(#EFAULT), symbol] | "#EFBIG" [klabel(#EFBIG), symbol] | "#EINTR" [klabel(#EINTR), symbol] | "#EINVAL" [klabel(#EINVAL), symbol] | "#EIO" [klabel(#EIO), symbol] | "#EISDIR" [klabel(#EISDIR), symbol] | "#EMFILE" [klabel(#EMFILE), symbol] | "#EMLINK" [klabel(#EMLINK), symbol] | "#ENAMETOOLONG" [klabel(#ENAMETOOLONG), symbol] | "#ENFILE" [klabel(#ENFILE), symbol] | "#ENODEV" [klabel(#ENODEV), symbol] | "#ENOENT" [klabel(#ENOENT), symbol] | "#ENOEXEC" [klabel(#ENOEXEC), symbol] | "#ENOLCK" [klabel(#ENOLCK), symbol] | "#ENOMEM" [klabel(#ENOMEM), symbol] | "#ENOSPC" [klabel(#ENOSPC), symbol] | "#ENOSYS" [klabel(#ENOSYS), symbol] | "#ENOTDIR" [klabel(#ENOTDIR), symbol] | "#ENOTEMPTY" [klabel(#ENOTEMPTY), symbol] | "#ENOTTY" [klabel(#ENOTTY), symbol] | "#ENXIO" [klabel(#ENXIO), symbol] | "#EPERM" [klabel(#EPERM), symbol] | "#EPIPE" [klabel(#EPIPE), symbol] | "#ERANGE" [klabel(#ERANGE), symbol] | "#EROFS" [klabel(#EROFS), symbol] | "#ESPIPE" [klabel(#ESPIPE), symbol] | "#ESRCH" [klabel(#ESRCH), symbol] | "#EXDEV" [klabel(#EXDEV), symbol] | "#EWOULDBLOCK" [klabel(#EWOULDBLOCK), symbol] | "#EINPROGRESS" [klabel(#EINPROGRESS), symbol] | "#EALREADY" [klabel(#EALREADY), symbol] | "#ENOTSOCK" [klabel(#ENOTSOCK), symbol] | "#EDESTADDRREQ" [klabel(#EDESTADDRREQ), symbol] | "#EMSGSIZE" [klabel(#EMSGSIZE), symbol] | "#EPROTOTYPE" [klabel(#EPROTOTYPE), symbol] | "#ENOPROTOOPT" [klabel(#ENOPROTOOPT), symbol] | "#EPROTONOSUPPORT" [klabel(#EPROTONOSUPPORT), symbol] | "#ESOCKTNOSUPPORT" [klabel(#ESOCKTNOSUPPORT), symbol] | "#EOPNOTSUPP" [klabel(#EOPNOTSUPP), symbol] | "#EPFNOSUPPORT" [klabel(#EPFNOSUPPORT), symbol] | "#EAFNOSUPPORT" [klabel(#EAFNOSUPPORT), symbol] | "#EADDRINUSE" [klabel(#EADDRINUSE), symbol] | "#EADDRNOTAVAIL" [klabel(#EADDRNOTAVAIL), symbol] | "#ENETDOWN" [klabel(#ENETDOWN), symbol] | "#ENETUNREACH" [klabel(#ENETUNREACH), symbol] | "#ENETRESET" [klabel(#ENETRESET), symbol] | "#ECONNABORTED" [klabel(#ECONNABORTED), symbol] | "#ECONNRESET" [klabel(#ECONNRESET), symbol] | "#ENOBUFS" [klabel(#ENOBUFS), symbol] | "#EISCONN" [klabel(#EISCONN), symbol] | "#ENOTCONN" [klabel(#ENOTCONN), symbol] | "#ESHUTDOWN" [klabel(#ESHUTDOWN), symbol] | "#ETOOMANYREFS" [klabel(#ETOOMANYREFS), symbol] | "#ETIMEDOUT" [klabel(#ETIMEDOUT), symbol] | "#ECONNREFUSED" [klabel(#ECONNREFUSED), symbol] | "#EHOSTDOWN" [klabel(#EHOSTDOWN), symbol] | "#EHOSTUNREACH" [klabel(#EHOSTUNREACH), symbol] | "#ELOOP" [klabel(#ELOOP), symbol] | "#EOVERFLOW" [klabel(#EOVERFLOW), symbol]`

### 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 */ ")" [klabel(#systemResult), symbol]`

### 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 ")" [klabel(#tempFile), symbol]`

### 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]`

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

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] | #traceK(value: K) [function, total, hook(IO.traceTerm), impure, returnsUnit, symbol]`

### 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> [unblock] /* 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`MInt`

s. - Compute the quotient
`/sMInt`

of two`MInt`

s interpreted as signed integers. - Compute the modulus
`%sMInt`

of two`MInt`

s interpreted as signed integers. - Compute the quotient
`/uMInt`

of two`MInt`

s interpreted as unsigned integers. - Compute the modulus
`%uMInt`

of two`MInt`

s interpreted as unsigned integers. - Compute the sum
`+MInt`

of two`MInt`

s. - Compute the difference
`-MInt`

of two`MInt`

s. - Compute the left shift
`<<MInt`

of two`MInt`

s. The second`MInt`

is always interpreted as positive. - Compute the arithmetic right shift
`>>aMInt`

of two`MInt`

s. The second`MInt`

is always interpreted as positve. - Compute the logical right shift
`>>lMInt`

of two`MInt`

s. The second`MInt`

is always interpreted as positive. - Compute the bitwise and
`&MInt`

of two`MInt`

s. - Compute the bitwise xor
`xorMInt`

of two`MInt`

s. - Compute the bitwise inclusive or
`|MInt`

of two`MInt`

s.

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
`MInt`

s.

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

k`endmodule`

## Strategies

K supports a built-in strategy language that allows you to control how rules
apply. In order to enable it, simply import the `STRATEGY`

module in your
definition. This includes the following basic strategy constructs:

`^ Category:#RuleTag`

- This is a strategy that indicates that you should apply a rule with the specified category exactly once. By default, all rules get the`regular`

tag. This can be changed on individual rules with the`tag`

attribute.`~ Category:#RuleTag`

- This is the state the strategy cell will be in after a rule has applied. In other words, all rules that do not mention the strategy cell are automatically instrumented so that they rewrite the current top of the`<s>`

cell from`^`

to`~`

`<s>`

- This is the strategy cell and contains the current strategy.`#STUCK()`

- By default, a rule is automatically inserted into the definition which adds`#STUCK()`

to the top of the`<s>`

cell if no other rules apply and if it is not already at the top of the`<s>`

cell.

k`module STRATEGY imports ML-SYNTAX imports KVARIABLE-SYNTAX imports private K-EQUAL syntax #RuleTag ::= #KVariable syntax Strategy ::= #STUCK() [symbol] | "^" #RuleTag [symbol, klabel(#applyRule)] | "~" #RuleTag [symbol, klabel(#appliedRule)] configuration <s> $STRATEGY:K </s> endmodule module RULE-TAG-SYNTAX imports BUILTIN-ID-TOKENS syntax #RuleTag ::= #LowerId [token] endmodule`

This is not a complete strategy language. However, it provides several basics.
The user can extend this strategy language into a complete strategy language
in one of three ways. First, they can import the `DEFAULT-STRATEGY`

module,
which provides a very basic strategy that is essentially equivalent to
execution without a strategy. This can be useful if you wish to wholly
manipulate the strategy cell yourself within other rules.

k`module DEFAULT-STRATEGY-CONCRETE [concrete] imports STRATEGY imports RULE-TAG-SYNTAX rule ~ regular => ^ regular [anywhere] endmodule module DEFAULT-STRATEGY-SYMBOLIC [symbolic] imports STRATEGY imports RULE-TAG-SYNTAX rule <s> ~ regular => ^ regular ... </s> endmodule module DEFAULT-STRATEGY imports STRATEGY imports DEFAULT-STRATEGY-CONCRETE imports DEFAULT-STRATEGY-SYMBOLIC rule initSCell(_) => <s> ^ regular </s> [priority(25)] endmodule`

The second way you can extend the strategy language is with the
`STRATEGY-ABSTRACT`

module. This provides a slightly more advanced set of
strategies which you can use to compose the basic strategies in the `STRATEGY`

module into more complex strategies. Note however that the functionality
provided is still relatively basic.

k`module STRATEGY-ABSTRACT imports STRATEGY syntax #RuleTag ::= "(" #RuleTag ")" [bracket] // ---------------------------------------------- syntax Strategy ::= ".Strategy" | "(" Strategy ")" [bracket] // ---------------------------------------------- rule <s> .Strategy => . ... </s> syntax KItem ::= #catchSTUCK ( Strategy ) // ----------------------------------------- rule <s> #catchSTUCK(_) => . ... </s> rule <s> #STUCK() ~> (_S:Strategy => .) ... </s> rule <s> #STUCK() ~> #catchSTUCK(S) => S ... </s> syntax Strategy ::= Strategy ";" Strategy [left] // ------------------------------------------------ rule <s> S:Strategy ; S':Strategy => S ~> S' ... </s> syntax #RuleTag ::= #RuleTag "|" #RuleTag [left, klabel(#alternateRule)] // ------------------------------------------------------------------------ rule <s> ^ RT:#RuleTag | RT':#RuleTag => ^ RT ~> #catchSTUCK(^ RT') ... </s> syntax #RuleTag ::= #RuleTag "*" [klabel(#repeatRule)] // ------------------------------------------------------ rule <s> ^ RT:#RuleTag * => ^ RT ~> ^ RT * ~> #catchSTUCK(.Strategy) ... </s> endmodule`

The third mechanism for extending the strategy language is to define your own strategy language. No special facility is required in K in order to compose strategies together, so you are free to write whatever rules that manipulate the strategy cell you want, and thus whatever more complex strategies you can compose from the base builtin strategies.