Merge pull request #77 from ftsrg/bv-refactor

Remove signedness info from bitvector type

build.gradle.kts

@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.2.1"
+    version = "2.3.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

subprojects/cfa/README.md

@@ -38,19 +38,19 @@ Variables of the CFA can have the following types.
 * `int`: Mathematical, unbounded SMT integers.
 * `rat`: Rational numbers (implemented as SMT reals).
 * `[K] -> V`: SMT arrays (associative maps) from a given key type `K` to a value type `V`.
-* `bv[L]`, `bitvec[L]`, `ubv[L]`, `ubitvec[L]`, `sbv[L]`, `sbitvec[L]`: Signed or unsigned bitvector of given length `L`. _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._
+* `bv[L]`: Bitvector of given length `L`. _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._
 
 Expressions of the CFA include the following.
 * Identifiers (variables).
 * Literals, e.g., `true`, `false` (Bool), `0`, `123` (integer), `4 % 5` (rational).
   * Array literals can be given by listing the key-value pairs and the (mandatory) default element, e.g., `[0 <- 182, 1 <- 41, default <- 75]`. If there are no elements, the key type has to be given before the default element, e.g., `[<int>default <- 75]`.
-  * Bitvector literals can be given by stating the length, information about the signedness, and the exact value of the bitvector in binary, decimal or hexadecimal form. (E.g. `4'd5` is a 4-bit-long unsigned bitvector with the decimal value 5.) _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._
+  * Bitvector literals can be given by stating the length and the exact value of the bitvector in binary, decimal or hexadecimal form. (E.g. `4'd5` is a 4-bit-long bitvector with the decimal value 5.) _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._
 * Comparison, e.g., `=`, `/=`, `<`, `>`, `<=`, `>=`.
 * Boolean operators, e.g., `and`, `or`, `xor`, `not`, `imply`, `iff`.
 * Arithmetic, e.g., `+`, `-`, `/`, `*`, `mod`, `rem`.
 * Conditional: `if . then . else .`.
 * Array read (`a[i]`) and write (`a[i <- v]`).
-* Bitvector specific operators, e.g., `&`, `|`, `^`, `<<`, `>>`, `>>>`, `<<~`, `~>>`, `~`. _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._
+* Bitvector specific operators, e.g., `bvand`, `bvor`, `bvxor`, `bvshl`, `bvashr`, `bvlshr`, `bvrol`, `bvror`, `bvnot`, etc. _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._
 
 ### Textual representation (DSL)
 

subprojects/cfa/doc/bitvectors.md

@@ -4,118 +4,96 @@ As of now, Theta has basic bitvector support for the CFA formalism.
 
 ## Overview
 
-In Theta, every bitvector has a length, and is either signed or unsigned. It follows, that the range of every bitvector has a size of 2<sup>n</sup>. There are different operations that are available for bitvectors. It is important to note, that only operations between bitvectors with the same size and signedness are valid.
+In Theta, every bitvector has a positive length. It follows, that the range of every bitvector has a size of 2<sup>n</sup>. There are different operations that are available for bitvectors. It is important to note, that (usually) only operations between bitvectors with the same size are valid.
 
-Bitvectors have n bits. If the bitvector is unsigned then the values of the bits come from the binary representation of the underlying number. However, if the bitvector is signed then the values of the bits come from the two's complement representation of the underlying number.
+Bitvectors have n bits. Interpreting the signedness (signed/unsigned) of bitvectors depend on the operations (e.g., signed greater vs unsigned greater). If the bitvector is interpreted as an unsigned number then the values of the bits are interpreted as the binary representation of the underlying number. However, if the bitvector is interpreted as a signed number then the values of the bits are interpreted as the two's complement representation of the underlying number.
 
 ## Declaring bitvector variables
 
-To declare a bitvector variable, one has to specify the size and the signedness.
+To declare a bitvector variable, one has to specify the size.
 
 ```
-var x1 : bv[4] // Unsigned 4-bit-long bitvector
-var x2 : bitvec[5] // Unsigned 5-bit-long bitvector
-
-var u1 : ubv[4] // Unsigned 4-bit-long bitvector
-var u2 : ubitvec[6] // Unsigned 6-bit-long bitvector
-
-var s1 : sbv[4] // Signed 4-bit-long bitvector
-var s2 : sbitvec[7] // Signed 7-bit-long bitvector
-
+var x1 : bv[4] // 4-bit-long bitvector
+var x2 : bv[7] // 7-bit-long bitvector
 ```
 
 ## Bitvector literals
 
-There is a new literal, the bitvector literal that can be used to create bitvectors. Each literal defines the size and signedness of the literal. Moreover, eah literal can be entered using three different formats:
+There is a new literal, the bitvector literal that can be used to create bitvectors. Each literal defines the size of the literal. Moreover, each literal can be entered using three different formats:
 
 - The bitwise precise binary form
 - The bitwise precise hexadecimal form
 - And the non-bitwise-precise, although user-friendly decimal form
 
-The two bitwise precise forms specify the value for all bits directly. These are useful for unsigned bitvectors, where there is no two's complement behavior (e.g. bitfields).
+The two bitwise precise forms specify the value for all bits directly. These are useful for "unsigned" bitvectors, where there is no two's complement behavior (e.g. bitfields).
 
 ```
-4'b0010 // Unsiged 4-bit-long bitvector literal (binary form)
-8'xAF // Unsiged 4-bit-long bitvector literal (hexadecimal form)
-
-4'bu0010 // Unsiged 4-bit-long bitvector literal (binary form)
-8'xuAF // Unsiged 4-bit-long bitvector literal (hexadecimal form)
-
-4'bs0010 // Signed 4-bit-long bitvector literal (binary form, not recommended)
-8'xsAF // Signed 4-bit-long bitvector literal (hexadecimal form, not recommended)
+4'b0010 // 4-bit-long bitvector literal (binary form)
+8'xAF // 8-bit-long bitvector literal (hexadecimal form)
 ```
 
-The non-bitwise-precise decimal form can be used to create bitvectors that are based on numbers. Thsi form is recommended for signed bitvectors, or unsigned bitvectors that are not bitfields.
+The non-bitwise-precise decimal form can be used to create bitvectors that are based on numbers. This form is recommended for "signed" bitvectors, or "unsigned" bitvectors that are not bitfields.
 
 ```
-4'd10 // Unsigned 4-bit-long bitvector literal (decimal form)
-
-4'du10 // Unsigned 4-bit-long bitvector literal (decimal form)
-
-4'ds5 // Signed 4-bit-long bitvector literal (decimal form, positive value)
-4'ds-5 // Signed 4-bit-long bitvector literal (decimal form, negative value)
+4'd5 // 4-bit-long bitvector literal (decimal form, positive value)
+4'd-5 // 4-bit-long bitvector literal (decimal form, negative value)
 ```
 
 ## Operations on bitvectors
 
-The following operations are defined on bitvectors. As a general rule, every binary operation requires the bitvector on the left hand side and the bitvector on the right hand side to have the same size and signedness.
+The following operations are defined on bitvectors. As a general rule, every binary operation requires the bitvector on the left-hand side and the bitvector on the right-hand side to have the same size.
 
 The operators and their precedence are based on the [operators in C langauge](https://en.cppreference.com/w/c/language/operator_precedence).
 
 ### Basic arithmetic operations
 
-These operations perform basic arithmetic operations on bitvectors. These operations require that the bitvector on the left hand side and the bitvector on the right hand side have the same size and signedness. These operations overflow!
+These operations perform basic arithmetic operations on bitvectors. These operations require that the bitvector on the left-hand side and the bitvector on the right-hand side have the same size. These operations overflow!
 
-- **Addition:** Adds two bitvectors; `a + b`
-- **Subtraction:** Subtracts a from b; `a - b`
-- **Multiplication:** Multiplies two bitvectors; `a * b`
-- **Integer division:** Divides two bitvectors, and takes the integer part of the result; `a / b`
-- **Modulo:** Calculates (a mod b); `a mod b`
-- **Remainder:** Calculates the remainder of a / b; `a rem b`
-- **Negate:** Negates the value of a (only valid for signed bitvectors); `-a`
+- **Addition:** Adds two bitvectors; `a bvadd b`
+- **Subtraction:** Subtracts a from b; `a bvsub b`
+- **Multiplication:** Multiplies two bitvectors; `a bvmul b`
+- **Unsigned integer division:** Divides two bitvectors interpreted as unsigned numbers, and takes the integer part of the result; `a bvudiv b`
+- **Signed integer division:** Divides two bitvectors interpreted as signed numbers, and takes the integer part of the result; `a bvsdiv b`
+- **(Signed) Modulo:** Calculates (a mod b); `a bvsmod b`
+- **Unsigned remainder:** Calculates the remainder of a / b interpreted as unsigned numbers; `a bvurem b`
+- **Signed remainder:** Calculates the remainder of a / b interpreted as signed numbers; `a bvsrem b`
+- **Negate:** Negates the value of a (only valid for signed bitvectors); `bvneg a`
 
 ### Bitvector specific operations
 
-These operations are specific to bitvectors only. These operations require that the bitvector on the left hand side and the bitvector on the right hand side have the same size and signedness. For the exact semantics check out the respective operators in C. These operations overflow!
+These operations are specific to bitvectors only. These operations require that the bitvector on the left-hand side and the bitvector on the right-hand side have the same size. For the exact semantics check out the respective operators in C. These operations overflow!
+
+- **Bitwise and**: Ands two bitvectors; `a bvand b`
+- **Bitwise or**: Ors two bitvectors; `a bvor b`
+- **Bitwise xor**: XORs two bitvectors; `a bvxor b`
+- **Bitwise shift left**: Shifts *a* to the left with *b*; `a bvshl b`
+- **Bitwise arithmetic shift right**: Shifts *a* arithmetically to the right with *b*; `a bvashr b`
+- **Bitwise logical shift right**: Shifts *a* logically to the right with *b*; `a bvlshr b`
+- **Bitwise rotate left**: Rotates *a* to the left with *b*; `a bvrol b`
+- **Bitwise rotate right**: Rotates *a* to the right with *b*; `a bvror b`
+- **Bitwise not:** Negates all the bits in bitvectors; `bvnot a`
+
+The following four operators are special operators specific to bitvectors.
 
-- **Bitwise and**: Ands two bitvectors; `a & b`
-- **Bitwise or**: Ors two bitvectors; `a | b`
-- **Bitwise xor**: XORs two bitvectors; `a ^ b`
-- **Bitwise shift left**: Shifts *a* to the left with *b*; `a << b`
-- **Bitwise arithmetic shift right**: Shifts *a* arithmetically to the right with *b*; `a >> b`
-- **Bitwise logical shift right**: Shifts *a* logically to the right with *b*; `a >>> b`
-- **Bitwise rotate left**: Rotates *a* to the left with *b*; `a <<~ b`
-- **Bitwise rotate right**: Rotates *a* to the right with *b*; `a ~>> b`
-- **Bitwise not:** Negates all the bits in bitvectors; `~a`
+- **Concatenation**: Concatenates two bitvectors. The bitvectors do not have to be the same size; `a ++ b`
+- **Extraction**: Extracts a part of the bitvector. The indexes must be constant integer literals. Parameter from is interpreted as the starting index (with the least significant bit being 0), while parameter until is interpreted as the (exclusive) ending index (with the least significant bit being 0). The result is a bitvector of length _until-from_; `a[until:from]`
+- **Zero extend**: Extends the size of the bitvector to size N. The new bits will have the value 0; `a bv_zero_extend bv[N]`
+- **Sign extend**: Extends the size of the bitvector to size N. The new bits will have the value of the most significant bit of a; `a bv_sign_extend bv[N]`
 
 ### Relational operations
 
-These operations encode relational operations between bitvectors. These operations require that the bitvector on the left hand side and the bitvector on the right hand side have the same size and signedness.
+These operations encode relational operations between bitvectors. These operations require that the bitvector on the left-hand side and the bitvector on the right-hand side have the same size.
 
 - **Equality**: Checks if a equals to b; `a = b`
 - **Non-equality**: Checks if a does not equal to b; `a /= b`
-- **Greater than or equals to**: Checks if a is greater than or equals to b; `a >= b`
-- **Greater than**: Checks if a is greater than b; `a > b`
-- **Less than or equals to**: Checks if a is less than or equals to b; `a <= b`
-- **Less than**: Checks if a is less than b; `a < b`
-
-### Conversion "operations"
-
-Bitvectors can be converted to integers, and vice-versa. However, since integers can have an arbitrily huge value, should that value be impossible to be represented in the bitvectors range, an exception will be thrown. So procede with caution!
-
-There is no explicit conversion operator, however, the assignment statement converts between the two types.
-
-```
-var bv1 : bv[4]
-var i1 : int
-
-// ...
-
-L0 -> L1 {
-    bv1 := i1
-    i1 := bv1
-}
-```
+- **Unsigned greater than or equals to**: Checks if a is greater than or equals to b (a and b are interpreted as unsigned numbers); `a bvuge b`
+- **Unsigned greater than**: Checks if a is greater than b (a and b are interpreted as unsigned numbers); `a bvugt b`
+- **Unsigned less than or equals to**: Checks if a is less than or equals to b (a and b are interpreted as unsigned numbers); `a bvule b`
+- **Unsigned less than**: Checks if a is less than b (a and b are interpreted as unsigned numbers); `a bvult b`
+- **Signed greater than or equals to**: Checks if a is greater than or equals to b (a and b are interpreted as signed numbers); `a bvsge b`
+- **Signed greater than**: Checks if a is greater than b (a and b are interpreted as signed numbers); `a bvsgt b`
+- **Signed less than or equals to**: Checks if a is less than or equals to b (a and b are interpreted as signed numbers); `a bvsle b`
+- **Signed less than**: Checks if a is less than b (a and b are interpreted as signed numbers); `a bvslt b`
 
 ## Algorithmic support for verification with bitvectors