From 43b80b13bd24bb789849aac3385df6ac4a8233be Mon Sep 17 00:00:00 2001 From: boehmes Date: Thu, 27 Sep 2012 17:13:45 +0200 Subject: Boogie: added type 'real' with overloaded arithmetic operations plus real division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested) --- Source/Core/Scanner.cs | 355 +++++++++++++++++++++++++++---------------------- 1 file changed, 195 insertions(+), 160 deletions(-) (limited to 'Source/Core/Scanner.cs') diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index b9f4ec42..60c15b41 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner { const char EOL = '\n'; const int eofSym = 0; /* pdt */ - const int maxT = 88; - const int noSym = 88; + const int maxT = 92; + const int noSym = 92; [ContractInvariantMethod] @@ -256,40 +256,41 @@ public class Scanner { for (int i = 65; i <= 90; ++i) start[i] = 2; for (int i = 94; i <= 122; ++i) start[i] = 2; for (int i = 126; i <= 126; ++i) start[i] = 2; - for (int i = 48; i <= 57; ++i) start[i] = 9; + for (int i = 48; i <= 57; ++i) start[i] = 16; for (int i = 34; i <= 34; ++i) start[i] = 6; start[92] = 1; - start[59] = 12; - start[40] = 13; - start[41] = 14; - start[58] = 47; - start[44] = 15; - start[91] = 16; - start[93] = 17; - start[60] = 48; - start[62] = 49; - start[123] = 18; - start[125] = 50; - start[61] = 51; - start[42] = 19; - start[8660] = 22; - start[8658] = 24; - start[8656] = 25; - start[38] = 26; - start[8743] = 28; - start[124] = 52; - start[8744] = 30; - start[33] = 53; - start[8800] = 34; - start[8804] = 35; - start[8805] = 36; - start[43] = 54; - start[45] = 38; - start[172] = 39; - start[8704] = 42; - start[8707] = 43; - start[955] = 44; - start[8226] = 46; + start[59] = 19; + start[40] = 20; + start[41] = 21; + start[58] = 55; + start[44] = 22; + start[91] = 23; + start[93] = 24; + start[60] = 56; + start[62] = 57; + start[123] = 25; + start[125] = 58; + start[61] = 59; + start[42] = 60; + start[8660] = 28; + start[8658] = 30; + start[8656] = 31; + start[38] = 32; + start[8743] = 34; + start[124] = 61; + start[8744] = 36; + start[33] = 62; + start[8800] = 40; + start[8804] = 41; + start[8805] = 42; + start[43] = 63; + start[45] = 44; + start[47] = 45; + start[172] = 47; + start[8704] = 50; + start[8707] = 51; + start[955] = 52; + start[8226] = 54; start[Buffer.EOF] = -1; } @@ -487,44 +488,45 @@ public class Scanner { void CheckLiteral() { switch (t.val) { - case "var": t.kind = 6; break; - case "where": t.kind = 12; break; - case "int": t.kind = 13; break; - case "bool": t.kind = 14; break; - case "const": t.kind = 19; break; - case "unique": t.kind = 20; break; - case "extends": t.kind = 21; break; - case "complete": t.kind = 22; break; - case "function": t.kind = 23; break; - case "returns": t.kind = 24; break; - case "axiom": t.kind = 27; break; - case "type": t.kind = 28; break; - case "procedure": t.kind = 30; break; - case "implementation": t.kind = 31; break; - case "modifies": t.kind = 32; break; - case "free": t.kind = 33; break; - case "requires": t.kind = 34; break; - case "ensures": t.kind = 35; break; - case "goto": t.kind = 36; break; - case "return": t.kind = 37; break; - case "if": t.kind = 38; break; - case "else": t.kind = 39; break; - case "while": t.kind = 40; break; - case "invariant": t.kind = 41; break; - case "break": t.kind = 43; break; - case "assert": t.kind = 44; break; - case "assume": t.kind = 45; break; - case "havoc": t.kind = 46; break; - case "call": t.kind = 48; break; - case "forall": t.kind = 49; break; - case "div": t.kind = 71; break; - case "mod": t.kind = 72; break; - case "false": t.kind = 75; break; - case "true": t.kind = 76; break; - case "old": t.kind = 77; break; - case "then": t.kind = 80; break; - case "exists": t.kind = 82; break; - case "lambda": t.kind = 84; break; + case "var": t.kind = 7; break; + case "where": t.kind = 13; break; + case "int": t.kind = 14; break; + case "real": t.kind = 15; break; + case "bool": t.kind = 16; break; + case "const": t.kind = 21; break; + case "unique": t.kind = 22; break; + case "extends": t.kind = 23; break; + case "complete": t.kind = 24; break; + case "function": t.kind = 25; break; + case "returns": t.kind = 26; break; + case "axiom": t.kind = 29; break; + case "type": t.kind = 30; break; + case "procedure": t.kind = 32; break; + case "implementation": t.kind = 33; break; + case "modifies": t.kind = 34; break; + case "free": t.kind = 35; break; + case "requires": t.kind = 36; break; + case "ensures": t.kind = 37; break; + case "goto": t.kind = 38; break; + case "return": t.kind = 39; break; + case "if": t.kind = 40; break; + case "else": t.kind = 41; break; + case "while": t.kind = 42; break; + case "invariant": t.kind = 43; break; + case "break": t.kind = 45; break; + case "assert": t.kind = 46; break; + case "assume": t.kind = 47; break; + case "havoc": t.kind = 48; break; + case "call": t.kind = 50; break; + case "forall": t.kind = 51; break; + case "div": t.kind = 73; break; + case "mod": t.kind = 74; break; + case "false": t.kind = 79; break; + case "true": t.kind = 80; break; + case "old": t.kind = 81; break; + case "then": t.kind = 84; break; + case "exists": t.kind = 86; break; + case "lambda": t.kind = 88; break; default: break; } } @@ -577,148 +579,181 @@ public class Scanner { case 6: if (ch == '"') {AddCh(); goto case 7;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 10;} + else if (ch == 92) {AddCh(); goto case 17;} else {goto case 0;} case 7: {t.kind = 4; break;} case 8: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} + else if (ch == '-') {AddCh(); goto case 9;} + else {goto case 0;} + case 9: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} + else {goto case 0;} + case 10: recEnd = pos; recKind = 5; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 8;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} else {t.kind = 5; break;} - case 9: + case 11: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} + else {goto case 0;} + case 12: + recEnd = pos; recKind = 6; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} + else if (ch == 'e') {AddCh(); goto case 13;} + else {t.kind = 6; break;} + case 13: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} + else if (ch == '-') {AddCh(); goto case 14;} + else {goto case 0;} + case 14: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} + else {goto case 0;} + case 15: + recEnd = pos; recKind = 6; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} + else {t.kind = 6; break;} + case 16: recEnd = pos; recKind = 3; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;} else if (ch == 'b') {AddCh(); goto case 3;} - else if (ch == '.') {AddCh(); goto case 8;} + else if (ch == 'e') {AddCh(); goto case 8;} + else if (ch == '.') {AddCh(); goto case 11;} else {t.kind = 3; break;} - case 10: - if (ch == '"') {AddCh(); goto case 11;} + case 17: + if (ch == '"') {AddCh(); goto case 18;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 10;} + else if (ch == 92) {AddCh(); goto case 17;} else {goto case 0;} - case 11: + case 18: recEnd = pos; recKind = 4; if (ch == '"') {AddCh(); goto case 7;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 10;} + else if (ch == 92) {AddCh(); goto case 17;} else {t.kind = 4; break;} - case 12: - {t.kind = 7; break;} - case 13: - {t.kind = 8; break;} - case 14: - {t.kind = 9; break;} - case 15: - {t.kind = 11; break;} - case 16: - {t.kind = 15; break;} - case 17: - {t.kind = 16; break;} - case 18: - {t.kind = 25; break;} case 19: - {t.kind = 42; break;} + {t.kind = 8; break;} case 20: - {t.kind = 47; break;} + {t.kind = 9; break;} case 21: - {t.kind = 50; break;} + {t.kind = 10; break;} case 22: - {t.kind = 51; break;} + {t.kind = 12; break;} case 23: - {t.kind = 52; break;} + {t.kind = 17; break;} case 24: - {t.kind = 53; break;} + {t.kind = 18; break;} case 25: - {t.kind = 55; break;} + {t.kind = 27; break;} case 26: - if (ch == '&') {AddCh(); goto case 27;} - else {goto case 0;} + {t.kind = 49; break;} case 27: - {t.kind = 56; break;} + {t.kind = 52; break;} case 28: - {t.kind = 57; break;} + {t.kind = 53; break;} case 29: - {t.kind = 58; break;} + {t.kind = 54; break;} case 30: - {t.kind = 59; break;} + {t.kind = 55; break;} case 31: - {t.kind = 62; break;} + {t.kind = 57; break;} case 32: - {t.kind = 63; break;} + if (ch == '&') {AddCh(); goto case 33;} + else {goto case 0;} case 33: - {t.kind = 64; break;} + {t.kind = 58; break;} case 34: - {t.kind = 65; break;} + {t.kind = 59; break;} case 35: - {t.kind = 66; break;} + {t.kind = 60; break;} case 36: - {t.kind = 67; break;} + {t.kind = 61; break;} case 37: - {t.kind = 68; break;} + {t.kind = 64; break;} case 38: - {t.kind = 70; break;} + {t.kind = 65; break;} case 39: - {t.kind = 74; break;} + {t.kind = 66; break;} case 40: - {t.kind = 78; break;} + {t.kind = 67; break;} case 41: - {t.kind = 79; break;} + {t.kind = 68; break;} case 42: - {t.kind = 81; break;} + {t.kind = 69; break;} case 43: - {t.kind = 83; break;} + {t.kind = 70; break;} case 44: - {t.kind = 85; break;} + {t.kind = 72; break;} case 45: - {t.kind = 86; break;} + {t.kind = 75; break;} case 46: - {t.kind = 87; break;} + {t.kind = 76; break;} case 47: - recEnd = pos; recKind = 10; - if (ch == '=') {AddCh(); goto case 20;} - else if (ch == ':') {AddCh(); goto case 45;} - else {t.kind = 10; break;} + {t.kind = 78; break;} case 48: - recEnd = pos; recKind = 17; - if (ch == '=') {AddCh(); goto case 55;} - else if (ch == ':') {AddCh(); goto case 33;} - else {t.kind = 17; break;} + {t.kind = 82; break;} case 49: - recEnd = pos; recKind = 18; - if (ch == '=') {AddCh(); goto case 31;} - else {t.kind = 18; break;} + {t.kind = 83; break;} case 50: - recEnd = pos; recKind = 26; - if (ch == '|') {AddCh(); goto case 41;} - else {t.kind = 26; break;} + {t.kind = 85; break;} case 51: - recEnd = pos; recKind = 29; - if (ch == '=') {AddCh(); goto case 56;} - else {t.kind = 29; break;} + {t.kind = 87; break;} case 52: - if (ch == '|') {AddCh(); goto case 29;} - else if (ch == '{') {AddCh(); goto case 40;} - else {goto case 0;} + {t.kind = 89; break;} case 53: - recEnd = pos; recKind = 73; - if (ch == '=') {AddCh(); goto case 32;} - else {t.kind = 73; break;} + {t.kind = 90; break;} case 54: - recEnd = pos; recKind = 69; - if (ch == '+') {AddCh(); goto case 37;} - else {t.kind = 69; break;} + {t.kind = 91; break;} case 55: - recEnd = pos; recKind = 61; - if (ch == '=') {AddCh(); goto case 57;} - else {t.kind = 61; break;} + recEnd = pos; recKind = 11; + if (ch == '=') {AddCh(); goto case 26;} + else if (ch == ':') {AddCh(); goto case 53;} + else {t.kind = 11; break;} case 56: - recEnd = pos; recKind = 60; - if (ch == '>') {AddCh(); goto case 23;} - else {t.kind = 60; break;} + recEnd = pos; recKind = 19; + if (ch == '=') {AddCh(); goto case 64;} + else if (ch == ':') {AddCh(); goto case 39;} + else {t.kind = 19; break;} case 57: - recEnd = pos; recKind = 54; - if (ch == '>') {AddCh(); goto case 21;} - else {t.kind = 54; break;} + recEnd = pos; recKind = 20; + if (ch == '=') {AddCh(); goto case 37;} + else {t.kind = 20; break;} + case 58: + recEnd = pos; recKind = 28; + if (ch == '|') {AddCh(); goto case 49;} + else {t.kind = 28; break;} + case 59: + recEnd = pos; recKind = 31; + if (ch == '=') {AddCh(); goto case 65;} + else {t.kind = 31; break;} + case 60: + recEnd = pos; recKind = 44; + if (ch == '*') {AddCh(); goto case 46;} + else {t.kind = 44; break;} + case 61: + if (ch == '|') {AddCh(); goto case 35;} + else if (ch == '{') {AddCh(); goto case 48;} + else {goto case 0;} + case 62: + recEnd = pos; recKind = 77; + if (ch == '=') {AddCh(); goto case 38;} + else {t.kind = 77; break;} + case 63: + recEnd = pos; recKind = 71; + if (ch == '+') {AddCh(); goto case 43;} + else {t.kind = 71; break;} + case 64: + recEnd = pos; recKind = 63; + if (ch == '=') {AddCh(); goto case 66;} + else {t.kind = 63; break;} + case 65: + recEnd = pos; recKind = 62; + if (ch == '>') {AddCh(); goto case 29;} + else {t.kind = 62; break;} + case 66: + recEnd = pos; recKind = 56; + if (ch == '>') {AddCh(); goto case 27;} + else {t.kind = 56; break;} } t.val = new String(tval, 0, tlen); -- cgit v1.2.3