diff --git a/src/jessie/ACSLtoWhy3.ml b/src/jessie/ACSLtoWhy3.ml index 79620c6ee5a7f1f43de0b21221e522abcf982355..933aab137f8d111c82e45710d5bb362a849bcebd 100644 --- a/src/jessie/ACSLtoWhy3.ml +++ b/src/jessie/ACSLtoWhy3.ml @@ -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 diff --git a/src/jessie/tests/basic/axiomatic.c b/src/jessie/tests/basic/axiomatic.c index d5f8d24c4ad9d8e6bba8db94712cee707c8e607c..25ba9fb379a9d04a860186fa8e684d065bb2a1d7 100644 --- a/src/jessie/tests/basic/axiomatic.c +++ b/src/jessie/tests/basic/axiomatic.c @@ -7,25 +7,26 @@ //@ lemma l1: \forall integer x; f1(x) >= 1; -/*@ axiomatic Bag { - @ type bag; - @ // logic integer occ( x, bag b); - @ // axiom extensionality: \forall bag b1,b2; - @ // (\forall x, occ(x,b1) == occ(x,b2)) ==> b1 == b2; - @ // logic bag singleton( x); - @ // axiom occ_singleton_eq: \forall x; - @ // occ(x,singleton(x)) == 1; - @ // axiom occ_singleton_neq: \forall x,y; - @ // x != y ==> occ(x,singleton(y)) == 0; - @ // logic bag bag_union(bag b1,bag b2); - @ // axiom occ_union: \forall x, bag 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: \forall bag 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); + @*/ diff --git a/src/jessie/tests/basic/generic.c b/src/jessie/tests/basic/generic.c new file mode 100644 index 0000000000000000000000000000000000000000..7d8c36e469fe3eb3628b2fe6046731842e718266 --- /dev/null +++ b/src/jessie/tests/basic/generic.c @@ -0,0 +1,17 @@ + +/*@ axiomatic Bag { + @ type bag; + @ // logic integer occ( x, bag b); + @ // axiom extensionality: \forall bag b1,b2; + @ // (\forall x, occ(x,b1) == occ(x,b2)) ==> b1 == b2; + @ // logic bag singleton( x); + @ // axiom occ_singleton_eq: \forall x; + @ // occ(x,singleton(x)) == 1; + @ // axiom occ_singleton_neq: \forall x,y; + @ // x != y ==> occ(x,singleton(y)) == 0; + @ // logic bag bag_union(bag b1,bag b2); + @ // axiom occ_union: \forall x, bag b1,b2; + @ // occ(x,union(b1,b2)) == occ(x,b1) + occ(x,b2); + @ lemma l2: f1(1) == 2; + @ } + @*/ diff --git a/src/jessie/tests/basic/oracle/axiomatic.res.oracle b/src/jessie/tests/basic/oracle/axiomatic.res.oracle index 40d83588a2ca9e76349e0c0735ddeeafaae5cbf1..f9a52267cf3e6a188e93a53d25ffebabdf1efdef 100644 --- a/src/jessie/tests/basic/oracle/axiomatic.res.oracle +++ b/src/jessie/tests/basic/oracle/axiomatic.res.oracle @@ -1,17 +1,23 @@ [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 diff --git a/src/jessie/tests/basic/oracle/forty-two.res.oracle b/src/jessie/tests/basic/oracle/forty-two.res.oracle index bb7b2a701891fa7e282a07f241ad9956b4dc8a27..9ef89d85fc193e21888b449afac9d4921ea070ca 100644 --- a/src/jessie/tests/basic/oracle/forty-two.res.oracle +++ b/src/jessie/tests/basic/oracle/forty-two.res.oracle @@ -1,6 +1,6 @@ [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 diff --git a/src/jessie/tests/basic/oracle/generic.err.oracle b/src/jessie/tests/basic/oracle/generic.err.oracle new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/jessie/tests/basic/oracle/generic.res.oracle b/src/jessie/tests/basic/oracle/generic.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..ba3398286cf2d601f68caa291c16ff8f9edafaef --- /dev/null +++ b/src/jessie/tests/basic/oracle/generic.res.oracle @@ -0,0 +1,4 @@ +[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. diff --git a/src/jessie/tests/basic/oracle/isqrt.res.oracle b/src/jessie/tests/basic/oracle/isqrt.res.oracle index 2b38d24a5b5167f43840a9081784b76ed6b21324..d6a1c31dc583d048accf64d1d03791919059c156 100644 --- a/src/jessie/tests/basic/oracle/isqrt.res.oracle +++ b/src/jessie/tests/basic/oracle/isqrt.res.oracle @@ -1,5 +1,8 @@ [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'. diff --git a/src/jessie/tests/basic/oracle/lemma.res.oracle b/src/jessie/tests/basic/oracle/lemma.res.oracle index fda45347b3e1a06a14b8d47e8ebba7d50e2cdb44..4361702996e8e570cfed2edb1cb21114adca4eb4 100644 --- a/src/jessie/tests/basic/oracle/lemma.res.oracle +++ b/src/jessie/tests/basic/oracle/lemma.res.oracle @@ -1,10 +1,10 @@ [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 *)