Commit 2eea2380 authored by MARCHE Claude's avatar MARCHE Claude

jessie3: complete support for axiomatics

parent eb04cd23
......@@ -72,13 +72,21 @@ let ctype ty =
| TBuiltin_va_list _
-> Self.not_yet_implemented "ctype"
let logic_type ty =
let logic_types = Hashtbl.create 257
let rec logic_type ty =
match ty with
| Linteger -> int_type
| Lreal -> real_type
| Ctype _
| Ltype (_, _)
| Ltype (lt, args) ->
begin
try
let ts = Hashtbl.find logic_types lt.lt_name in
Ty.ty_app ts (List.map logic_type args)
with Not_found -> Self.fatal "logic type %s not found" lt.lt_name
end
| Lvar _
| Ctype _
| Larrow (_, _) ->
Self.not_yet_implemented "logic_type"
......@@ -217,11 +225,12 @@ and term t = (t.term_type, term_node t.term_node)
let rel (ty1,t1) op (ty2,t2) =
match op,ty1,ty2 with
| Req,_,_ -> Term.t_equ t1 t2
| Rneq,_,_ -> Term.t_neq t1 t2
| Rge,Linteger,Linteger -> Term.t_app_infer ge_int [t1;t2]
| Rge,Lreal,Lreal -> Term.t_app_infer ge_real [t1;t2]
| Rge,_,_ ->
Self.not_yet_implemented "rel Rge"
| (Rlt|Rgt|Rle|Rneq),_,_ ->
| (Rlt|Rgt|Rle),_,_ ->
Self.not_yet_implemented "rel"
let rec predicate p =
......@@ -232,12 +241,13 @@ let rec predicate p =
| Pforall (lv, p) ->
let l = List.map create_lvar lv in
Term.t_forall_close l [] (predicate_named p)
| Pimplies (p1, p2) ->
Term.t_implies (predicate_named p1) (predicate_named p2)
| Papp (_, _, _)
| Pseparated _
| Pand (_, _)
| Por (_, _)
| Pxor (_, _)
| Pimplies (_, _)
| Piff (_, _)
| Pnot _
| Pif (_, _, _)
......@@ -268,7 +278,8 @@ let add_decls_as_theory theories id decls =
let th = Theory.create_theory id in
let th = use th int_theory in
let th = use th real_theory in
let th = List.fold_left Theory.add_decl th decls in
let th = List.fold_left use th theories in
let th = List.fold_left Theory.add_decl th (List.rev decls) in
let th = Theory.close_theory th in
th :: theories
......@@ -286,14 +297,15 @@ let rec annot ~in_axiomatic a _loc (theories,decls) =
Ty.create_tysymbol
(Ident.id_user lt.lt_name (Loc.extract loc)) targs tdef
in
Hashtbl.add logic_types lt.lt_name ts;
let d = Decl.create_ty_decl ts in
(theories,d::decls)
| Dfun_or_pred (li, _loc) ->
begin
match li.l_labels, li.l_tparams,li.l_body with
| [],[],LBnone ->
Self.not_yet_implemented "Dfun_or_pred without body"
(* create_param_decl : lsymbol -> decl *)
let ls,_ = create_lsymbol li in
(theories,Decl.create_param_decl ls :: decls)
| [],[],LBterm d ->
let ls,args = create_lsymbol li in
let (_ty,d) = term d in
......@@ -321,7 +333,7 @@ let rec annot ~in_axiomatic a _loc (theories,decls) =
Self.not_yet_implemented "Dlemma with labels or vars"
end
| Daxiomatic (name, decls', loc) ->
let theories = add_decls_as_theory theories (Ident.id_fresh "Decls") decls in
let theories = add_decls_as_theory theories (Ident.id_fresh "Top") decls in
let (t,decls'') =
List.fold_left
(fun acc d -> annot ~in_axiomatic:true d loc acc)
......@@ -451,10 +463,10 @@ let prog p =
in
Self.result "found %d decls" (List.length decls);
let theories =
add_decls_as_theory theories (Ident.id_fresh "Decls") decls
add_decls_as_theory theories (Ident.id_fresh "Top") decls
in
Self.result "made %d theories" (List.length theories);
theories
List.rev theories
with
Decl.UnknownIdent(s) ->
Self.fatal "unknown identifier %s" s.Ident.id_string
......@@ -7,25 +7,26 @@
//@ lemma l1: \forall integer x; f1(x) >= 1;
/*@ axiomatic Bag {
@ type bag<X>;
@ // logic integer occ<X>(<X> x, bag<X> b);
@ // axiom extensionality<X>: \forall bag<X> b1,b2;
@ // (\forall <X> x, occ(x,b1) == occ(x,b2)) ==> b1 == b2;
@ // logic bag<X> singleton<X>(<X> x);
@ // axiom occ_singleton_eq<X>: \forall <X> x;
@ // occ(x,singleton(x)) == 1;
@ // axiom occ_singleton_neq<X>: \forall <X> x,y;
@ // x != y ==> occ(x,singleton(y)) == 0;
@ // logic bag<X> bag_union<X>(bag<X> b1,bag<X> b2);
@ // axiom occ_union<X>: \forall <X> x, bag<X> b1,b2;
@ // occ(x,union(b1,b2)) == occ(x,b1) + occ(x,b2);
/*@ axiomatic BagInt {
@ type bag;
@ logic integer occ(integer x, bag b);
@ axiom extensionality: \forall bag b1,b2;
@ (\forall integer x; occ(x,b1) == occ(x,b2)) ==> b1 == b2;
@ logic bag singleton(integer x);
@ axiom occ_singleton_eq: \forall integer x;
@ occ(x,singleton(x)) == 1;
@ axiom occ_singleton_neq: \forall integer x,y;
@ x != y ==> occ(x,singleton(y)) == 0;
@ logic bag bag_union(bag b1,bag b2);
@ axiom occ_union: \forall integer x, bag b1,b2;
@ occ(x,bag_union(b1,b2)) == occ(x,b1) + occ(x,b2);
@ lemma l2: f1(1) == 2;
@ }
@*/
// lemma union_comm<X>: \forall bag<X> b1,b2;
// bag_union(b1,b2) == bag_union(b2,b1);
/*@ lemma union_comm: \forall bag b1,b2;
@ bag_union(b1,b2) == bag_union(b2,b1);
@*/
......
/*@ axiomatic Bag {
@ type bag<X>;
@ // logic integer occ<X>(<X> x, bag<X> b);
@ // axiom extensionality<X>: \forall bag<X> b1,b2;
@ // (\forall <X> x, occ(x,b1) == occ(x,b2)) ==> b1 == b2;
@ // logic bag<X> singleton<X>(<X> x);
@ // axiom occ_singleton_eq<X>: \forall <X> x;
@ // occ(x,singleton(x)) == 1;
@ // axiom occ_singleton_neq<X>: \forall <X> x,y;
@ // x != y ==> occ(x,singleton(y)) == 0;
@ // logic bag<X> bag_union<X>(bag<X> b1,bag<X> b2);
@ // axiom occ_union<X>: \forall <X> x, bag<X> b1,b2;
@ // occ(x,union(b1,b2)) == occ(x,b1) + occ(x,b2);
@ lemma l2: f1(1) == 2;
@ }
@*/
[kernel] preprocessing with "gcc -C -E -I. tests/basic/axiomatic.c"
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] creating logic symbol 739 (f1)
[jessie3] creating logic symbol 743 (occ)
[jessie3] creating logic symbol 748 (singleton)
[jessie3] creating logic symbol 754 (bag_union)
[jessie3] found 1 decls
[jessie3] made 3 theories
[jessie3] running theory 1:
[jessie3] theory Decls
[jessie3] theory Top
(* use BuiltIn *)
(* use int.Int *)
(* use real.Real *)
lemma l1 : (6 * 7) = 42
function f1 (x:int) : int = (x * x) + 1
lemma l1 : forall x:int. f1 x >= 1
end
[jessie3] Dealing with task 1
[jessie3] Status with CVC3 2.4.1: Valid
......@@ -20,28 +26,58 @@
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] running theory 1:
[jessie3] theory Bag
[jessie3] theory BagInt
(* use BuiltIn *)
(* use int.Int *)
(* use real.Real *)
type bag 'x
(* use Top *)
type bag
function occ int bag : int
axiom extensionality :
forall b1:bag, b2:bag. (forall x:int. occ x b1 = occ x b2) -> b1 = b2
function singleton int : bag
axiom occ_singleton_eq : forall x:int. occ x (singleton x) = 1
axiom occ_singleton_neq :
forall x:int, y:int. not x = y -> occ x (singleton y) = 0
function bag_union bag bag : bag
axiom occ_union :
forall x:int, b1:bag, b2:bag.
occ x (bag_union b1 b2) = (occ x b1 + occ x b2)
lemma l2 : f1 1 = 2
end
[jessie3] Dealing with task 1
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] running theory 1:
[jessie3] theory Decls1
[jessie3] theory Top1
(* use BuiltIn *)
(* use int.Int *)
(* use real.Real *)
lemma l2 : (6 + 7) = 13
(* use BagInt *)
lemma union_comm : forall b1:bag, b2:bag. bag_union b1 b2 = bag_union b2 b1
end
[jessie3] Dealing with task 1
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] Status with Alt-Ergo 0.94: Unknown
[kernel] preprocessing with "gcc -C -E -I. tests/basic/forty-two.c"
[jessie3] processing function f
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] processing function f
[jessie3] found 0 decls
[jessie3] made 0 theories
[kernel] preprocessing with "gcc -C -E -I. tests/basic/generic.c"
tests/basic/generic.c:15:[kernel] user error: unbound function f1 in annotation.
[kernel] user error: skipping file "tests/basic/generic.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
[kernel] preprocessing with "gcc -C -E -I. tests/basic/isqrt.c"
[jessie3] processing function main
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] creating logic symbol 739 (sqr)
[jessie3] processing function isqrt
[kernel] Plug-in jessie3 aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
'[Plug-in jessie3] ctype'.
[kernel] preprocessing with "gcc -C -E -I. tests/basic/lemma.c"
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] found 7 decls
[jessie3] made 1 theories
[jessie3] running theory 1:
[jessie3] theory Decls
[jessie3] theory Top
(* use BuiltIn *)
(* use int.Int *)
......
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