diff --git a/.gitignore b/.gitignore index c2b3656d..c219f17d 100644 --- a/.gitignore +++ b/.gitignore @@ -20,3 +20,4 @@ preprocessor/build tri-pp *.swp *.swo +.attach_pid* diff --git a/acsl-parser/acsl-parser.jar b/acsl-parser/acsl-parser.jar index f2c8bd7b..eddde5b3 100644 Binary files a/acsl-parser/acsl-parser.jar and b/acsl-parser/acsl-parser.jar differ diff --git a/cc-parser/cc-parser.jar b/cc-parser/cc-parser.jar index fdd6d84c..87995dca 100644 Binary files a/cc-parser/cc-parser.jar and b/cc-parser/cc-parser.jar differ diff --git a/cc-parser/concurrentC.cf b/cc-parser/concurrentC.cf index cf4d9181..0c6cf277 100644 --- a/cc-parser/concurrentC.cf +++ b/cc-parser/concurrentC.cf @@ -304,8 +304,8 @@ token OctalLong '0'["01234567"]* ('l'|'L'); token OctalUnsLong '0'["01234567"]* (('u''l')|('U''L')); -token CDouble (((digit+ '.')|('.' digit+))(('e'|'E') ('-')? digit+)?)| - (digit+ ('e'|'E') ('-')? digit+)|(digit+ '.' digit+ 'E' ('-')? digit+); +token CDouble (((digit+ '.' digit+)|(digit+ '.')|('.' digit+))(('e'|'E')('-')? digit+)? + )|((digit+ ('e'|'E')('-')? digit+)); token CFloat (((digit+ '.' digit+)|(digit+ '.')|('.' digit+))(('e'|'E')('-')? digit+)? ('f'|'F'))|((digit+ ('e'|'E')('-')? digit+)('f'|'F')); @@ -354,7 +354,7 @@ Econst. Exp17 ::= Constant; Estring. Exp17 ::= String; Enondet. Exp17 ::= "_"; -Efloat. Constant ::= Double; +Einf. Constant ::= "INFINITY"; Echar. Constant ::= Char; Eunsigned. Constant ::= Unsigned; Elong. Constant ::= Long; @@ -367,13 +367,10 @@ Eoctal. Constant ::= Octal; Eoctalunsign. Constant ::= OctalUnsigned; Eoctallong. Constant ::= OctalLong; Eoctalunslong. Constant ::= OctalUnsLong; -Ecdouble. Constant ::= CDouble; Ecfloat. Constant ::= CFloat; +Ecdouble. Constant ::= CDouble; Eclongdouble. Constant ::= CLongDouble; -Eint. Constant ::= UnboundedInteger; - --- internal Elonger. Constant ::= Integer; --- internal Edouble. Constant ::= Double; +Eint. Constant ::= UnboundedInteger; Especial. Constant_expression ::= Exp3; diff --git a/regression-tests/double/Answers b/regression-tests/double/Answers new file mode 100644 index 00000000..fd94215d --- /dev/null +++ b/regression-tests/double/Answers @@ -0,0 +1,42 @@ + +add_1.c +SAFE + +add_2.c +UNSAFE + +add_3.c +UNSAFE + +div_1.c +SAFE + +div_2.c +UNSAFE + +div_3.c +SAFE + +init_1.c +SAFE + +init_2.c +SAFE + +mul_1.c +SAFE + +mul_2.c +UNSAFE + +loop_1.c +SAFE + +loop_2.c +UNSAFE + +sub_1.c +SAFE + +sub_2.c +UNSAFE diff --git a/regression-tests/double/add_1.c b/regression-tests/double/add_1.c new file mode 100644 index 00000000..f2578fa9 --- /dev/null +++ b/regression-tests/double/add_1.c @@ -0,0 +1,7 @@ +// SAFE +int main () { + double a = 0.22; + double b = 0.1; + assert(a+b== 0.32); + return 0; +} diff --git a/regression-tests/double/add_2.c b/regression-tests/double/add_2.c new file mode 100644 index 00000000..0cd9add3 --- /dev/null +++ b/regression-tests/double/add_2.c @@ -0,0 +1,7 @@ +//UNSAFE +int main() { + double a = 3.0; + double b = 0.5; + assert(a+b == 3.501); + return 0; +} diff --git a/regression-tests/double/add_3.c b/regression-tests/double/add_3.c new file mode 100644 index 00000000..0013619e --- /dev/null +++ b/regression-tests/double/add_3.c @@ -0,0 +1,6 @@ +//UNSAFE +int main() { + double a = 2.0; + double b = a + 0.5; + assert(a + 0.4 == b); +} diff --git a/regression-tests/double/div_1.c b/regression-tests/double/div_1.c new file mode 100644 index 00000000..286e97a3 --- /dev/null +++ b/regression-tests/double/div_1.c @@ -0,0 +1,7 @@ +//SAFE +int main () { + double a = 4.0; + double b = 0.5; + assert(a/b== 8.0); + return 0; +} diff --git a/regression-tests/double/div_2.c b/regression-tests/double/div_2.c new file mode 100644 index 00000000..e973b1c4 --- /dev/null +++ b/regression-tests/double/div_2.c @@ -0,0 +1,7 @@ +//UNSAFE +int main () { + double a = 4.0; + double b = 0.5; + assert(a/b== 8.01); + return 0; +} diff --git a/regression-tests/double/div_3.c b/regression-tests/double/div_3.c new file mode 100644 index 00000000..6e379e2b --- /dev/null +++ b/regression-tests/double/div_3.c @@ -0,0 +1,7 @@ +int main () { + double a = 4.0; + double b = 0.1; + assert(a/b <= 40.00001); + assert(a/b >= 39.99999); + return 0; +} diff --git a/regression-tests/double/init_1.c b/regression-tests/double/init_1.c new file mode 100644 index 00000000..e13dfbf3 --- /dev/null +++ b/regression-tests/double/init_1.c @@ -0,0 +1,7 @@ +//SAFE +int main() { + double a = 0.0; + assert(a == 0.0); + return 0; + +} diff --git a/regression-tests/double/init_2.c b/regression-tests/double/init_2.c new file mode 100644 index 00000000..0c2c56d3 --- /dev/null +++ b/regression-tests/double/init_2.c @@ -0,0 +1,6 @@ +//SAFE +int main() { + double a = 4.24242; + assert(a == 4.24242); + return 0; +} diff --git a/regression-tests/double/init_3.c b/regression-tests/double/init_3.c new file mode 100644 index 00000000..2f92a113 --- /dev/null +++ b/regression-tests/double/init_3.c @@ -0,0 +1,7 @@ +//UNSAFE +int main() { + double a = 4.24242; + assert(a == 4.24241); + return 0; + +} diff --git a/regression-tests/double/int_plus_float.c b/regression-tests/double/int_plus_float.c new file mode 100644 index 00000000..a187b1ee --- /dev/null +++ b/regression-tests/double/int_plus_float.c @@ -0,0 +1,7 @@ +//SAFE +int main () { + double a = 2.0; + int b = 1; + assert(a+b == 3.0); + return 0; +} diff --git a/regression-tests/double/leq_1.c b/regression-tests/double/leq_1.c new file mode 100644 index 00000000..ebc00916 --- /dev/null +++ b/regression-tests/double/leq_1.c @@ -0,0 +1,6 @@ +//SAFE +int main() { + double a = 2.3; + double b = 2.25;; + assert(b <= a); +} diff --git a/regression-tests/double/loop_1.c b/regression-tests/double/loop_1.c new file mode 100644 index 00000000..58480f19 --- /dev/null +++ b/regression-tests/double/loop_1.c @@ -0,0 +1,12 @@ +//SAFE +void main(void) { + int i = 0; + double x = 0.5; + double y = x; + while (x < 3000.0) { + x = x*2.0; + y = x; + ++i; + } + assert(x==y); +} diff --git a/regression-tests/double/loop_2.c b/regression-tests/double/loop_2.c new file mode 100644 index 00000000..b00f7506 --- /dev/null +++ b/regression-tests/double/loop_2.c @@ -0,0 +1,15 @@ +//UNSAFE +int N = _; + +void main(void) { + int i = 0; + double x = 0.5; + double y = x; + while (i < N) { + if(x == y) { + x = x+2.25; + } + ++i; + } + assert(x==y); +} diff --git a/regression-tests/double/mul_1.c b/regression-tests/double/mul_1.c new file mode 100644 index 00000000..172cc3b8 --- /dev/null +++ b/regression-tests/double/mul_1.c @@ -0,0 +1,7 @@ +//SAFE +int main () { + double a = 0.5; + double b = 0.5; + assert(a*b== 0.25); + return 0; +} diff --git a/regression-tests/double/mul_2.c b/regression-tests/double/mul_2.c new file mode 100644 index 00000000..ce17e7e1 --- /dev/null +++ b/regression-tests/double/mul_2.c @@ -0,0 +1,6 @@ +int main () { + double a = 0.5; + double b = 0.5; + assert(a*b== 0.251); + return 0; +} diff --git a/regression-tests/double/nan.c b/regression-tests/double/nan.c new file mode 100644 index 00000000..2f08ec85 --- /dev/null +++ b/regression-tests/double/nan.c @@ -0,0 +1,8 @@ +//UNSAFE IF NAN IS INCLUDED OTHERWISE SAFE +int main() +{ + double x = _; + + assert(x==x); + return 0; +} diff --git a/regression-tests/double/nan_create.c b/regression-tests/double/nan_create.c new file mode 100644 index 00000000..a7bb5969 --- /dev/null +++ b/regression-tests/double/nan_create.c @@ -0,0 +1,5 @@ +//UNSAFE +int main() { + double nan = 0/0; + assert(nan == 2); +} diff --git a/regression-tests/double/nan_range.c b/regression-tests/double/nan_range.c new file mode 100644 index 00000000..fac54bed --- /dev/null +++ b/regression-tests/double/nan_range.c @@ -0,0 +1,10 @@ +// SAFE +int main() { + double x = _; + + if (x >= -0.00001 && x <= -0.00001) { + assert(x==x); + } + return 0; +} + diff --git a/regression-tests/double/nondet_1.c b/regression-tests/double/nondet_1.c new file mode 100644 index 00000000..ace4be01 --- /dev/null +++ b/regression-tests/double/nondet_1.c @@ -0,0 +1,7 @@ +// SAFE +int main() { + double x = _; + double y = x + 1.0; + assert(y>x); + +} diff --git a/regression-tests/double/nondet_2.c b/regression-tests/double/nondet_2.c new file mode 100644 index 00000000..f3a5e2f3 --- /dev/null +++ b/regression-tests/double/nondet_2.c @@ -0,0 +1,6 @@ +// UNSAFE +int main() { + double x = _; + double y = x + 1.0; + assert(y&1 | grep -v 'at ' +done + diff --git a/regression-tests/double/sub_1.c b/regression-tests/double/sub_1.c new file mode 100644 index 00000000..e2fc46fe --- /dev/null +++ b/regression-tests/double/sub_1.c @@ -0,0 +1,8 @@ +//SAFE +int main() { + double a = 1.5; + double b = 0.5; + assert(a-b== 1.0); + return 0; + +} diff --git a/regression-tests/double/sub_2.c b/regression-tests/double/sub_2.c new file mode 100644 index 00000000..3510abcf --- /dev/null +++ b/regression-tests/double/sub_2.c @@ -0,0 +1,7 @@ +// UNSAFE +int main() { + double a = 0.22; + double b = 0.1; + assert(a-b == 0.1); + return 0; +} diff --git a/regression-tests/float/Answers b/regression-tests/float/Answers new file mode 100644 index 00000000..1aafa6b6 --- /dev/null +++ b/regression-tests/float/Answers @@ -0,0 +1,39 @@ + +add_1.c +SAFE + +add_2.c +SAFE + +add_3.c +UNSAFE + +div_1.c +SAFE + +div_2.c +SAFE + +init_1.c +SAFE + +init_2.c +SAFE + +loop_1.c +SAFE + +loop_2.c +UNSAFE + +mul_1.c +SAFE + +mul_2.c +UNSAFE + +sub_1.c +SAFE + +sub_2.c +UNSAFE diff --git a/regression-tests/float/add_1.c b/regression-tests/float/add_1.c new file mode 100644 index 00000000..8f01dd53 --- /dev/null +++ b/regression-tests/float/add_1.c @@ -0,0 +1,6 @@ +int main () { + float a = 0.5f; + float b = 0.75f; + assert(a+b== 1.25f); + return 0; +} diff --git a/regression-tests/float/add_2.c b/regression-tests/float/add_2.c new file mode 100644 index 00000000..5fd93d92 --- /dev/null +++ b/regression-tests/float/add_2.c @@ -0,0 +1,6 @@ +int main() { + float a = 3.0f; + float b = 0.5f; + assert(a+b == 3.5f); + return 0; +} diff --git a/regression-tests/float/add_3.c b/regression-tests/float/add_3.c new file mode 100644 index 00000000..7df0b362 --- /dev/null +++ b/regression-tests/float/add_3.c @@ -0,0 +1,5 @@ +int main() { + float a = 2.0f; + float b = a + 0.5f; + assert(a + 0.4f == b); +} diff --git a/regression-tests/float/div_1.c b/regression-tests/float/div_1.c new file mode 100644 index 00000000..95ff0cc3 --- /dev/null +++ b/regression-tests/float/div_1.c @@ -0,0 +1,7 @@ +int main () { + float a = 4.0f; + float b = 0.1f; + assert(a/b <= 40.00001f); + assert(a/b >= 39.99999f); + return 0; +} diff --git a/regression-tests/float/div_2.c b/regression-tests/float/div_2.c new file mode 100644 index 00000000..ad292ce2 --- /dev/null +++ b/regression-tests/float/div_2.c @@ -0,0 +1,6 @@ +int main () { + float a = 4.0f; + float b = 0.5f; + assert(a/b== 8.0f); + return 0; +} diff --git a/regression-tests/float/example.c b/regression-tests/float/example.c new file mode 100644 index 00000000..062f5bf5 --- /dev/null +++ b/regression-tests/float/example.c @@ -0,0 +1,10 @@ +int main() { + int x = 0; + int y = 3; + while(x <= 2) { + x++; + y = x; + } + assert(x==y); +} + diff --git a/regression-tests/float/industrial_tricera_simple.c b/regression-tests/float/industrial_tricera_simple.c new file mode 100644 index 00000000..5c68d3aa --- /dev/null +++ b/regression-tests/float/industrial_tricera_simple.c @@ -0,0 +1,88 @@ +//Global variables 'acting' as return variables +float return_modMin; +float return_modMax; + +int return_modStatus; + +float mod0_status; + +float mod0_min; + +float mod0_max; + +float batt_min_output; +float batt_max_output; +int batt_status_output; + +void modStatus() { + return_modStatus = mod0_status; +} + +void modMin() { + return_modMin = mod0_min; +} + +void modMax() { + return_modMax = mod0_max; +} + +void moduleDiag(int idx) { + modMin(); + modMax(); + modStatus(); + + //Update the status + if (return_modStatus == 1) { + batt_status_output = 1; + } else { + batt_status_output = batt_status_output; + } + + //Update the max value + if (return_modMax > batt_max_output) { + batt_max_output = return_modMax; + } else { + batt_max_output = batt_max_output; + } + + //Update the min value + if (return_modMin < batt_min_output) { + batt_min_output = return_modMin; + } else { + batt_min_output = batt_min_output; + } +} + +void batteryDiag() +{ + //Initializing the battery values + batt_max_output = 3000.25f; + batt_min_output = -3000.25f; + batt_status_output = 0; + + //Run the diagnostics, one module at the time + moduleDiag(0); +} + + +void main() +{ + //Non-det assignment of all global C variables + return_modMin = 0.0f; + return_modMax = 0.0f; + return_modStatus = 0; + mod0_status = 0; + mod0_min = 0.0f; + mod0_max = 0.0f; + + //Declare the paramters of the function to be called + + //Function call that the harness function verifies + batteryDiag(); + + //The 'ensures'-clauses translated into asserts + //assert((!(((old_mod0_status == 0) && (old_mod1_status == 0)) && + //!(batt_status_output == 0)) && !(((old_mod0_status == 1) || + //(old_mod1_status == 1)) && !(batt_status_output == 1)))); + assert(batt_max_output <= 3000.25f); +} diff --git a/regression-tests/float/init_1.c b/regression-tests/float/init_1.c new file mode 100644 index 00000000..da28ff2e --- /dev/null +++ b/regression-tests/float/init_1.c @@ -0,0 +1,6 @@ +int main() { + float a = 0.0f; + assert(a == 0.0f); + return 0; + +} diff --git a/regression-tests/float/init_2.c b/regression-tests/float/init_2.c new file mode 100644 index 00000000..6d11b62d --- /dev/null +++ b/regression-tests/float/init_2.c @@ -0,0 +1,5 @@ +int main() { + float a = 4.24242f; + assert(a == 4.24242f); + return 0; +} diff --git a/regression-tests/float/init_3.c b/regression-tests/float/init_3.c new file mode 100644 index 00000000..c4dab6cf --- /dev/null +++ b/regression-tests/float/init_3.c @@ -0,0 +1,6 @@ +int main() { + float a = 4.24242f; + assert(a == 4.24241f); + return 0; + +} diff --git a/regression-tests/float/int_plus_float.c b/regression-tests/float/int_plus_float.c new file mode 100644 index 00000000..05ccf844 --- /dev/null +++ b/regression-tests/float/int_plus_float.c @@ -0,0 +1,7 @@ +int main () +{ + float a = 2.0f; + int b = 1; + assert(a+b == 3.0f); + return 0; +} diff --git a/regression-tests/float/leq_1.c b/regression-tests/float/leq_1.c new file mode 100644 index 00000000..24d24696 --- /dev/null +++ b/regression-tests/float/leq_1.c @@ -0,0 +1,5 @@ +int main() { + float a = 2.3f; + float b = 2.25f;; + assert(b <= a); +} diff --git a/regression-tests/float/leq_2.c b/regression-tests/float/leq_2.c new file mode 100644 index 00000000..52f41fe4 --- /dev/null +++ b/regression-tests/float/leq_2.c @@ -0,0 +1,8 @@ +int main() { + float a = -32.23f; + float b = -54.425f; + assert(a < b); + +} + + diff --git a/regression-tests/float/loop_1.c b/regression-tests/float/loop_1.c new file mode 100644 index 00000000..95052c65 --- /dev/null +++ b/regression-tests/float/loop_1.c @@ -0,0 +1,11 @@ +void main() { + int i = 0; + float x = 0.5f; + float y = x; + while (x < 3000.0f) { + x = x*2.0f; + y = x; + ++i; + } + assert(x==y); +} \ No newline at end of file diff --git a/regression-tests/float/loop_2.c b/regression-tests/float/loop_2.c new file mode 100644 index 00000000..eb4edca3 --- /dev/null +++ b/regression-tests/float/loop_2.c @@ -0,0 +1,14 @@ +int N = _; + +void main(void) { + int i = 0; + float x = 0.5f; + float y = x; + while (i < N) { + if(x == y) { + x = x+2.25f; + } + ++i; + } + assert(x==y); +} diff --git a/regression-tests/float/mul_1.c b/regression-tests/float/mul_1.c new file mode 100644 index 00000000..c9753339 --- /dev/null +++ b/regression-tests/float/mul_1.c @@ -0,0 +1,6 @@ +int main () { + float a = 4.0f; + float b = 2.0f; + assert(a*b== 8.0f); + return 0; +} diff --git a/regression-tests/float/mul_2.c b/regression-tests/float/mul_2.c new file mode 100644 index 00000000..9e07d77d --- /dev/null +++ b/regression-tests/float/mul_2.c @@ -0,0 +1,6 @@ +int main () { + float a = 4.0f; + float b = 0.5f; + assert(a*b== 2.001f); + return 0; +} diff --git a/regression-tests/float/nan.c b/regression-tests/float/nan.c new file mode 100644 index 00000000..c3a323b2 --- /dev/null +++ b/regression-tests/float/nan.c @@ -0,0 +1,7 @@ +int main() +{ + float x = _; + + assert(x==x); + return 0; +} diff --git a/regression-tests/float/nan_create.c b/regression-tests/float/nan_create.c new file mode 100644 index 00000000..967a9276 --- /dev/null +++ b/regression-tests/float/nan_create.c @@ -0,0 +1,4 @@ +int main() { + float nan = 0/0; + assert(nan == 2); +} diff --git a/regression-tests/float/nan_range.c b/regression-tests/float/nan_range.c new file mode 100644 index 00000000..13ebeade --- /dev/null +++ b/regression-tests/float/nan_range.c @@ -0,0 +1,10 @@ +int main() +{ + float x = _; + + if (x >= -0.00001f && x <= -0.00001f) { + assert(x==x); + } + return 0; +} + diff --git a/regression-tests/float/nondet_1.c b/regression-tests/float/nondet_1.c new file mode 100644 index 00000000..2b08d474 --- /dev/null +++ b/regression-tests/float/nondet_1.c @@ -0,0 +1,5 @@ +int main() { + float x = _; + float y = x + 1.0f; + assert(y>=x); +} diff --git a/regression-tests/float/nondet_2.c b/regression-tests/float/nondet_2.c new file mode 100644 index 00000000..6ee31b80 --- /dev/null +++ b/regression-tests/float/nondet_2.c @@ -0,0 +1,5 @@ +int main() { + float x = _; + float y = x + 1.0f; + assert(y&1 | grep -v 'at ' +done + diff --git a/regression-tests/float/simple_bsed_orig_code.c b/regression-tests/float/simple_bsed_orig_code.c new file mode 100644 index 00000000..aac6f486 --- /dev/null +++ b/regression-tests/float/simple_bsed_orig_code.c @@ -0,0 +1,87 @@ +//Global variables 'acting' as return variables +int return_modMin; +int return_modMax; +int return_modStatus; + +int mod0_status; +int mod1_status; + +int mod0_min; +int mod1_min; + +int mod0_max; +int mod1_max; + +int batt_min_output; +int batt_max_output; +int batt_status_output; + +void modStatus(int idx) { + if (idx == 0) { + return_modStatus = mod0_status; + } else { + return_modStatus = mod1_status; + } +} + +void modMin(int idx) { + if (idx == 0) { + return_modMin = mod0_min; + } else { + return_modMin = mod1_min; + } +} + +void modMax(int idx) { + if (idx == 0) { + return_modMax = mod0_max; + } else { + return_modMax = mod1_max; + } +} + +void moduleDiag(int idx) { + modMin(idx); + modMax(idx); + modStatus(idx); + + //Update the status + if (return_modStatus == 1) { + batt_status_output = 1; + } else { + batt_status_output = batt_status_output; + } + + //Update the max value + if (return_modMax > batt_max_output) { + batt_max_output = return_modMax; + } else { + batt_max_output = batt_max_output; + } + + //Update the min value + if (return_modMin < batt_min_output) { + batt_min_output = return_modMin; + } else { + batt_min_output = batt_min_output; + } +} + +/*@ + assigns return_modMax, return_modMin, return_modStatus, batt_min_output, + batt_max_output, batt_status_output; + ensures + ((\old(mod0_status) == 0 && \old(mod1_status) == 0) ==> batt_status_output == 0) && + ((\old(mod0_status) == 1 || \old(mod1_status) == 1) ==> batt_status_output == 1); +*/ +void batteryDiag(int dummy) +{ + //Initializing the battery values + batt_max_output = -2147483648; + batt_min_output = 2147483647; + batt_status_output = 0; + + //Run the diagnostics, one module at the time + moduleDiag(0); + moduleDiag(1); +} diff --git a/regression-tests/float/simple_bsed_test.c b/regression-tests/float/simple_bsed_test.c new file mode 100644 index 00000000..1340863c --- /dev/null +++ b/regression-tests/float/simple_bsed_test.c @@ -0,0 +1,124 @@ +#include +//Global variables 'acting' as return variables +float return_modMin; +float return_modMax; +int return_modStatus; + +int mod0_status; +int mod1_status; + +float mod0_min; +float mod1_min; + +float mod0_max; +float mod1_max; + +float batt_min_output; +float batt_max_output; +int batt_status_output; + +/*@contract@*/ +void modStatus(int idx) { + if (idx == 0) { + return_modStatus = mod0_status; + } else { + return_modStatus = mod1_status; + } +} + +/*@contract@*/ +void modMin(int idx) { + if (idx == 0) { + return_modMin = mod0_min; + } else { + return_modMin = mod1_min; + } +} + +/*@contract@*/ +void modMax(int idx) { + if (idx == 0) { + return_modMax = mod0_max; + } else { + return_modMax = mod1_max; + } +} + +/*@contract@*/ +void moduleDiag(int idx) { + modMin(idx); + modMax(idx); + modStatus(idx); + + //Update the status + if (return_modStatus == 1) { + batt_status_output = 1; + } else { + batt_status_output = batt_status_output; + } + + //Update the max value + if (return_modMax > batt_max_output) { + batt_max_output = return_modMax; + } else { + batt_max_output = batt_max_output; + } + + //Update the min value + if (return_modMin < batt_min_output) { + batt_min_output = return_modMin; + } else { + batt_min_output = batt_min_output; + } +} + +void batteryDiag(int dummy) +{ + //Initializing the battery values + batt_max_output = 5.0f; + batt_min_output = -5.0f; + batt_status_output = 0; + + //Run the diagnostics, one module at the time + moduleDiag(0); + moduleDiag(1); +} +int extern non_det(); + +int main() +{ + //Non-det assignment of all global C variables + // return_modMin = 0.0f; + // return_modMax = 0.0f; + // return_modStatus = 0; + mod0_status = 0; + mod1_status = 1; + mod0_min = -1.0f; + mod1_min = -1.0f; + mod0_max = 2.0f; + mod1_max = 2.0f; + // batt_max_output = -200.0f; + //batt_min_output = 200.0f; + // batt_status_output = 0; + + //Declare the paramters of the function to be called + int dummy = 0; + + //Initialization of logical old-variables + // int old_mod0_status; + // int old_mod1_status; + // int old_batt_status_output; + // assume(old_mod0_status == mod0_status); + // assume(old_mod1_status == mod1_status); + // assume(old_batt_status_output == batt_status_output); + + //Function call that the harness function verifies + batteryDiag(dummy); + + //The 'ensures'-clauses translated into asserts + // assert((!(((old_mod0_status == 0) && (old_mod1_status == 0)) && + // !(batt_status_output == 0)) && !(((old_mod0_status == 1) || + // (old_mod1_status == 1)) && !(batt_status_output == 1)))); + printf("%f", batt_max_output); + return 0; +} diff --git a/regression-tests/float/simple_bsed_tricera.c b/regression-tests/float/simple_bsed_tricera.c new file mode 100644 index 00000000..fe2373d1 --- /dev/null +++ b/regression-tests/float/simple_bsed_tricera.c @@ -0,0 +1,115 @@ +//Global variables 'acting' as return variables +int return_modMin; +int return_modMax; +int return_modStatus; + +int mod0_status; +int mod1_status; + +int mod0_min; +int mod1_min; + +int mod0_max; +int mod1_max; + +int batt_min_output; +int batt_max_output; +int batt_status_output; + +void modStatus(int idx) { + if (idx == 0) { + return_modStatus = mod0_status; + } else { + return_modStatus = mod1_status; + } +} + +void modMin(int idx) { + if (idx == 0) { + return_modMin = mod0_min; + } else { + return_modMin = mod1_min; + } +} + +void modMax(int idx) { + if (idx == 0) { + return_modMax = mod0_max; + } else { + return_modMax = mod1_max; + } +} + +void moduleDiag(int idx) { + modMin(idx); + modMax(idx); + modStatus(idx); + + //Update the status + if (return_modStatus == 1) { + batt_status_output = 1; + } else { + batt_status_output = batt_status_output; + } + + //Update the max value + if (return_modMax > batt_max_output) { + batt_max_output = return_modMax; + } else { + batt_max_output = batt_max_output; + } + + //Update the min value + if (return_modMin < batt_min_output) { + batt_min_output = return_modMin; + } else { + batt_min_output = batt_min_output; + } +} + +void batteryDiag(int dummy) +{ + //Initializing the battery values + batt_max_output = -30000000000.5f; + batt_min_output = 30000000000.5f; + batt_status_output = 0; + + //Run the diagnostics, one module at the time + moduleDiag(0); + moduleDiag(1); +} + +int extern non_det(); + +void main() +{ + //Non-det assignment of all global C variables + return_modMin = non_det(); + return_modMax = non_det(); + return_modStatus = non_det(); + mod0_status = non_det(); + mod1_status = non_det(); + mod0_min = non_det(); + mod1_min = non_det(); + mod0_max = non_det(); + mod1_max = non_det(); + + //Declare the paramters of the function to be called + int dummy; + + //Initialization of logical old-variables + int old_mod0_status; + int old_mod1_status; + int old_batt_status_output; + assume(old_mod0_status == mod0_status); + assume(old_mod1_status == mod1_status); + assume(old_batt_status_output == batt_status_output); + + //Function call that the harness function verifies + batteryDiag(dummy); + + //The 'ensures'-clauses translated into asserts + assert((!(((old_mod0_status == 0) && (old_mod1_status == 0)) && + !(batt_status_output == 0)) && !(((old_mod0_status == 1) || + (old_mod1_status == 1)) && !(batt_status_output == 1)))); +} diff --git a/regression-tests/float/sub_1.c b/regression-tests/float/sub_1.c new file mode 100644 index 00000000..2a8339d0 --- /dev/null +++ b/regression-tests/float/sub_1.c @@ -0,0 +1,7 @@ +int main() { + float a = 4.0f; + float b = 2.0f; + assert(a-b== 2.0f); + return 0; + +} diff --git a/regression-tests/float/sub_2.c b/regression-tests/float/sub_2.c new file mode 100644 index 00000000..03d9d6b7 --- /dev/null +++ b/regression-tests/float/sub_2.c @@ -0,0 +1,6 @@ +int main() { + float a = 3.0f; + float b = 0.5f; + assert(a-b == 2.501f); + return 0; +} diff --git a/regression-tests/long_double/Answers b/regression-tests/long_double/Answers new file mode 100644 index 00000000..558203ff --- /dev/null +++ b/regression-tests/long_double/Answers @@ -0,0 +1,42 @@ + +add_1.c +SAFE + +add_2.c +SAFE + +add_3.c +UNSAFE + +div_1.c +SAFE + +div_2.c +UNSAFE + +mul_1.c +SAFE + +mul_2.c +UNSAFE + +loop_1.c +SAFE + +loop_2.c +UNSAFE + +sub_1.c +SAFE + +sub_2.c +UNSAFE + +init_1.c +SAFE + +init_2.c +SAFE + +init_3.c +UNSAFE diff --git a/regression-tests/long_double/add_1.c b/regression-tests/long_double/add_1.c new file mode 100644 index 00000000..282155ec --- /dev/null +++ b/regression-tests/long_double/add_1.c @@ -0,0 +1,6 @@ +int main () { + long double a = 4.0l; + long double b = 2.0l; + assert(a+b== 6.0l); + return 0; +} diff --git a/regression-tests/long_double/add_2.c b/regression-tests/long_double/add_2.c new file mode 100644 index 00000000..02b2cd8d --- /dev/null +++ b/regression-tests/long_double/add_2.c @@ -0,0 +1,6 @@ +int main() { + long double a = 3.0l; + long double b = 0.5l; + assert(a+b == 3.5l); + return 0; +} diff --git a/regression-tests/long_double/add_3.c b/regression-tests/long_double/add_3.c new file mode 100644 index 00000000..c8c6fe24 --- /dev/null +++ b/regression-tests/long_double/add_3.c @@ -0,0 +1,5 @@ +int main() { + long double a = 2.0l; + long double b = a + 0.5l; + assert(a + 0.4l == b); +} diff --git a/regression-tests/long_double/div_1.c b/regression-tests/long_double/div_1.c new file mode 100644 index 00000000..00469762 --- /dev/null +++ b/regression-tests/long_double/div_1.c @@ -0,0 +1,6 @@ +int main () { + long double a = 4.0l; + long double b = 2.0l; + assert(a/b== 2.0l); + return 0; +} diff --git a/regression-tests/long_double/div_2.c b/regression-tests/long_double/div_2.c new file mode 100644 index 00000000..af8d9bc1 --- /dev/null +++ b/regression-tests/long_double/div_2.c @@ -0,0 +1,6 @@ +int main () { + long double a = 4.0l; + long double b = 0.5l; + assert(a/b== 9.0l); + return 0; +} diff --git a/regression-tests/long_double/init_1.c b/regression-tests/long_double/init_1.c new file mode 100644 index 00000000..b5de3f06 --- /dev/null +++ b/regression-tests/long_double/init_1.c @@ -0,0 +1,6 @@ +int main() { + long double a = 0.0l; + assert(a == 0.0l); + return 0; + +} diff --git a/regression-tests/long_double/init_2.c b/regression-tests/long_double/init_2.c new file mode 100644 index 00000000..50a2d788 --- /dev/null +++ b/regression-tests/long_double/init_2.c @@ -0,0 +1,5 @@ +int main() { + long double a = 4.24242l; + assert(a == 4.24242l); + return 0; +} diff --git a/regression-tests/long_double/init_3.c b/regression-tests/long_double/init_3.c new file mode 100644 index 00000000..6be926fc --- /dev/null +++ b/regression-tests/long_double/init_3.c @@ -0,0 +1,6 @@ +int main() { + long double a = 4.24242l; + assert(a == 4.24241l); + return 0; + +} diff --git a/regression-tests/long_double/int_plus_float.c b/regression-tests/long_double/int_plus_float.c new file mode 100644 index 00000000..2fcbf907 --- /dev/null +++ b/regression-tests/long_double/int_plus_float.c @@ -0,0 +1,7 @@ +int main () +{ + long double a = 2.0l; + int b = 1; + assert(a+b == 3.0l); + return 0; +} diff --git a/regression-tests/long_double/leq_1.c b/regression-tests/long_double/leq_1.c new file mode 100644 index 00000000..67d8cb93 --- /dev/null +++ b/regression-tests/long_double/leq_1.c @@ -0,0 +1,5 @@ +int main() { + long double a = 2.3l; + long double b = 2.25l;; + assert(b <= a); +} diff --git a/regression-tests/long_double/loop_1.c b/regression-tests/long_double/loop_1.c new file mode 100644 index 00000000..e592915e --- /dev/null +++ b/regression-tests/long_double/loop_1.c @@ -0,0 +1,11 @@ +void main(void) { + int i = 0; + long double x = 0.5l; + long double y = x; + while (x < 3000.0l) { + x = x*2.0l; + y = x; + ++i; + } + assert(x==y); +} diff --git a/regression-tests/long_double/loop_2.c b/regression-tests/long_double/loop_2.c new file mode 100644 index 00000000..aec3f6f5 --- /dev/null +++ b/regression-tests/long_double/loop_2.c @@ -0,0 +1,14 @@ +int N = _; + +void main(void) { + int i = 0; + long double x = 0.5l; + long double y = x; + while (i < N) { + if(x == y) { + x = x+2.25l; + } + ++i; + } + assert(x==y); +} diff --git a/regression-tests/long_double/mul_1.c b/regression-tests/long_double/mul_1.c new file mode 100644 index 00000000..1a93c1ac --- /dev/null +++ b/regression-tests/long_double/mul_1.c @@ -0,0 +1,6 @@ +int main () { + long double a = 4.0l; + long double b = 2.0l; + assert(a*b== 8.0l); + return 0; +} diff --git a/regression-tests/long_double/mul_2.c b/regression-tests/long_double/mul_2.c new file mode 100644 index 00000000..49d1284b --- /dev/null +++ b/regression-tests/long_double/mul_2.c @@ -0,0 +1,6 @@ +int main () { + long double a = 4.0l; + long double b = 0.5l; + assert(a*b== 2.01l); + return 0; +} diff --git a/regression-tests/long_double/nan.c b/regression-tests/long_double/nan.c new file mode 100644 index 00000000..376357f8 --- /dev/null +++ b/regression-tests/long_double/nan.c @@ -0,0 +1,7 @@ +int main() +{ + double x = _; + + assert(x==x); + return 0; +} diff --git a/regression-tests/long_double/nan_create.c b/regression-tests/long_double/nan_create.c new file mode 100644 index 00000000..9440e44b --- /dev/null +++ b/regression-tests/long_double/nan_create.c @@ -0,0 +1,4 @@ +int main() { + double nan = 0/0; + assert(nan == 2); +} diff --git a/regression-tests/long_double/nan_range.c b/regression-tests/long_double/nan_range.c new file mode 100644 index 00000000..73184580 --- /dev/null +++ b/regression-tests/long_double/nan_range.c @@ -0,0 +1,10 @@ +int main() +{ + double x = _; + + if (x >= -0.00001f && x <= -0.00001f) { + assert(x==x); + } + return 0; +} + diff --git a/regression-tests/long_double/nondet_1.c b/regression-tests/long_double/nondet_1.c new file mode 100644 index 00000000..7dbca4f8 --- /dev/null +++ b/regression-tests/long_double/nondet_1.c @@ -0,0 +1,6 @@ +int main() { + double x = _; + double y = x + 1.0l; + assert(y>x); + +} diff --git a/regression-tests/long_double/nondet_2.c b/regression-tests/long_double/nondet_2.c new file mode 100644 index 00000000..e4c3c1a7 --- /dev/null +++ b/regression-tests/long_double/nondet_2.c @@ -0,0 +1,5 @@ +int main() { + double x = _; + double y = x + 1.0l; + assert(y&1 | grep -v 'at ' +done + diff --git a/regression-tests/long_double/sub_1.c b/regression-tests/long_double/sub_1.c new file mode 100644 index 00000000..a9d12f8a --- /dev/null +++ b/regression-tests/long_double/sub_1.c @@ -0,0 +1,8 @@ +int main() { + long double a = 1.0l; + long double b = 0.5l; + assert(a-b == 0.5l); + + return 0; + +} diff --git a/regression-tests/long_double/sub_2.c b/regression-tests/long_double/sub_2.c new file mode 100644 index 00000000..a1028edc --- /dev/null +++ b/regression-tests/long_double/sub_2.c @@ -0,0 +1,6 @@ +int main() { + double a = 3.0l; + double b = 0.5l; + assert(a-b == 2.5l); + return 0; +} diff --git a/regression-tests/misc/INFINITY_macro.c b/regression-tests/misc/INFINITY_macro.c new file mode 100644 index 00000000..16521bcb --- /dev/null +++ b/regression-tests/misc/INFINITY_macro.c @@ -0,0 +1,6 @@ +#include + +int main() { + float inf = INFINITY; + assert(isinf(inf)); +} \ No newline at end of file diff --git a/regression-tests/misc/NAN_macro.c b/regression-tests/misc/NAN_macro.c new file mode 100644 index 00000000..81ea5e53 --- /dev/null +++ b/regression-tests/misc/NAN_macro.c @@ -0,0 +1,6 @@ +#include + +int main() { + float NaN = NAN; + assert(isnan(NaN)); +} \ No newline at end of file diff --git a/regression-tests/misc/int-test.c b/regression-tests/misc/int-test.c new file mode 100644 index 00000000..c1354f1a --- /dev/null +++ b/regression-tests/misc/int-test.c @@ -0,0 +1,6 @@ +int main() { + int a = 1; + int b = 2; + assert(a+b==3); +} + diff --git a/regression-tests/runalldirs b/regression-tests/runalldirs index 0e8b91fe..bdb8adbd 100755 --- a/regression-tests/runalldirs +++ b/regression-tests/runalldirs @@ -25,6 +25,9 @@ run_test ./rundir math-arrays "" -assert -dev -t:60 run_test ./rundir quantifiers "" -assert -dev -t:60 run_test ./rundir interpreted-predicates "" -assert -dev -t:60 run_test ./rundir properties "" -assert -dev -t:60 +run_test ./rundir float "" -assert -dev -t:60 +run_test ./rundir double "" -assert -dev -t:60 +run_test ./rundir long_double "" -assert -dev -t:60 #run_test ./rundir ParametricEncoder "" if [ $ERRORS -ne 0 ]; then diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala index baa51351..9f0b99c0 100644 --- a/src/tricera/Main.scala +++ b/src/tricera/Main.scala @@ -270,14 +270,18 @@ class Main (args: Array[String]) { val cppFileName = if (cPreprocessor) { val preprocessedFile = File.createTempFile("tri-", ".i") System.setOut(new PrintStream(new FileOutputStream(preprocessedFile))) - val cmdLine = Seq("cpp", fileName, "-E", "-P", "-CC") - try Process(cmdLine) ! + val cmdLine = "cpp " + fileName + " -E -P -CC" + try { + cmdLine ! + } catch { case _: Throwable => - throw new Main.MainException("The C preprocessor could not" + - " be executed (option -cpp). This might be due cpp not being " + - "installed in the system.\n" + "Attempted command: " + - cmdLine.mkString(" ")) + throw new Main.MainException("The preprocessor could not" + + " be executed. This might be due to TriCera preprocessor binary " + + "not being in the current directory. Alternatively, use the " + + "-noPP switch to disable the preprocessor.\n" + + "Preprocessor command: " + cmdLine + ) } preprocessedFile.deleteOnExit() preprocessedFile.getAbsolutePath diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala index be7f2cdc..acd3ab3d 100644 --- a/src/tricera/concurrency/CCReader.scala +++ b/src/tricera/concurrency/CCReader.scala @@ -29,9 +29,9 @@ package tricera.concurrency -import ap.basetypes.IdealInt +import ap.basetypes.{IdealInt, IdealRat} import ap.parser._ -import ap.theories.{ADT, ExtArray, Heap, ModuloArithmetic} +import ap.theories.{ADT, ExtArray, Heap, ModuloArithmetic, rationals} import ap.types.{MonoSortedIFunction, MonoSortedPredicate, SortedConstantTerm} import concurrent_c._ import concurrent_c.Absyn._ @@ -39,7 +39,7 @@ import hornconcurrency.ParametricEncoder import lazabs.horn.abstractions.VerificationHints import lazabs.horn.abstractions.VerificationHints.{VerifHintElement, VerifHintInitPred, VerifHintTplElement, VerifHintTplEqTerm, VerifHintTplPred} import lazabs.horn.bottomup.HornClauses -import IExpression.{ConstantTerm, Predicate, Sort, toFunApplier} +import IExpression.{ConstantTerm, Predicate, Sort, i, toFunApplier} import scala.collection.mutable.{ArrayBuffer, Buffer, Stack, HashMap => MHashMap, HashSet => MHashSet} import tricera.Util._ @@ -51,6 +51,12 @@ import tricera.parsers.AnnotationParser import tricera.parsers.AnnotationParser._ import CCExceptions._ import tricera.{Util, properties} +import tricera.concurrency.Floats.floatToFraction +import tricera.concurrency.Doubles.doubleToFraction +import tricera.concurrency.LongDoubles.longDoubleToFraction + +import ap.theories.rationals.Rationals +import ap.theories.rationals.Rationals.Fraction object CCReader { private[concurrency] var useTime = false @@ -113,6 +119,7 @@ object CCReader { object ArithmeticMode extends Enumeration { val Mathematical, ILP32, LP64, LLP64 = Value } + ////////////////////////////////////////////////////////////////////////////// class CCClause(val clause : HornClauses.Clause, val srcInfo : Option[SourceInfo]) { @@ -354,7 +361,6 @@ class CCReader private (prog : Program, res } - ////////////////////////////////////////////////////////////////////////////// private val channels = new MHashMap[String, ParametricEncoder.CommChannel] @@ -2147,6 +2153,12 @@ private def collectVarDecls(dec : Dec, // ignore case _ : Tchar => // ignore + case _ : Tfloat => + typ = CCFloat + case _: Tdouble if typ == CCLong => + typ = CCLongDouble + case _: Tdouble => + typ = CCDouble case _ : Tsigned => typ = CCInt case _ : Tunsigned => @@ -3976,9 +3988,24 @@ private def collectVarDecls(dec : Dec, pushVal(CCTerm(IdealInt(constant.octallong_.substring( 0, constant.octallong_.size - 1), 8), CCLong, srcInfo)) // case constant : Eoctalunslong. Constant ::= OctalUnsLong; -// case constant : Ecdouble. Constant ::= CDouble; -// case constant : Ecfloat. Constant ::= CFloat; -// case constant : Eclongdouble. Constant ::= CLongDouble; + case constant : Ecfloat => + //val frac : (String, String) = floatToFraction(constant.cfloat_) + val (num, denum) = floatToFraction(constant.cfloat_) + val floatData = Fraction(i((IdealInt(num))), i(IdealInt(denum))) + pushVal(CCTerm(FloatADT.floatCtor(floatData), + CCFloat, Some(getSourceInfo(constant)))) + // assertProperty(FloatADT.isFloat(floatData), None)) // todo: just an example of adding an implicit assertion + // addGuard(FloatADT.isFloat(floatData)) // todo: just an example of adding an assumption + case constant : Ecdouble => + val (num, denum) = doubleToFraction(constant.cdouble_) + val doubleData = Fraction(i((IdealInt(num))), i(IdealInt(denum))) + pushVal(CCTerm(DoubleADT.doubleCtor(doubleData), + CCDouble, Some(getSourceInfo(constant)))) + case constant : Eclongdouble => + val (num, denum) = doubleToFraction(constant.clongdouble_.dropRight(1)) + val longDoubleData = Fraction(i((IdealInt(num))), i(IdealInt(denum))) + pushVal(CCTerm(LongDoubleADT.longDoubleCtor(longDoubleData), + CCLongDouble, Some(getSourceInfo(constant)))) case constant : Eint => pushVal(CCTerm(IExpression.i(IdealInt( constant.unboundedinteger_)), CCInt, srcInfo)) diff --git a/src/tricera/concurrency/Floating-Point.scala b/src/tricera/concurrency/Floating-Point.scala new file mode 100644 index 00000000..4383aaf6 --- /dev/null +++ b/src/tricera/concurrency/Floating-Point.scala @@ -0,0 +1,337 @@ + +package tricera.concurrency + +import ap.parser._ +import ap.theories.rationals.Rationals +import ap.theories.{ADT} +import ap.types.{MonoSortedIFunction} + + ////////////////////////////////////////////////////////////////////////////// + // Long Doubles + object LongDoubleADT { + private val longDoubleADTCtorSignatures: Seq[(String, ADT.CtorSignature)] = Seq( + ("longDoubleData", ADT.CtorSignature( + Seq(("getLongDouble", ADT.OtherSort(Rationals.dom))), ADT.ADTSort(0))), + ("NaN", ADT.CtorSignature(Nil, ADT.ADTSort(0))), + ("plusInfinity", ADT.CtorSignature(Nil, ADT.ADTSort(0))), + ("negativeInfinity", ADT.CtorSignature(Nil, ADT.ADTSort(0))) + ) + + val longDoubleADT = new ADT(sortNames = Seq("longDoubleADT"), + longDoubleADTCtorSignatures) + val sort = longDoubleADT.sorts.head + + val longDoubleCtor: MonoSortedIFunction = longDoubleADT.constructors(0) + val getData: MonoSortedIFunction = longDoubleADT.selectors(0)(0) + + val nan: ITerm = IFunApp(longDoubleADT.constructors(1), Nil) + val plusInf: ITerm = IFunApp(longDoubleADT.constructors(2), Nil) + val negInf: ITerm = IFunApp(longDoubleADT.constructors(3), Nil) + + def isFloat(t: ITerm): IFormula = longDoubleADT.hasCtor(t, 0) + + def isNan(t: ITerm): IFormula = longDoubleADT.hasCtor(t, 1) + + def isPlusinf(t: ITerm): IFormula = longDoubleADT.hasCtor(t, 2) + + def isNeginf(t: ITerm): IFormula = longDoubleADT.hasCtor(t, 3) + } + + object LongDoubles { + + import scala.util.control._ + import scala.math._ + + // todo: uses the same implementation as Doubles right now. Should be fixed + def longDoubleToFraction(fp: String): (String, String) = { + val f: Double = fp.toDouble + println("Warning: wrong implementation for converting Long Doubles to Doubles") + if (f.isNaN) { + ("0", "0") + } + else if (f.isInfinity) { + ("0", "0") + } + else { + val mantissaBits: Long = (java.lang.Double.doubleToLongBits(f) << 12 >>> 12) + val mantissa: String = String.format("%52s", java.lang.Long.toBinaryString(mantissaBits)).replace(' ', '0') + + val exponentBits: Long = (java.lang.Double.doubleToLongBits(f) << 1 >>> 53) + val exponent: String = String.format("%11s", java.lang.Long.toBinaryString(exponentBits)).replace(' ', '0') + + val signBit = (java.lang.Double.doubleToLongBits(f) >>> 63).toBinaryString + + var bitCount: Int = 53 + var denominator: BigInt = 1 + var numerator: BigInt = 0 + + //Get the denominator from the mantissa + var loop = new Breaks + loop.breakable { + for (bit <- mantissa.reverse) { + if (bit == '1') { + denominator = BigInt(2).pow(bitCount) + loop.break() + } + bitCount = bitCount - 1 + } + } + + // reset bitCount + bitCount = 1 + numerator = denominator + //Get the numerator from the mantissa + for (bit <- mantissa) { + if (bit == '1') { + numerator = numerator + denominator / BigInt(2).pow(bitCount) + } + bitCount = bitCount + 1 + } + + bitCount = 0 + // Get the exponent + var exponentInt: Int = -pow(2, exponent.length() - 1).toInt + 1 + for (bit <- exponent.reverse) { + if (bit == '1') { + exponentInt = exponentInt + pow(2, bitCount).toInt + } + bitCount = bitCount + 1 + } + + if (exponentInt > 0) { + numerator = numerator * BigInt(2).pow(exponentInt) + } + if (exponentInt < 0) { + denominator = denominator * BigInt(2).pow(abs(exponentInt)) + } + // Case for when the float is 0 + if (exponentInt == -pow(2, exponent.length() - 1).toInt + 1 && numerator == 1) { + numerator = 0 + denominator = 1 + } + if (signBit == "1") { + numerator = -numerator + } + (numerator.toString, denominator.toString) + } + } + } + + ////////////////////////////////////////////////////////////////////////////// + // Doubles + object DoubleADT { + private val doubleADTCtorSignatures: Seq[(String, ADT.CtorSignature)] = Seq( + ("doubleData", ADT.CtorSignature( + Seq(("getDouble", ADT.OtherSort(Rationals.dom))), ADT.ADTSort(0))), + ("NaN", ADT.CtorSignature(Nil, ADT.ADTSort(0))), + ("plusInfinity", ADT.CtorSignature(Nil, ADT.ADTSort(0))), + ("negativeInfinity", ADT.CtorSignature(Nil, ADT.ADTSort(0))) + ) + + val doubleADT = new ADT(sortNames = Seq("doubleADT"), + doubleADTCtorSignatures) + val sort = doubleADT.sorts.head + + val doubleCtor: MonoSortedIFunction = doubleADT.constructors(0) + val getData: MonoSortedIFunction = doubleADT.selectors(0)(0) + + val nan: ITerm = IFunApp(doubleADT.constructors(1), Nil) + val plusInf: ITerm = IFunApp(doubleADT.constructors(2), Nil) + val negInf: ITerm = IFunApp(doubleADT.constructors(3), Nil) + + def isFloat(t: ITerm): IFormula = doubleADT.hasCtor(t, 0) + + def isNan(t: ITerm): IFormula = doubleADT.hasCtor(t, 1) + + def isPlusinf(t: ITerm): IFormula = doubleADT.hasCtor(t, 2) + + def isNeginf(t: ITerm): IFormula = doubleADT.hasCtor(t, 3) + } + + object Doubles { + import scala.util.control._ + import scala.math._ + def doubleToFraction(fp: String): (String, String) = { + val f: Double = fp.toDouble + if (f.isNaN) { + ("0", "0") + } + else if (f.isInfinity) { + ("1", "0") + } + else { + val mantissaBits: Long = (java.lang.Double.doubleToLongBits(f) << 12 >>> 12) + val mantissa: String = String.format("%52s", java.lang.Long.toBinaryString(mantissaBits)).replace(' ', '0') + + val exponentBits: Long = (java.lang.Double.doubleToLongBits(f) << 1 >>> 53) + val exponent: String = String.format("%11s", java.lang.Long.toBinaryString(exponentBits)).replace(' ', '0') + + val signBit = (java.lang.Double.doubleToLongBits(f) >>> 63).toBinaryString + + var bitCount: Int = 53 + var denominator: BigInt = 1 + var numerator: BigInt = 0 + + //Get the denominator from the mantissa + var loop = new Breaks + loop.breakable { + for (bit <- mantissa.reverse) { + if (bit == '1') { + denominator = BigInt(2).pow(bitCount) + loop.break() + } + bitCount = bitCount - 1 + } + } + + // reset bitCount + bitCount = 1 + numerator = denominator + //Get the numerator from the mantissa + for (bit <- mantissa) { + if (bit == '1') { + numerator = numerator + denominator / BigInt(2).pow(bitCount) + } + bitCount = bitCount + 1 + } + + bitCount = 0 + // Get the exponent + var exponentInt: Int = -pow(2, exponent.length() - 1).toInt + 1 + for (bit <- exponent.reverse) { + if (bit == '1') { + exponentInt = exponentInt + pow(2, bitCount).toInt + } + bitCount = bitCount + 1 + } + + if (exponentInt > 0) { + numerator = numerator * BigInt(2).pow(exponentInt) + } + if (exponentInt < 0) { + denominator = denominator * BigInt(2).pow(abs(exponentInt)) + } + // Case for when the float is 0 + if (exponentInt == -pow(2, exponent.length() - 1).toInt + 1 && numerator == 1) { + numerator = 0 + denominator = 1 + } + if (signBit == "1") { + numerator = -numerator + } + (numerator.toString, denominator.toString) + } + } + } + + ////////////////////////////////////////////////////////////////////////////// + // Floats + object FloatADT { + private val floatADTCtorSignatures : Seq[(String, ADT.CtorSignature)] = Seq( + ("floatData", ADT.CtorSignature( + Seq(("getFloat", ADT.OtherSort(Rationals.dom))), ADT.ADTSort(0))), + ("NaN", ADT.CtorSignature(Nil, ADT.ADTSort(0))), + ("plusInfinity", ADT.CtorSignature(Nil, ADT.ADTSort(0))), + ("negativeInfinity", ADT.CtorSignature(Nil, ADT.ADTSort(0))) + ) + + val floatADT = new ADT(sortNames = Seq("floatADT"), + floatADTCtorSignatures) + val sort = floatADT.sorts.head + + val floatCtor : MonoSortedIFunction = floatADT.constructors(0) + val getData : MonoSortedIFunction = floatADT.selectors(0)(0) + + val nan : ITerm = IFunApp(floatADT.constructors(1), Nil) + val plusInf : ITerm = IFunApp(floatADT.constructors(2), Nil) + val negInf : ITerm = IFunApp(floatADT.constructors(3), Nil) + + // val isFloat : Predicate = floatADT.ctorIdPreds(0) + + def isFloat(t: ITerm): IFormula = floatADT.hasCtor(t, 0) + def isNan(t: ITerm): IFormula = floatADT.hasCtor(t, 1) + def isPlusinf(t: ITerm): IFormula = floatADT.hasCtor(t, 2) + def isNeginf(t: ITerm): IFormula = floatADT.hasCtor(t, 3) + + // val isFloat : Predicate = floatADT.hasCtor(I, 0) + // val isNan : Predicate = floatADT.ctorIdPreds(1) + // val isPlusInf : Predicate = floatADT.ctorIdPreds(2) + // val isNegInf : Predicate = floatADT.ctorIdPreds(3) + } + + object Floats { + + import scala.util.control._ + import scala.math._ + def floatToFraction(fp: String): (String, String) = { + val f: Float = fp.toFloat + + if (f.isNaN) { + ("0", "0") + } + else if (f.isInfinity) { + ("0", "0") + } + else { + // + val mantissaBits: Int = java.lang.Float.floatToIntBits(f) << 9 >>> 9 + val mantissa: String = String.format("%23s", Integer.toBinaryString(mantissaBits)).replace(' ', '0') + + val exponentBits: Int = (java.lang.Float.floatToIntBits(f) << 1 >>> 24) + val exponent: String = String.format("%8s", Integer.toBinaryString(exponentBits)).replace(' ', '0') + + val signBit = (java.lang.Float.floatToIntBits(f) >>> 31).toBinaryString + + var bitCount: Int = 23 + + var denominator: BigInt = 1 + var numerator: BigInt = 0 + var loop = new Breaks + loop.breakable { + for (bit <- mantissa.reverse) { + if (bit == '1') { + denominator = BigInt(2).pow(bitCount) + loop.break() + } + bitCount = bitCount - 1 + } + } + + // reset bitCount + bitCount = 1 + numerator = denominator + for (bit <- mantissa) { + if (bit == '1') { + numerator = numerator + denominator / BigInt(2).pow(bitCount) + } + bitCount = bitCount + 1 + } + + bitCount = 0 + var exponentInt: Int = -pow(2, exponent.length() - 1).toInt + 1 + for (bit <- exponent.reverse) { + if (bit == '1') { + exponentInt = exponentInt + pow(2, bitCount).toInt + } + bitCount = bitCount + 1 + } + denominator + if (exponentInt > 0) { + numerator = numerator * BigInt(2).pow(exponentInt) + } + if (exponentInt < 0) { + denominator = denominator * BigInt(2).pow(abs(exponentInt)) + } + // Case for when the float is 0 + if (exponentInt == -pow(2, exponent.length() - 1).toInt + 1 && numerator == 1){ + numerator = 0 + denominator = 1 + } + if (signBit == "1") { + numerator = -numerator + } + (numerator.toString, denominator.toString) + } + } + } + diff --git a/src/tricera/concurrency/ccreader/CCBinaryExpressions.scala b/src/tricera/concurrency/ccreader/CCBinaryExpressions.scala index 4a298e9a..27628ede 100644 --- a/src/tricera/concurrency/ccreader/CCBinaryExpressions.scala +++ b/src/tricera/concurrency/ccreader/CCBinaryExpressions.scala @@ -34,6 +34,10 @@ import tricera.concurrency.CCReader._ import tricera.concurrency.ccreader.CCExceptions.TranslationException import IExpression._ import tricera.Util.getLineString +import ap.theories.rationals.Rationals +import tricera.concurrency.FloatADT +import tricera.concurrency.DoubleADT +import tricera.concurrency.LongDoubleADT object CCBinaryExpressions { object BinaryOperators { @@ -50,14 +54,20 @@ object CCBinaryExpressions { // these should be handled in relevant cases supporting pointer arithmetic, // e.g., addition - protected def getFloatRes: IExpression - protected def getIntRes: IExpression + protected def getLongDoubleRes: IExpression + protected def getDoubleRes: IExpression + protected def getFloatRes: IExpression + protected def getIntRes: IExpression def expr: CCExpr = { try {(lhs.typ, rhs.typ) match { - case (CCFloat, _) => toCCExpr(getFloatRes) - case (_, CCFloat) => toCCExpr(getFloatRes) - case _ => toCCExpr(getIntRes) + case (CCFloat, _) => toCCExpr(getFloatRes) + case (_, CCFloat) => toCCExpr(getFloatRes) + case (CCDouble, _) => toCCExpr(getDoubleRes) + case (_, CCDouble) => toCCExpr(getDoubleRes) + case (CCLongDouble, _) => toCCExpr(getLongDoubleRes) + case (_, CCLongDouble) => toCCExpr(getLongDoubleRes) + case _ => toCCExpr(getIntRes) }} catch { case e : IllegalArgumentException => throw new TranslationException( @@ -87,6 +97,8 @@ object CCBinaryExpressions { ModuloArithmetic.bvor(lhs.typ cast2Unsigned lhs.toTerm, lhs.typ cast2Unsigned rhs.toTerm) override def getFloatRes = ??? + override def getDoubleRes = ??? + override def getLongDoubleRes = ??? } case class BitwiseAnd(_lhs: CCExpr, _rhs: CCExpr) @@ -95,6 +107,8 @@ object CCBinaryExpressions { ModuloArithmetic.bvand(lhs.typ cast2Unsigned lhs.toTerm, lhs.typ cast2Unsigned rhs.toTerm) override def getFloatRes = ??? + override def getDoubleRes = ??? + override def getLongDoubleRes = ??? } case class BitwiseXor(_lhs: CCExpr, _rhs: CCExpr) @@ -103,6 +117,8 @@ object CCBinaryExpressions { ModuloArithmetic.bvxor(lhs.typ cast2Unsigned lhs.toTerm, lhs.typ cast2Unsigned rhs.toTerm) override def getFloatRes = ??? + override def getDoubleRes = ??? + override def getLongDoubleRes = ??? } case class ShiftLeft(_lhs: CCExpr, _rhs: CCExpr) @@ -111,6 +127,8 @@ object CCBinaryExpressions { ModuloArithmetic.bvshl(lhs.typ cast2Unsigned lhs.toTerm, lhs.typ cast2Unsigned rhs.toTerm) override def getFloatRes = ??? + override def getDoubleRes = ??? + override def getLongDoubleRes = ??? } case class ShiftRight(_lhs: CCExpr, _rhs: CCExpr) @@ -119,6 +137,8 @@ object CCBinaryExpressions { ModuloArithmetic.bvashr(lhs.typ cast2Unsigned lhs.toTerm, lhs.typ cast2Unsigned rhs.toTerm) override def getFloatRes = ??? + override def getDoubleRes = ??? + override def getLongDoubleRes = ??? } //////////////////////////////////////////////////////////////////////////// @@ -129,7 +149,13 @@ object CCBinaryExpressions { val (lhsTerm, rhsTerm) = getActualOperandsForBinPred(lhs, rhs) override def getIntRes = lhsTerm === rhsTerm - override def getFloatRes = ??? + override def getFloatRes = { + //IExpression.ite(FloatADT.isFloat(lhsTerm),(FloatADT.getData(lhsTerm) === FloatADT.getData(rhsTerm)), !(FloatADT.getData(lhsTerm) === FloatADT.getData(rhsTerm))) + (FloatADT.getData(lhsTerm) === FloatADT.getData(rhsTerm))// &&& (!FloatADT.isNan(lhsTerm) ||| !FloatADT.isNan(rhsTerm)) //todo: Should it be the same + } + override def getDoubleRes = DoubleADT.getData(lhsTerm) === DoubleADT.getData(rhsTerm) + override def getLongDoubleRes = LongDoubleADT.getData(lhsTerm) === LongDoubleADT.getData(rhsTerm) + } case class Disequality(_lhs: CCExpr, _rhs: CCExpr) @@ -137,7 +163,11 @@ object CCBinaryExpressions { val (lhsTerm, rhsTerm) = getActualOperandsForBinPred(lhs, rhs) override def getIntRes = lhsTerm =/= rhsTerm - override def getFloatRes = ??? + override def getFloatRes = + FloatADT.getData(lhsTerm) =/= FloatADT.getData(rhsTerm) //todo: Should it be the same + override def getDoubleRes = DoubleADT.getData(lhsTerm) =/= DoubleADT.getData(rhsTerm) + override def getLongDoubleRes = LongDoubleADT.getData(lhsTerm) =/= LongDoubleADT.getData(rhsTerm) + } case class Less(_lhs: CCExpr, _rhs: CCExpr) @@ -145,7 +175,9 @@ object CCBinaryExpressions { val (lhsTerm, rhsTerm) = getActualOperandsForBinPred(lhs, rhs) override def getIntRes = lhsTerm < rhsTerm - override def getFloatRes = ??? + override def getFloatRes = Rationals.lt(FloatADT.getData(lhsTerm), FloatADT.getData(rhsTerm)) + override def getDoubleRes = Rationals.lt(DoubleADT.getData(lhsTerm), DoubleADT.getData(rhsTerm)) + override def getLongDoubleRes = Rationals.lt(LongDoubleADT.getData(lhsTerm), LongDoubleADT.getData(rhsTerm)) } case class Greater(_lhs: CCExpr, _rhs: CCExpr) @@ -153,7 +185,11 @@ object CCBinaryExpressions { val (lhsTerm, rhsTerm) = getActualOperandsForBinPred(lhs, rhs) override def getIntRes = lhsTerm > rhsTerm - override def getFloatRes = ??? + override def getFloatRes = Rationals.gt(FloatADT.getData(lhsTerm), FloatADT.getData(rhsTerm)) + + override def getDoubleRes = Rationals.gt(DoubleADT.getData(lhsTerm), DoubleADT.getData(rhsTerm)) + + override def getLongDoubleRes = Rationals.gt(LongDoubleADT.getData(lhsTerm), LongDoubleADT.getData(rhsTerm)) } case class LessEqual(_lhs: CCExpr, _rhs: CCExpr) @@ -161,7 +197,9 @@ object CCBinaryExpressions { val (lhsTerm, rhsTerm) = getActualOperandsForBinPred(lhs, rhs) override def getIntRes = lhsTerm <= rhsTerm - override def getFloatRes = ??? + override def getFloatRes = Rationals.leq(FloatADT.getData(lhsTerm), FloatADT.getData(rhsTerm)) + override def getDoubleRes = Rationals.leq(DoubleADT.getData(lhsTerm), DoubleADT.getData(rhsTerm)) + override def getLongDoubleRes = Rationals.leq(LongDoubleADT.getData(lhsTerm), LongDoubleADT.getData(rhsTerm)) } case class GreaterEqual(_lhs: CCExpr, _rhs: CCExpr) @@ -169,7 +207,9 @@ object CCBinaryExpressions { val (lhsTerm, rhsTerm) = getActualOperandsForBinPred(lhs, rhs) override def getIntRes = lhsTerm >= rhsTerm - override def getFloatRes = ??? + override def getFloatRes = Rationals.geq(FloatADT.getData(lhsTerm), FloatADT.getData(rhsTerm)) + override def getDoubleRes = Rationals.geq(DoubleADT.getData(lhsTerm), DoubleADT.getData(rhsTerm)) + override def getLongDoubleRes = Rationals.geq(LongDoubleADT.getData(lhsTerm), LongDoubleADT.getData(rhsTerm)) } //////////////////////////////////////////////////////////////////////////// @@ -184,7 +224,45 @@ object CCBinaryExpressions { case _ => lhs.toTerm + rhs.toTerm } - override def getFloatRes = ??? + override def getFloatRes = (lhs.typ, rhs.typ) match { + case(CCFloat, CCFloat) => + FloatADT.floatCtor(Rationals.plus( + FloatADT.getData(lhs.toTerm), FloatADT.getData(rhs.toTerm))) + + /* Semantics for addition when using the ADT + IExpression.ite(FloatADT.isFloat(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm), + FloatADT.floatCtor(Rationals.plus( + FloatADT.getData(lhs.toTerm), FloatADT.getData(rhs.toTerm))), + + IExpression.ite((FloatADT.isPlusinf(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm)) + ||| (FloatADT.isFloat(lhs.toTerm) &&& FloatADT.isPlusinf(rhs.toTerm)) + ||| (FloatADT.isPlusinf(lhs.toTerm) &&& FloatADT.isPlusinf(rhs.toTerm)), + FloatADT.plusInf, + + IExpression.ite((FloatADT.isNeginf(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm)) + ||| (FloatADT.isFloat(lhs.toTerm) &&& FloatADT.isNeginf(rhs.toTerm)) + ||| (FloatADT.isNeginf(lhs.toTerm) &&& FloatADT.isNeginf(rhs.toTerm)), + FloatADT.negInf, FloatADT.nan))) + */ + + case _ => + throw new Exception("Unmatched types") + } + override def getDoubleRes = (lhs.typ, rhs.typ) match { + case (CCDouble, CCDouble) => + DoubleADT.doubleCtor(Rationals.plus( + DoubleADT.getData(lhs.toTerm), DoubleADT.getData(rhs.toTerm))) + case _ => + throw new Exception("Unmatched types") + } + + override def getLongDoubleRes = (lhs.typ, rhs.typ) match { + case (CCLongDouble, CCLongDouble) => + LongDoubleADT.longDoubleCtor(Rationals.plus( + LongDoubleADT.getData(lhs.toTerm), LongDoubleADT.getData(rhs.toTerm))) + case _ => + throw new Exception("Unmatched types") + } } case class Minus(_lhs: CCExpr, _rhs: CCExpr) @@ -193,25 +271,138 @@ object CCBinaryExpressions { throwErrorIfPointerArithmetic(lhs, rhs) lhs.toTerm - rhs.toTerm } - override def getFloatRes = ??? + override def getFloatRes = (lhs.typ, rhs.typ) match { + case (CCFloat, CCFloat) => + FloatADT.floatCtor(Rationals.minus( + FloatADT.getData(lhs.toTerm), FloatADT.getData(rhs.toTerm))) + + /* Semantics for subtraction using the ADT + IExpression.ite(FloatADT.isFloat(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm), + FloatADT.floatCtor(Rationals.minus( + FloatADT.getData(lhs.toTerm), FloatADT.getData(rhs.toTerm))), + + IExpression.ite((FloatADT.isPlusinf(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm)) + ||| (FloatADT.isFloat(lhs.toTerm) &&& FloatADT.isNeginf(rhs.toTerm)), + FloatADT.plusInf, + + IExpression.ite((FloatADT.isNeginf(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm)) + ||| (FloatADT.isFloat(lhs.toTerm) &&& FloatADT.isPlusinf(rhs.toTerm)) + ||| (FloatADT.isNeginf(lhs.toTerm) &&& FloatADT.isPlusinf(rhs.toTerm)), + FloatADT.negInf, FloatADT.nan))) + */ + + case _ => + throw new Exception("Unmatched types") + } - case class Times(_lhs: CCExpr, _rhs: CCExpr) - extends BinaryOperation(_lhs, _rhs) { - override def getIntRes = { - throwErrorIfPointerArithmetic(lhs, rhs) - ap.theories.nia.GroebnerMultiplication.mult(lhs.toTerm, rhs.toTerm) - } - override def getFloatRes = ??? + override def getDoubleRes = (lhs.typ, rhs.typ) match { + case (CCDouble, CCDouble) => + DoubleADT.doubleCtor(Rationals.minus( + DoubleADT.getData(lhs.toTerm), DoubleADT.getData(rhs.toTerm))) + case _ => + throw new Exception("Unmatched types") } - case class Div(_lhs: CCExpr, _rhs: CCExpr) - extends BinaryOperation(_lhs, _rhs) { - override def getIntRes = { - throwErrorIfPointerArithmetic(lhs, rhs) - ap.theories.nia.GroebnerMultiplication.tDiv(lhs.toTerm, rhs.toTerm) + override def getLongDoubleRes = (lhs.typ, rhs.typ) match { + case (CCLongDouble, CCLongDouble) => + LongDoubleADT.longDoubleCtor(Rationals.minus( + LongDoubleADT.getData(lhs.toTerm), LongDoubleADT.getData(rhs.toTerm))) + case _ => + throw new Exception("Unmatched types") + } + } + + case class Times(_lhs: CCExpr, _rhs: CCExpr) + extends BinaryOperation(_lhs, _rhs) { + override def getIntRes = { + throwErrorIfPointerArithmetic(lhs, rhs) + ap.theories.nia.GroebnerMultiplication.mult(lhs.toTerm, rhs.toTerm) + } + override def getFloatRes = (lhs.typ, rhs.typ) match { + case (CCFloat, CCFloat) => + FloatADT.floatCtor(Rationals.mul( + FloatADT.getData(lhs.toTerm), FloatADT.getData(rhs.toTerm))) + + /* Semantics for multiplication using the ADT + IExpression.ite(FloatADT.isFloat(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm), + FloatADT.floatCtor(Rationals.mul( + FloatADT.getData(lhs.toTerm), FloatADT.getData(rhs.toTerm))), + + IExpression.ite((FloatADT.isPlusinf(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm)) + ||| (FloatADT.isFloat(lhs.toTerm) &&& FloatADT.isPlusinf(rhs.toTerm)) + ||| (FloatADT.isPlusinf(lhs.toTerm) &&& FloatADT.isPlusinf(rhs.toTerm)) + ||| (FloatADT.isNeginf(lhs.toTerm) &&& FloatADT.isNeginf(rhs.toTerm)), + FloatADT.plusInf, + + IExpression.ite((FloatADT.isNeginf(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm)) + ||| (FloatADT.isFloat(lhs.toTerm) &&& FloatADT.isNeginf(rhs.toTerm)) + ||| (FloatADT.isNeginf(lhs.toTerm) &&& FloatADT.isPlusinf(rhs.toTerm)) + ||| (FloatADT.isPlusinf(lhs.toTerm) &&& FloatADT.isNeginf(rhs.toTerm)), + FloatADT.negInf, FloatADT.nan))) + */ + + case _ => + throw new Exception("Unmatched types") + } + override def getDoubleRes = (lhs.typ, rhs.typ) match { + case (CCDouble, CCDouble) => + DoubleADT.doubleCtor(Rationals.mul( + DoubleADT.getData(lhs.toTerm), DoubleADT.getData(rhs.toTerm))) + case _ => + throw new Exception("Unmatched types") + } + + override def getLongDoubleRes = (lhs.typ, rhs.typ) match { + case (CCLongDouble, CCLongDouble) => + LongDoubleADT.longDoubleCtor(Rationals.mul( + LongDoubleADT.getData(lhs.toTerm), LongDoubleADT.getData(rhs.toTerm))) + case _ => + throw new Exception("Unmatched types") + } + } + + case class Div(_lhs: CCExpr, _rhs: CCExpr) + extends BinaryOperation(_lhs, _rhs) { + override def getIntRes = { + throwErrorIfPointerArithmetic(lhs, rhs) + ap.theories.nia.GroebnerMultiplication.tDiv(lhs.toTerm, rhs.toTerm) + } + override def getFloatRes = (lhs.typ, rhs.typ) match { + case (CCFloat, CCFloat) => + FloatADT.floatCtor(Rationals.div( + FloatADT.getData(lhs.toTerm), FloatADT.getData(rhs.toTerm))) + + /* Semantics for division using the ADT + IExpression.ite(FloatADT.isFloat(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm), + FloatADT.floatCtor(Rationals.div( + FloatADT.getData(lhs.toTerm), FloatADT.getData(rhs.toTerm))), + + IExpression.ite((FloatADT.isPlusinf(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm)), + FloatADT.plusInf, + + IExpression.ite((FloatADT.isNeginf(lhs.toTerm) &&& FloatADT.isFloat(rhs.toTerm)), + FloatADT.negInf, FloatADT.nan))) + */ + case _ => + throw new Exception("Unmatched types") + } + + override def getDoubleRes = (lhs.typ, rhs.typ) match { + case (CCDouble, CCDouble) => + DoubleADT.doubleCtor(Rationals.div( + DoubleADT.getData(lhs.toTerm), DoubleADT.getData(rhs.toTerm))) + case _ => + throw new Exception("Unmatched types") + } + + override def getLongDoubleRes = (lhs.typ, rhs.typ) match { + case (CCLongDouble, CCLongDouble) => + LongDoubleADT.longDoubleCtor(Rationals.div( + LongDoubleADT.getData(lhs.toTerm), LongDoubleADT.getData(rhs.toTerm))) + case _ => + throw new Exception("Unmatched types") } - override def getFloatRes = ??? } case class Mod(_lhs: CCExpr, _rhs: CCExpr) @@ -221,6 +412,8 @@ object CCBinaryExpressions { ap.theories.nia.GroebnerMultiplication.tMod(lhs.toTerm, rhs.toTerm) } override def getFloatRes = ??? + override def getDoubleRes = ??? + override def getLongDoubleRes = ??? } private def throwErrorIfPointerArithmetic(lhs: CCExpr, diff --git a/src/tricera/concurrency/ccreader/CCType.scala b/src/tricera/concurrency/ccreader/CCType.scala index 7b3a0743..88d9b0f3 100644 --- a/src/tricera/concurrency/ccreader/CCType.scala +++ b/src/tricera/concurrency/ccreader/CCType.scala @@ -31,8 +31,11 @@ package tricera.concurrency.ccreader import ap.basetypes.IdealInt import ap.parser.{IFormula, IFunction, IIntLit, ITerm} -import ap.theories.Heap +import ap.theories.{Heap, ADT} import tricera.concurrency.CCReader._ +import tricera.concurrency.FloatADT +import tricera.concurrency.DoubleADT +import tricera.concurrency.LongDoubleADT import ap.parser.IExpression.{Sort, _} import ap.theories.bitvectors.ModuloArithmetic._ import ap.types.{MonoSortedIFunction, SortedConstantTerm} @@ -61,6 +64,8 @@ abstract sealed class CCType { case CCStruct(ctor, _) => ctor.resSort case CCStructField(n, s) => s(n).ctor.resSort case CCIntEnum(_, _) => Sort.Integer + case CCFloat => FloatADT.sort + case CCDouble => DoubleADT.sort case _ => Sort.Integer } case ArithmeticMode.ILP32 => @@ -73,6 +78,9 @@ abstract sealed class CCType { case CCULong => UnsignedBVSort(32) case CCLongLong => SignedBVSort(64) case CCULongLong => UnsignedBVSort(64) + case CCFloat => FloatADT.sort + case CCDouble => DoubleADT.sort + case CCLongDouble => LongDoubleADT.sort case CCDuration => Sort.Nat case CCHeap(heap) => heap.HeapSort case CCStackPointer(_, _, _) => Sort.Integer @@ -94,6 +102,9 @@ abstract sealed class CCType { case CCULong => UnsignedBVSort(64) case CCLongLong => SignedBVSort(64) case CCULongLong => UnsignedBVSort(64) + case CCFloat => FloatADT.sort + case CCDouble => DoubleADT.sort + case CCLongDouble => LongDoubleADT.sort case CCDuration => Sort.Nat case CCHeap(heap) => heap.HeapSort case CCStackPointer(_, _, _) => Sort.Integer @@ -115,6 +126,9 @@ abstract sealed class CCType { case CCULong => UnsignedBVSort(32) case CCLongLong => SignedBVSort(64) case CCULongLong => UnsignedBVSort(64) + case CCFloat => FloatADT.sort + case CCDouble => DoubleADT.sort + case CCLongDouble => LongDoubleADT.sort case CCDuration => Sort.Nat case CCHeap(heap) => heap.HeapSort case CCStackPointer(_, _, _) => Sort.Integer @@ -285,6 +299,14 @@ case object CCFloat extends CCType { override def toString : String = "float" def shortName = "float" } +case object CCDouble extends CCType { + override def toString : String = "double" + def shortName = "double" +} +case object CCLongDouble extends CCType { + override def toString : String = "long double" + def shortName = "long double" +} case class CCHeap(heap : Heap) extends CCType { override def toString : String = heap.toString diff --git a/unit-tests/tricera/concurrency/CCReaderCollectVarDecls.scala b/unit-tests/tricera/concurrency/CCReaderCollectVarDecls.scala index ce05a6f7..4ca753f5 100644 --- a/unit-tests/tricera/concurrency/CCReaderCollectVarDecls.scala +++ b/unit-tests/tricera/concurrency/CCReaderCollectVarDecls.scala @@ -34,6 +34,15 @@ import CCReader._ import ccreader._ import tricera.params.TriCeraParameters +import scala.util.control._ +import scala.math.BigInt +import scala.math._ +import java.math.BigInteger +import org.scalatest._ +import tricera.concurrency.ccreader._ +import scala.math.BigDecimal.int2bigDecimal + + class CCReaderCollectVarDecls extends AnyFlatSpec { //////////////////////////////////////////////////////////////////////////////// // Configuration diff --git a/unit-tests/tricera/concurrency/float2fractionTest.scala b/unit-tests/tricera/concurrency/float2fractionTest.scala new file mode 100644 index 00000000..d1f94f06 --- /dev/null +++ b/unit-tests/tricera/concurrency/float2fractionTest.scala @@ -0,0 +1,91 @@ +/** + * Copyright (c) 2022-2023 Zafer Esen, Philipp Ruemmer. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package tricera.concurrency + +import org.scalatest.flatspec.AnyFlatSpec +import tricera.concurrency.Floats.floatToFraction +class FractionTest extends AnyFlatSpec { + // create a dummy file to create an instance of CCReader + + //////////////////////////////////////////////////////////////////////////////// + // Tests + var foo: (String, String) = floatToFraction("2.0f") + assert(foo == ("2", "1")) + + foo = floatToFraction("-2.0f") + assert(foo == ("-2", "1")) + + foo = floatToFraction("8.0f") + assert(foo == ("8", "1")) + + foo = floatToFraction("-8.0f") + assert(foo == ("-8", "1")) + + foo = floatToFraction("3.14f") + assert(foo == ("26340230", "8388608")) + + foo = floatToFraction("-3.14f") + assert(foo == ("-26340230", "8388608")) + + foo = floatToFraction("2.64f") + assert(foo == ("22145926", "8388608")) + + foo = floatToFraction("-2.64f") + assert(foo == ("-22145926", "8388608")) + + foo = floatToFraction("0.125f") + assert(foo == ("1", "8")) + + foo = floatToFraction("-0.125f") + assert(foo == ("-1", "8")) + + foo = floatToFraction("0.0032f") + assert(foo == ("13743895", "4294967296")) + + foo = floatToFraction("-0.0032f") + assert(foo == ("-13743895", "4294967296")) + + foo = floatToFraction("0.69f") + assert(foo == ("11576279", "16777216")) + + foo = floatToFraction("-0.69f") + assert(foo == ("-11576279", "16777216")) + + foo = floatToFraction("2.35098856151e-38") + assert(foo == ("16777215" , "713623846352979940529142984724747568191373312")) + + foo = floatToFraction("-2.35098856151e-38") + assert(foo == ("-16777215", "713623846352979940529142984724747568191373312")) + + foo = floatToFraction("0.0f") + assert(foo == ("0", "1")) + + println("ALL TESTS PASSED") +}