C Integer Programs - Revision history

Cryingshadow: parse expressions from left to right when there are no parantheses

2015-07-06T17:36:50Z

parse expressions from left to right when there are no parantheses

Cryingshadow: allow negative mutliplicative expressions

2015-07-06T16:51:24Z

allow negative mutliplicative expressions

Cryingshadow: allow chaining of expressions without parantheses (e.g., 1 + 1 + 1 instead of 1 + (1 + 1))

2015-07-06T16:21:58Z

allow chaining of expressions without parantheses (e.g., 1 + 1 + 1 instead of 1 + (1 + 1))

Cryingshadow: also allow comments

2015-07-06T09:44:55Z

also allow comments

Cryingshadow: provide ANTLR grammar to fix issues with old grammar and make it easier for other participants to build a parser

2015-07-03T15:29:17Z

provide ANTLR grammar to fix issues with old grammar and make it easier for other participants to build a parser

Show changes

Cryingshadow at 13:11, 22 June 2015

2015-06-22T13:11:23Z

Cryingshadow: fix format and grammar

2015-06-22T13:10:51Z

fix format and grammar

Cryingshadow at 13:08, 22 June 2015

2015-06-22T13:08:59Z

Cryingshadow at 13:05, 22 June 2015

2015-06-22T13:05:20Z

Cryingshadow: Add new page for integer C category

2015-06-22T12:57:42Z

Add new page for integer C category

New page

[[Category:Categories]]

Non-terminals:
P: Program
PRE: Start of the program, including the declaration of an external
function for non-deterministic values
POST: The end of the program
D: Variable declaration
V: Variable name
INS: Instruction
A: Assignment
L: Loop
C: Condition
NE: Numerical expression
N: Number
BE: Boolean expression
NO: Numerical operator
BO: Boolean operator
BC: Boolean connective
W: Whitespace

Grammar:
P = PRE D* W? I* POST
PRE = W?
"extern"
W
"int"
W
"__VERIFIER_nondet_int"
W?
"("
W?
"void"
W?
")"
W?
";"
W?
"int"
W
"main"
W?
"("
W?
")"
W?
"{"
W?
POST = W? "return" W "0" W? ";" W? "}" W?
D = "int" W V W? ";"
V = [a-z,A-Z] [a-z,A-Z,0-9]*
I = (A | L | C) W? ";"
A = V W? "=" W? NE
L = "while" W? "(" W? BE W? ")" W? "{" W? I* W? "}"
C = "if" W? "(" W? BE W? ")" W? "{" W? I* W? "}" (W? "else" W? "{" W? I* W? "}")?
NE = N | V | NE W? NO W? NE | "(" W? NE W? ")" | "-" W? NE
N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"
BE = "true" | "false" | NE W? BO W? NE | BE W? BC W? BE | "!" W? BE | "(" W? BE W? ")"
NO = "+" | "-" | "*"
BO = "<" | ">" | "<=" | ">=" | "==" | "!="
BC = "&&" | "||" | "==" | "!="
W = (" " | "\n") (" " | "\n")*

Calls to __VERIFIER_nondet_int() yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics are used.

@@ Line 50: / Line 50: @@
   num_atom : ZERO | POS | nondet | V | OPENP W* bool_expr W* CLOSEP;
-  mult_expr : num_atom (W* MULT W* mult_expr)?;
+  mult_expr : num_atom (W* MULT W* num_atom)*;
-  num_expr : mult_expr (W* (PLUS | MINUS) W* num_expr)? | MINUS W* mult_expr;
+  num_expr : mult_expr (W* (PLUS | MINUS) W* mult_expr)* | MINUS W* mult_expr (W* (PLUS | MINUS) W* mult_expr)*;
   bool_atom : TRUE | FALSE | num_expr (W* BO W* num_expr)?;
-  and_expr : bool_atom (W* AND W* and_expr)?;
+  and_expr : bool_atom (W* AND W* bool_atom)*;
-  bool_expr : and_expr (W* OR W* bool_expr)? | NOT W* bool_atom;
+  bool_expr : and_expr (W* OR W* and_expr)* | NOT W* bool_atom;
   loop : WHILE W* OPENP W* bool_expr W* CLOSEP W* OPENC W* (instructions W*)? CLOSEC;

@@ Line 52: / Line 52: @@
   mult_expr : num_atom (W* MULT W* mult_expr)?;
-  num_expr : mult_expr (W* (PLUS | MINUS) W* num_expr)? | MINUS W* num_atom;
+  num_expr : mult_expr (W* (PLUS | MINUS) W* num_expr)? | MINUS W* mult_expr;
   bool_atom : TRUE | FALSE | num_expr (W* BO W* num_expr)?;

@@ Line 50: / Line 50: @@
   num_atom : ZERO | POS | nondet | V | OPENP W* bool_expr W* CLOSEP;
-  mult_expr : num_atom (W* MULT W* num_atom)?;
+  mult_expr : num_atom (W* MULT W* mult_expr)?;
   num_expr : mult_expr (W* (PLUS | MINUS) W* num_expr)? | MINUS W* num_atom;
@@ Line 56: / Line 56: @@
   bool_atom : TRUE | FALSE | num_expr (W* BO W* num_expr)?;
-  and_expr : bool_atom (W* AND W* bool_atom)?;
+  and_expr : bool_atom (W* AND W* and_expr)?;
-  bool_expr : and_expr (W* OR W* and_expr)? | NOT W* bool_atom;
+  bool_expr : and_expr (W* OR W* bool_expr)? | NOT W* bool_atom;
   loop : WHILE W* OPENP W* bool_expr W* CLOSEP W* OPENC W* (instructions W*)? CLOSEC;

@@ Line 136: / Line 136: @@
   fragment UP: 'A'..'Z';
   W : ' ' | '\n' | '\r' | '\t';
 Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.
 Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics is used. So while the grammar above allows, e.g., nesting of boolean expressions inside arithmetic expressions (to make the automated generation of a parser easier), such programs have no defined semantics and are excluded from benchmarks for the competition.

← Older revision		Revision as of 13:11, 22 June 2015
Line 86:		Line 86:
	Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.		Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

−	Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics ~~are~~ used.	+	Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics is used.

@@ Line 43: / Line 43: @@
 The grammar is then (EBNF-like):
-  P = PRE D* W? I* POST
+  P = PRE D* W? INS* POST
   PRE = W?
         "extern"
@@ Line 72: / Line 72: @@
   D = "int" W V W? ";"
   V = [a-z,A-Z] [a-z,A-Z,0-9]*
-  I = (A | L | C) W? ";"
+  INS = (A | L | C) W? ";"
   A = V W? "=" W? NE
-  L = "while" W? "(" W? BE W? ")" W? "{" W? I* W? "}"
+  L = "while" W? "(" W? BE W? ")" W? "{" W? INS* W? "}"
-  C = "if" W? "(" W? BE W? ")" W? "{" W? I* W? "}" (W? "else" W? "{" W? I* W? "}")?
+  C = "if" W? "(" W? BE W? ")" W? "{" W? INS* W? "}" (W? "else" W? "{" W? INS* W? "}")?
   NE = N | V | NE W? NO W? NE | "(" W? NE W? ")" | "-" W? NE
   N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"

@@ Line 9: / Line 9: @@
 The syntax of termination problems in this category is defined using the following non-terminals:
-P:: Program
+;P
-PRE:: Start of the program, including the declaration of an external function for non-deterministic values
+: Program
-POST:: The end of the program
+;PRE
-D:: Variable declaration
+: Start of the program, including the declaration of an external function for non-deterministic values
-V:: Variable name
+;POST
-INS:: Instruction
+: The end of the program
-A:: Assignment
+;D
-L:: Loop
+: Variable declaration
-C:: Condition
+;V
-NE:: Numerical expression
+: Variable name
-N:: Number
+;INS
-BE:: Boolean expression
+: Instruction
-NO:: Numerical operator
+;A
-BO:: Boolean operator
+: Assignment
-BC:: Boolean connective
+;L
-W:: Whitespace
+: Loop
 The grammar is then (EBNF-like):
-{{{
+ P = PRE D* W? I* POST
-P = PRE D* W? I* POST
+ PRE = W?
-PRE = W?
+       "extern"
-      "extern"
+       "int"
-      "int"
+       "__VERIFIER_nondet_int"
-      "__VERIFIER_nondet_int"
+       W?
-      W?
+       "("
-      "("
+       W?
-      W?
+       "void"
-      "void"
+       W?
-      W?
+       ")"
-      ")"
+       W?
-      W?
+       ";"
-      ";"
+       W?
-      W?
+       "int"
-      "int"
+       "main"
-      "main"
+       W?
-      W?
+       "("
-      "("
+       W?
-      W?
+       ")"
-      ")"
+       W?
-      W?
+       "{"
-      "{"
+       W?
-      W?
+ POST = W? "return" W "0" W? ";" W? "}" W?
-POST = W? "return" W "0" W? ";" W? "}" W?
+ D = "int" W V W? ";"
-D = "int" W V W? ";"
+ V = [a-z,A-Z] [a-z,A-Z,0-9]*
-V = [a-z,A-Z] [a-z,A-Z,0-9]*
+ I = (A | L | C) W? ";"
-I = (A | L | C) W? ";"
+ A = V W? "=" W? NE
-A = V W? "=" W? NE
+ L = "while" W? "(" W? BE W? ")" W? "{" W? I* W? "}"
-L = "while" W? "(" W? BE W? ")" W? "{" W? I* W? "}"
+ C = "if" W? "(" W? BE W? ")" W? "{" W? I* W? "}" (W? "else" W? "{" W? I* W? "}")?
-C = "if" W? "(" W? BE W? ")" W? "{" W? I* W? "}" (W? "else" W? "{" W? I* W? "}")?
+ NE = N | V | NE W? NO W? NE | "(" W? NE W? ")" | "-" W? NE
-NE = N | V | NE W? NO W? NE | "(" W? NE W? ")" | "-" W? NE
+ N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"
-N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"
+ BE = "true" | "false" | NE W? BO W? NE | BE W? BC W? BE | "!" W? BE | "(" W? BE W? ")"
-BE = "true" | "false" | NE W? BO W? NE | BE W? BC W? BE | "!" W? BE | "(" W? BE W? ")"
+ NO = "+" | "-" | "*"
-NO = "+" | "-" | "*"
+ BO = "<" | ">" | "<=" | ">=" | "==" | "!="
-BO = "<" | ">" | "<=" | ">=" | "==" | "!="
+ BC = "&&" | "||" | "==" | "!="
-BC = "&&" | "||" | "==" | "!="
+ W = (" " | "\n") (" " | "\n")*
-Calls to {{{__VERIFIER_nondet_int()}}} yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.
+Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.
 Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics are used.

@@ Line 1: / Line 1: @@
 [[Category:Categories]]
-Non-terminals:
+== Proposal ==
-Grammar:
+For the Termination Competition 2015, we propose a new category for C programs restricted to a very small subset of C operating only on integers with addition, subtraction, and multiplication. The purpose of this category is twofold: First, it is easier for new participants to first start with a restricted subset of C than directly tackling the whole language. Second, this subset captures all necessary concepts to express integer transition systems as used by many program analysis tools as intermediate representation of programs.
 P = PRE D* W? I* POST
 PRE = W?
@@ Line 61: / Line 68: @@
 BC = "&&" | "||" | "==" | "!="
 W = (" " | "\n") (" " | "\n")*
-Calls to __VERIFIER_nondet_int() yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.
+Calls to {{{__VERIFIER_nondet_int()}}} yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.
 Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics are used.