micro-C: for loop, recursive functions

parent 8f1cb933
A plugin to verify programs written in a (microscopic) fragment of C.
Designed for teaching purposes .
Differences/limitations wrt C:
- types are limited to integers and arrays of integers
- integers of type 'int' only, and assumed to be of arbitrary precision
- arrays can be stack allocated or passed as arguments, but cannot be returned
- scanf is limited to scanf("%d", &x)
- a call to printf is ignored (but arguments are evaluated first)
- rand() returns a nonnegative integer, but with no upper limit (no RAND_MAX);
not an issue when used in expressions such as a+rand()%(b-a+1)
Todo:
- spec before or after {
- rand() returns a nonnegative integer
- arrays, stack-allocated
int a[n]; --> array_create n
- functions return either void or int, not int*
- for loop
- function/predicate, possibly with a definition
//@ function int foo(int x, int y);
//@ function int bar(int x, int y) = x+y;
......
......@@ -23,7 +23,9 @@ type binop =
| Band | Bor (* && || *)
type ty =
| Tvoid
| Tint
| Tarray
type loop_annotation =
Ptree.invariant * Ptree.variant
......
......@@ -26,7 +26,7 @@
["if", IF; "else", ELSE;
"return", RETURN; "while", WHILE;
"for", FOR; "break", BREAK;
"int", INT; "scanf", SCANF;
"void", VOID; "int", INT; "scanf", SCANF;
(* annotations *)
"true", TRUE; "false", FALSE;
"forall", FORALL; "exists", EXISTS; "then", THEN; "let", LET; "in", LET;
......
......@@ -48,8 +48,6 @@ let constant ~loc i =
mk_expr ~loc (Econst (Number.int_const_of_int i))
let constant_s ~loc s =
mk_expr ~loc (Econst (Number.(ConstInt (int_literal ILitDec ~neg:false s))))
let len ~loc =
Qident (mk_id ~loc "len")
let break ~loc =
Qident (mk_id ~loc "Break")
let break_handler ~loc =
......@@ -85,8 +83,8 @@ let empty_env =
{ vars = Mstr.empty;
for_index = 0; }
let add_var env = function
| Tint, id -> { env with vars = Mstr.add id.id_str id env.vars }
let add_var env (_, id) =
{ env with vars = Mstr.add id.id_str id env.vars }
let for_vars ~loc env =
let i = env.for_index in
......@@ -173,7 +171,8 @@ let rec expr env ({Mc_ast.expr_loc = loc; Mc_ast.expr_desc = d } as e) =
(Elet (mk_id ~loc "_", false, Expr.RKnone, expr env e, res)) in
List.fold_left eval (mk_unit ~loc) el
| Mc_ast.Ecall (id, el) ->
mk_expr ~loc (Eidapp (Qident id, List.map (expr env) el))
let el = if el = [] then [mk_unit ~loc] else List.map (expr env) el in
mk_expr ~loc (Eidapp (Qident id, el))
| Mc_ast.Eget (e1, e2) ->
mk_expr ~loc (Eidapp (get_op ~loc, [expr env e1; expr env e2]))
......@@ -292,8 +291,7 @@ let decl = function
let param (_ty, id) = id.id_loc, Some id, false, None in
let params = if idl = [] then no_params ~loc else List.map param idl in
let d = if stmt_has_call id bl then
assert false (*TODO*)
(* Drec ([id, false, Expr.RKnone, params, None, Ity.MaskVisible, sp, body], s) *)
Drec ([id, false, Expr.RKnone, params, None, Ity.MaskVisible, sp, body])
else
let e = Efun (params, None, Ity.MaskVisible, sp, body) in
Dlet (id, false, Expr.RKnone, mk_expr ~loc e) in
......@@ -308,10 +306,6 @@ let decl = function
let translate dl =
List.iter decl dl
(* let bl = block empty_env ~loc dl in *)
(* let fd = Efun (no_params ~loc, None, Ity.MaskVisible, empty_spec, bl) in *)
(* let main = Dlet (mk_id ~loc "main", false, Expr.RKnone, mk_expr ~loc fd) in *)
(* Typing.add_decl loc main *)
let read_channel env path file c =
let f : Mc_ast.file = Mc_lexer.parse file c in
......
......@@ -71,7 +71,7 @@
%token EOF
%token LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ COMMA EQUAL SEMICOLON LBRC RBRC
%token PLUS MINUS TIMES DIV MOD
%token INT
%token VOID INT
(* annotations *)
%token INVARIANT VARIANT ASSUME ASSERT CHECK REQUIRES ENSURES LABEL
%token FUNCTION PREDICATE TRUE FALSE
......@@ -122,18 +122,21 @@ func:
{ Dlogic (false, id, l) }
def:
| ty=type_ f=ident LEFTPAR x=separated_list(COMMA, param) RIGHTPAR
| ty=return_type f=ident LEFTPAR x=separated_list(COMMA, param) RIGHTPAR
s=spec bl=block
{ Dfun (ty, f, x, s, bl) }
;
type_:
| INT { Tint }
return_type:
| VOID { Tvoid }
| INT { Tint }
;
param:
| ty=type_ id=ident
{ ty, id }
| INT id=ident
{ Tint, id }
| INT id=ident LEFTSQ RIGHTSQ
{ Tarray, id }
;
spec:
......@@ -249,24 +252,18 @@ simple_stmt_desc:
{ Sskip }
| RETURN e = expr SEMICOLON
{ Sreturn e }
| ty=type_ id=ident EQUAL e = expr SEMICOLON
{ Svar (ty, id, e) }
| ty=type_ id=ident SEMICOLON
| INT id=ident SEMICOLON
{ let any_int = mk_id "any_int" $startpos $endpos in
let loc = floc $startpos $endpos in
let e = mk_expr loc (Ecall (any_int, [mk_expr loc Eunit])) in
Svar (ty, id, e) }
| id = ident EQUAL e = expr SEMICOLON
{ Sassign (id, e) }
| id = ident op=assignop e = expr SEMICOLON
{ let loc = floc $startpos $endpos in
Seval (mk_expr loc (Ecall (op, [mk_expr loc (Eaddr id); e]))) }
| e1 = expr LEFTSQ e2 = expr RIGHTSQ EQUAL e3 = expr SEMICOLON
{ Sset (e1, e2, e3) }
Svar (Tint, id, e) }
| INT id=ident LEFTSQ e=expr RIGHTSQ SEMICOLON
{ let alloc_array = mk_id "alloc_array" $startpos $endpos in
let loc = floc $startpos $endpos in
let e = mk_expr loc (Ecall (alloc_array, [e])) in
Svar (Tarray, id, e) }
| k=assertion_kind t = term SEMICOLON
{ Sassert (k, t) }
| e = expr SEMICOLON
{ Seval e }
| BREAK SEMICOLON
{ Sbreak }
| LABEL id=ident SEMICOLON
......@@ -277,10 +274,31 @@ simple_stmt_desc:
{ Sif (c, s1, s2) }
| WHILE LEFTPAR e=expr RIGHTPAR b=loop_body
{ let iv, l = b in Swhile (e, iv, l) }
(* TODO: below, do not accept simple_stmt for e1 and e2, only expr *)
| FOR LEFTPAR s1=simple_stmt SEMICOLON e=expr SEMICOLON s2=simple_stmt
| FOR LEFTPAR e1=expr_stmt SEMICOLON e=expr SEMICOLON e2=expr_stmt
RIGHTPAR b=loop_body
{ assert false (*TODO*) }
{ let loc = floc $startpos $endpos in
let iv, l = b in
Sblock [e1;
mk_stmt loc (Swhile (e, iv, mk_stmt loc (Sblock [l; e2])))]
}
| s=expr_stmt_desc SEMICOLON
{ s }
;
expr_stmt: located(expr_stmt_desc) { $1 };
expr_stmt_desc:
| INT id=ident EQUAL e = expr
{ Svar (Tint, id, e) }
| id = ident EQUAL e = expr
{ Sassign (id, e) }
| id = ident op=assignop e = expr
{ let loc = floc $startpos $endpos in
Seval (mk_expr loc (Ecall (op, [mk_expr loc (Eaddr id); e]))) }
| e1 = expr LEFTSQ e2 = expr RIGHTSQ EQUAL e3 = expr
{ Sset (e1, e2, e3) }
| e = expr
{ Seval e }
;
assignop:
......
#include <stdio.h>
#include <stdlib.h>
int foo(int a[])
//@ requires length(a) >= 1;
//@ ensures result == 0 ;
{
return a[0];
}
int main()
{
int x;
//@ assert x == 0;
printf("%d", 2);
int a[10];
int r = foo(a);
//@ assert r == 0;
int x = 10 + rand() % 10;
//@ assert 10 <= x <= 19;
}
......
......@@ -7,6 +7,9 @@ module MicroC
use ref.Ref
use array.Array
function length (a: array 'a) : int =
Array.length a
function ([]) (l: array 'a) (i: int) : 'a =
Array.([]) l i
......
#include <stdio.h>
#include <stdlib.h>
// recherche dichotomique dans un tableau trié
int dicho(int a[], int n, int v)
//@ requires length(a) == n;
//@ requires forall i1, i2. 0 <= i1 <= i2 < n -> a[i1] <= a[i2];
//@ ensures -1 <= result < n;
//@ ensures result == -1 -> forall i. 0 <= i < n -> a[i] != v;
//@ ensures result >= 0 -> a[result] == v;
{
int l = 0;
int u = n-1;
int r = -1;
while (l <= u) {
//@ invariant 0 <= l && u < n;
//@ invariant r == -1;
//@ invariant forall i. 0 <= i < n -> a[i] == v -> l <= i <= u;
//@ variant u - l;
int m = (l + u) / 2;
if (a[m] < v)
l = m+1;
else if (a[m] > v)
u = m-1;
else {
r = m;
break;
}
}
return r;
}
int main() {
int n = 42;
int a[n];
a[0] = rand() % 100;
printf("%d, ", a[0]);
for (int i = 1; i < n; i++) {
//@ invariant 1 <= i <= n;
//@ invariant forall i1, i2. 0 <= i1 <= i2 < i -> a[i1] <= a[i2];
//@ variant n - i;
a[i] = a[i-1] + rand() % 10;
printf("%d, ", a[i]);
}
printf("\n");
//@ assert forall i1, i2. 0 <= i1 <= i2 < length(a) -> a[i1] <= a[i2];
printf("quelle valeur cherchez-vous ? ");
int v;
scanf("%d", &v);
int r = dicho(a, n, v);
if (r == -1)
printf("valeur absente\n");
else
printf("valeur présente à la position %d\n,", r);
}
// tri par insertion
#include <stdio.h>
#include <stdlib.h>
void sort(int a[], int n)
//@ requires length(a) == n >= 1;
//@ ensures forall i,j. 0 <= i <= j < n -> a[i] <= a[j];
{
for (int m = 1; m < n; m++) {
//@ invariant 1 <= m <= n;
//@ invariant forall i,j. 0 <= i <= j < m -> a[i] <= a[j];
//@ variant n - m;
int x = a[m];
int k;
for (k = m; k > 0 && a[k-1] > x; k--) {
//@ invariant 0 <= k <= m;
//@ invariant forall i,j. 0 <= i <= j < k -> a[i] <= a[j];
//@ invariant forall i,j. 0 <= i < k < j <= m -> a[i] <= a[j];
//@ invariant forall i,j. k < i <= j <= m -> a[i] <= a[j];
//@ invariant forall j. k < j <= m -> x < a[j];
//@ variant k;
a[k] = a[k-1];
}
a[k] = x;
}
}
int main() {
int n = 42;
int a[n];
for (int i = 0; i < n; i++) {
//@ invariant 0 <= i <= n; //@ variant n - i;
a[i] = rand() % 100;
printf("%d, ", a[i]);
}
printf("\n");
sort(a, n);
for (int i = 0; i < n; i++) {
//@ invariant 0 <= i <= n; //@ variant n - i;
printf("%d, ", a[i]);
}
printf("\n");
return 0;
}
#include <stdio.h>
// la somme des n premiers entiers
int triangular(int n)
//@ requires n >= 0;
//@ ensures result == n * (n+1) / 2;
//@ ensures result == n * (n + 1) / 2;
{
int s = 0;
int k = 0;
while (k <= n) {
//@ invariant k <= n+1;
for (int k = 0; k <= n; k++) {
//@ invariant k <= n + 1;
//@ invariant s == (k - 1) * k / 2;
//@ variant n - k;
s += k;
k++;
}
return s;
}
int triangular2(int n)
//@ requires n >= 0;
//@ ensures result == n * (n + 1) / 2;
//@ variant n;
{
if (n == 0) return 0;
return n + triangular2(n - 1);
}
int main() {
printf("somme 1 + .. + 100 = %d\n", triangular(100));
printf("somme 1 + .. + 100 = %d\n", triangular2(100));
return 0;
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment