Skip to content
Snippets Groups Projects
Commit 8363a1f3 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] remove all non-standard metas in Why3 theories

parent eaff43d4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/ProverWhy3.ml
+ 0
− 15
View file @ 8363a1f3
......@@ -1184,21 +1184,6 @@ let prover_task env prover task =
let prover_config = Why3.Whyconf.get_prover_config config prover in
let drv = Why3.Driver.load_driver_for_prover (Why3.Whyconf.get_main config)
env prover_config in
let remove_for_prover =
if prover.prover_name = "Alt-Ergo"
then Filter_axioms.remove_for_altergo
else Filter_axioms.remove_for_why3
in
let trans = Why3.Trans.seq [
remove_for_prover;
Filter_axioms.trans;
Filter_axioms.def_into_axiom
] in
let task =
if prover.prover_name = "Coq"
then task
else Why3.Trans.apply trans task
in
drv , prover_config , Why3.Driver.prepare_task drv task
(* -------------------------------------------------------------------------- *)
......
src/plugins/wp/filter_axioms.ml deleted 100644 → 0
+ 0
− 176
View file @ eaff43d4
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2024 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Why3
open Term
open Decl
let meta_remove_altergo =
Theory.register_meta "remove_for_altergo"
[Theory.MTprsymbol]
~desc:"Don't@ translate@ this@ lemma@ for@ altergo."
let meta_remove_why3 =
Theory.register_meta "remove_for_why3"
[Theory.MTprsymbol]
~desc:"Don't@ translate@ this@ lemma@ for@ why3."
let meta_remove_ =
Theory.register_meta "remove_for_"
[Theory.MTprsymbol]
~desc:"Don't@ translate@ this@ lemma@ for@ why3 and altergo."
let elim_abstract remove_pr d = match d.d_node with
| Dprop (Paxiom,pr,_) when Spr.mem pr remove_pr -> []
| Dprop (Paxiom,_,_) -> [d]
| _ -> [d]
let remove_prop meta =
Trans.on_tagged_pr meta
(fun remove_pr ->
Trans.on_tagged_pr meta_remove_
(fun remove_pr2 ->
Trans.decl (elim_abstract (Spr.union remove_pr remove_pr2)) None))
let remove_for_altergo = remove_prop meta_remove_altergo
let remove_for_why3 = remove_prop meta_remove_why3
let () =
Trans.register_transform "remove_for_altergo"
remove_for_altergo
~desc:"Remove@ tagged@ proposition@ with \"remove_for_altergo\"@ and \
\"remove_for_\"@ metas."
let () =
Trans.register_transform "remove_for_why3"
remove_for_why3
~desc:"Remove@ tagged@ proposition@ with \"remove_for_why3\"@ and \
\"remove_for_\" metas."
(** inlining *)
let meta_inline_in =
Theory.register_meta "inline_in"
[Theory.MTlsymbol;Theory.MTprsymbol;]
~desc:"Inline@ the@ symbol@ in@ the@ proposition."
let t_unfold defs fs tl ty =
match Mls.find_opt fs defs with
| None ->
assert false (* absurd: it is in mpr so it is in sls so added in defs *)
| Some (vl,e) ->
let add (mt,mv) x y = Ty.ty_match mt x.vs_ty (t_type y), Mvs.add x y mv in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vl tl in
let mt = Ty.oty_match mt e.t_ty ty in
t_ty_subst mt mv e
(* inline every symbol *)
let rec t_replace_all defs s t =
let t = t_map (t_replace_all defs s) t in
match t.t_node with
| Tapp (fs,tl) when Sls.mem fs s ->
t_attr_copy t (t_unfold defs fs tl t.t_ty)
| _ -> t
let fold mpr sls d (defs, task) =
(* replace *)
let d = match d.d_node with
| Dprop (k,pr,f) ->
let s = Mpr.find_def Sls.empty pr mpr in
if Sls.is_empty s then d
else create_prop_decl k pr (t_replace_all defs s f)
| _ -> d
in
(* add to defs if needed *)
match d.d_node with
| Dlogic [ls,ld] when Sls.mem ls sls ->
let vl,e = open_ls_defn ld in
Mls.add ls (vl,e) defs, Task.add_decl task d
| _ ->
defs, Task.add_decl task d
let fold mpr sls task_hd (defs, task) =
match task_hd.Task.task_decl.Theory.td_node with
| Theory.Decl d ->
fold mpr sls d (defs, task)
| _ ->
defs, Task.add_tdecl task task_hd.Task.task_decl
let trans =
let add (mpr,sls) = function
| [Theory.MAls ls; Theory.MApr pr] ->
Mpr.change (function None -> Some (Sls.singleton ls)
| Some s -> Some (Sls.add ls s)) pr mpr,
Sls.add ls sls
| _ -> assert false
in
Trans.on_meta meta_inline_in (fun l ->
let mpr, sls = List.fold_left add (Mpr.empty,Sls.empty) l in
Trans.fold_map (fold mpr sls) Mls.empty None)
let () =
Trans.register_transform "inline_in"
trans
~desc:"Inline@ the@ symbol@ in@ the@ proposition(meta@ of@ the@ same@ name)"
(*** eliminate function *)
let meta_def_into_axiom =
Theory.register_meta "def_into_axiom"
[Theory.MTlsymbol]
~desc:"Turn the marked function into an axiom"
let add_ld which (ls,ld) (abst,defn,axl) =
if which ls then
let vl,e = open_ls_defn ld in
let nm = ls.ls_name.Ident.id_string ^ "_def" in
let pr = create_prsymbol (Ident.id_derive nm ls.ls_name) in
let hd = t_app ls (List.map t_var vl) e.t_ty in
let e = TermTF.t_selecti Term.t_equ_simp Term.t_iff_simp hd e in
let ax = t_forall_close vl [[hd]] e in
let ax = create_prop_decl Paxiom pr ax in
let ld = create_param_decl ls in
ld :: abst, defn, ax :: axl
else
abst, (ls,ld) :: defn, axl
let elim_decl which l =
let abst,defn,axl = List.fold_right (add_ld which) l ([],[],[]) in
let defn = if defn = [] then [] else [create_logic_decl defn] in
abst @ defn @ axl
let elim which d = match d.d_node with
| Dlogic l -> elim_decl which l
| _ -> [d]
let def_into_axiom =
Trans.on_tagged_ls meta_def_into_axiom (fun sls ->
Trans.decl (elim (fun ls -> Term.Sls.mem ls sls)) None)
let () =
Trans.register_transform "def_into_axiom"
def_into_axiom
~desc:"Turn the marked function into an axiom"
src/plugins/wp/filter_axioms.mli deleted 100644 → 0
+ 0
− 26
View file @ eaff43d4
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2024 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
val remove_for_altergo : Why3.Task.task Why3.Trans.trans
val remove_for_why3 : Why3.Task.task Why3.Trans.trans
val trans : Why3.Task.task Why3.Trans.trans
val def_into_axiom : Why3.Task.task Why3.Trans.trans
src/plugins/wp/share/why3/frama_c_wp/cbits.mlw
+ 0
− 240
View file @ 8363a1f3
......@@ -61,9 +61,6 @@ theory Cbits
axiom land_0bis: forall x:int [land x 0]. (land x 0) = 0
axiom land_1: forall x:int [land (-1) x]. (land (-1) x) = x
axiom land_1bis: forall x:int [land x (-1)]. (land x (-1)) = x
axiom land_bool:
(land 0 0) = 0 /\ (land 0 1) = 0 /\ (land 1 0) = 0 /\ (land 1 1) = 1
meta "remove_for_" axiom land_bool
(** ** lor identities *)
axiom lor_idemp: forall x:int [lor x x]. (lor x x) = x
......@@ -72,9 +69,6 @@ theory Cbits
axiom lor_1bis: forall x:int [lor x (-1)]. (lor x (-1)) = -1
axiom lor_0: forall x:int [lor 0 x]. (lor 0 x) = x
axiom lor_0bis: forall x:int [lor x 0]. (lor x 0) = x
axiom lor_bool:
(lor 0 0) = 0 /\ (lor 0 1) = 1 /\ (lor 1 0) = 1 /\ (lor 1 1) = 1
meta "remove_for_" axiom lor_bool
(** ** lxor identities *)
axiom lxor_nilpotent: forall x:int [lxor x x]. (lxor x x) = 0
......@@ -83,9 +77,6 @@ theory Cbits
axiom lxor_1bis: forall x:int [lxor x (-1)]. (lxor x (-1)) = (lnot x)
axiom lxor_0: forall x:int [lxor 0 x]. (lxor 0 x) = x
axiom lxor_0bis: forall x:int [lxor x 0]. (lxor x 0) = x
axiom lxor_bool:
(lxor 0 0) = 0 /\ (lxor 0 1) = 1 /\ (lxor 1 0) = 1 /\ (lxor 1 1) = 0
meta "remove_for_" axiom lxor_bool
(** ** lsl identities *)
......@@ -115,9 +106,6 @@ theory Cbits
axiom bit_test_extraction: forall x k:int [land x (lsl 1 k)|land (lsl 1 k) x].
0<=k -> (land x (lsl 1 k))<>0 <-> (bit_test x k)
lemma bit_test_extraction_eq: forall x k:int [land x (lsl 1 k)|land (lsl 1 k) x].
0<=k -> (land x (lsl 1 k))=(lsl 1 k) <-> (bit_test x k)
meta "remove_for_" lemma bit_test_extraction_eq
axiom lsl_1_0:
lsl 1 0 = 1
......@@ -126,276 +114,97 @@ theory Cbits
axiom bit_test_extraction_bis_eq: forall x :int [land x 1|land 1 x].
(bit_test x 0) -> (land 1 x)=1
lemma lnot_extraction_bool: forall x i:int [bit_testb (lnot x) i].
0<=i -> bit_testb (lnot x) i = notb (bit_testb x i)
axiom lnot_extraction: forall x i:int [bit_test (lnot x) i].
0<=i -> (bit_test (lnot x) i) <-> not (bit_test x i)
meta "remove_for_" lemma lnot_extraction_bool
lemma land_extraction_bool: forall x y i:int [bit_testb (land x y) i].
0<=i -> bit_testb (land x y) i = andb (bit_testb x i) (bit_testb y i)
axiom land_extraction: forall x y i:int [bit_test (land x y) i].
0<=i -> bit_test (land x y) i <-> ((bit_test x i) /\ (bit_test y i))
meta "remove_for_" lemma land_extraction_bool
lemma lor_extraction_bool: forall x y i:int [bit_testb (lor x y) i].
0<=i -> bit_testb (lor x y) i = orb (bit_testb x i) (bit_testb y i)
axiom lor_extraction: forall x y i:int [bit_test (lor x y) i].
0<=i -> (bit_test (lor x y) i) <-> ((bit_test x i) \/ (bit_test y i))
meta "remove_for_" lemma lor_extraction_bool
lemma lxor_extraction_bool: forall x y i:int [bit_testb (lxor x y) i].
0<=i -> bit_testb (lxor x y) i = xorb (bit_testb x i) (bit_testb y i)
axiom lxor_extraction: forall x y i:int [bit_test (lxor x y) i].
0<=i -> (bit_test (lxor x y) i) <-> ((bit_test x i) <-> not (bit_test y i))
meta "remove_for_" lemma lxor_extraction_bool
(** ** Shift operators *)
lemma lsl_1_two_power : forall n : int. 0 <= n -> lsl 1 n = Cint.two_power_abs n
meta "remove_for_" lemma lsl_1_two_power
axiom land_1_lsl_1 : forall a x n : int [(lsl 1 (1+n)),(lsl 1 n),(2*a+(land 1 x))] .
0<=n -> a<lsl 1 n -> 2*a+(land 1 x)<lsl 1 (1+n)
lemma lsl_extraction_sup_bool: forall x n m:int [bit_testb (lsl x n) m].
0<=n -> 0<=m -> m>=n -> bit_testb (lsl x n) m = bit_testb x (m-n)
axiom lsl_extraction_sup: forall x n m:int [bit_test (lsl x n) m].
0<=n -> 0<=m -> m>=n -> (bit_test (lsl x n) m) <-> (bit_test x (m-n))
meta "remove_for_" lemma lsl_extraction_sup_bool
lemma lsl_extraction_inf_bool: forall x n m:int [bit_testb (lsl x n) m].
0<=n -> 0<=m -> m< n -> bit_testb (lsl x n) m = False
axiom lsl_extraction_inf: forall x n m:int [bit_test (lsl x n) m].
0<=n -> 0<=m -> m< n -> not (bit_test (lsl x n) m)
meta "remove_for_" lemma lsl_extraction_inf_bool
lemma lsr_extraction_bool: forall x n m:int [bit_testb (lsr x n) m].
0<=n -> 0<=m -> bit_testb (lsr x n) m = bit_testb x (m+n)
axiom lsr_extractionl: forall x n m:int [bit_test (lsr x n) m].
0<=n -> 0<=m -> (bit_test (lsr x n) m) <-> (bit_test x (m+n))
meta "remove_for_" lemma lsr_extraction_bool
lemma lsl1_extraction_bool: forall i j:int [bit_testb (lsl 1 i) j].
0<=i -> 0<=j -> bit_testb (lsl 1 i) j = eqb i j
axiom lsl1_extraction: forall i j:int [bit_test (lsl 1 i) j].
0<=i -> 0<=j -> (bit_test (lsl 1 i) j) <-> i=j
meta "remove_for_" lemma lsl1_extraction_bool
lemma pos_extraction_sup: forall x i j:int [(lsl 1 i),(bit_test x j)].
0<=x -> 0<=i -> x < (lsl 1 i) -> i <= j -> not (bit_test x j)
meta "remove_for_" lemma pos_extraction_sup
lemma pos_extraction_sup_inv: forall x i :int .
0<=i -> (forall j: int . i <= j -> not (bit_test x j)) -> 0<= x < (lsl 1 i)
meta "remove_for_" lemma pos_extraction_sup_inv
(** * Link between Bit extraction and C type conversions *)
(** ** Unsigned conversions *)
lemma to_uint_extraction_sup: forall n x i:int .
0<=n<=i -> is_uint n x -> not (bit_test x i)
lemma to_uint_extraction_inf_bool: forall n x i:int .
0<=i<n -> (bit_testb (to_uint n x) i) = (bit_testb x i)
lemma to_uint_extraction_inf: forall n x i:int .
0<=i<n -> (bit_test (to_uint n x) i) <-> (bit_test x i)
lemma is_uint_ext : forall n x y:int .
0<=n -> is_uint n x -> is_uint n y
-> (forall i: int. 0<=i<n -> (bit_test x i <-> bit_test y i))
-> x = y
meta "remove_for_" lemma to_uint_extraction_sup
meta "remove_for_" lemma to_uint_extraction_inf_bool
meta "remove_for_" lemma to_uint_extraction_inf
meta "remove_for_" lemma is_uint_ext
(** *** Cast to uint8 C type *)
axiom to_uint8_extraction_sup: forall x i:int [(is_uint8 x),(bit_test x i)].
8<=i -> is_uint8 x -> not (bit_test x i)
lemma to_uint8_extraction_inf_bool: forall x i:int [bit_testb (to_uint8 x) i].
0<=i<8 -> (bit_testb (to_uint8 x) i) = (bit_testb x i)
axiom to_uint8_extraction_inf: forall x i:int [bit_test (to_uint8 x) i].
0<=i<8 -> (bit_test (to_uint8 x) i) <-> (bit_test x i)
meta "remove_for_" lemma to_uint8_extraction_inf_bool
lemma is_uint8_ext : forall x y:int .
is_uint8 x -> is_uint8 y
-> (forall i: int. 0<=i<8 -> (bit_test x i <-> bit_test y i))
-> x = y
meta "remove_for_" lemma is_uint8_ext
(** *** Cast to uint16 C type *)
axiom to_uint16_extraction_sup: forall x i:int [(is_uint16 x),(bit_test x i)].
16<=i -> is_uint16 x -> not (bit_test x i)
lemma to_uint16_extraction_inf_bool: forall x i:int [bit_testb (to_uint16 x) i].
0<=i<16 -> (bit_testb (to_uint16 x) i) = (bit_testb x i)
axiom to_uint16_extraction_inf: forall x i:int [bit_test (to_uint16 x) i].
0<=i<16 -> (bit_test (to_uint16 x) i) <-> (bit_test x i)
meta "remove_for_" lemma to_uint16_extraction_inf_bool
lemma is_uint16_ext : forall x y:int .
is_uint16 x -> is_uint16 y
-> (forall i: int. 0<=i<16 -> (bit_test x i <-> bit_test y i))
-> x = y
meta "remove_for_" lemma is_uint16_ext
(** *** Cast to uint32 C type *)
axiom to_uint32_extraction_sup: forall x i:int [(is_uint32 x),(bit_test x i)].
32<=i -> is_uint32 x -> not (bit_test x i)
lemma to_uint32_extraction_inf_bool: forall x i:int [bit_testb (to_uint32 x) i].
0<=i<32 -> (bit_testb (to_uint32 x) i) = (bit_testb x i)
axiom to_uint32_extraction_inf: forall x i:int [bit_test (to_uint32 x) i].
0<=i<32 -> (bit_test (to_uint32 x) i) <-> (bit_test x i)
meta "remove_for_" lemma to_uint32_extraction_inf_bool
lemma is_uint32_ext : forall x y:int .
is_uint32 x -> is_uint32 y
-> (forall i: int. 0<=i<32 -> (bit_test x i <-> bit_test y i))
-> x = y
meta "remove_for_" lemma is_uint32_ext
(** *** Cast to uint64 C type *)
axiom to_uint64_extraction_sup: forall x i:int [(is_uint64 x),(bit_test x i)].
64<=i -> (is_uint64 x) -> not (bit_test x i)
lemma to_uint64_extraction_inf_bool: forall x i:int [bit_testb (to_uint64 x) i].
0<=i<64 -> (bit_testb (to_uint64 x) i) = (bit_testb x i)
axiom to_uint64_extraction_inf: forall x i:int [bit_test (to_uint64 x) i].
0<=i<64 -> (bit_test (to_uint64 x) i) <-> (bit_test x i)
meta "remove_for_" lemma to_uint64_extraction_inf_bool
lemma is_uint64_ext : forall x y:int .
is_uint64 x -> is_uint64 y
-> (forall i: int. 0<=i<64 -> (bit_test x i <-> bit_test y i))
-> x = y
meta "remove_for_" lemma is_uint64_ext
(** ** Signed conversions *)
lemma to_sint_extraction_sup: forall n x i:int .
0<=n<=i -> is_sint n x -> (bit_test x i) <-> x < 0
lemma to_sint_extraction_inf_bool: forall n x i:int .
0<=i<n -> (bit_testb (to_sint n x) i) = (bit_testb x i)
lemma to_sint_extraction_inf: forall n x i:int .
0<=i<n -> (bit_test (to_sint n x) i) <-> (bit_test x i)
lemma is_sint_ext : forall n x y:int .
0<=n -> is_sint n x -> is_sint n y
-> (forall i: int. 0<=i<=n -> (bit_test x i <-> bit_test y i))
-> x = y
meta "remove_for_" lemma to_sint_extraction_sup
meta "remove_for_" lemma to_sint_extraction_inf_bool
meta "remove_for_" lemma to_sint_extraction_inf
meta "remove_for_" lemma is_sint_ext
(** *** Cast to sint8 C type *)
axiom to_sint8_extraction_sup: forall x i:int [(is_sint8 x),(bit_test x i)].
7<=i -> is_sint8 x -> (bit_test x i) <-> x < 0
lemma to_sint8_extraction_inf_bool: forall x i:int [(bit_testb (to_sint8 x) i)].
0<=i<7 -> (bit_testb (to_sint8 x) i) = (bit_testb x i)
axiom to_sint8_extraction_inf: forall x i:int [(bit_test (to_sint8 x) i)].
0<=i<7 -> (bit_test (to_sint8 x) i) <-> (bit_test x i)
meta "remove_for_" lemma to_sint8_extraction_inf_bool
lemma is_sint8_ext : forall x y:int .
is_sint8 x -> is_sint8 y
-> (forall i: int. 0<=i<=7 -> (bit_test x i <-> bit_test y i))
-> x = y
meta "remove_for_" lemma is_sint8_ext
(** *** Cast to sint16 C type *)
axiom to_sint16_extraction_sup: forall x i:int [(is_sint16 x),(bit_test x i)].
15<=i -> is_sint16 x -> (bit_test x i) <-> x < 0
lemma to_sint16_extraction_inf_bool: forall x i:int [bit_testb (to_sint16 x) i].
0<=i<15 -> (bit_testb (to_sint16 x) i) = (bit_testb x i)
axiom to_sint16_extraction_inf: forall x i:int [bit_test (to_sint16 x) i].
0<=i<15 -> (bit_test (to_sint16 x) i) <-> (bit_test x i)
meta "remove_for_" lemma to_sint16_extraction_inf_bool
lemma is_sint16_ext : forall x y:int .
is_sint16 x -> is_sint16 y
-> (forall i: int. 0<=i<=15 -> (bit_test x i <-> bit_test y i))
-> x = y
meta "remove_for_" lemma is_sint16_ext
(** *** Cast to sint32 C type *)
axiom to_sint32_extraction_sup: forall x i:int [(is_sint32 x),(bit_test x i)].
31<=i -> is_sint32 x -> (bit_test x i) <-> x < 0
lemma to_sint32_extraction_inf_bool: forall x i:int [bit_testb (to_sint32 x) i].
0<=i<31 -> (bit_testb (to_sint32 x) i) = (bit_testb x i)
axiom to_sint32_extraction_inf: forall x i:int [bit_test (to_sint32 x) i].
0<=i<31 -> (bit_test (to_sint32 x) i) <-> (bit_test x i)
meta "remove_for_" lemma to_sint32_extraction_inf_bool
lemma is_sint32_ext : forall x y:int .
is_sint32 x -> is_sint32 y
-> (forall i: int. 0<=i<=31 -> (bit_test x i <-> bit_test y i))
-> x = y
meta "remove_for_" lemma is_sint32_ext
(** *** Cast to sint64 C type *)
axiom to_sint64_extraction_sup: forall x i:int [(is_sint64 x),(bit_test x i)].
63<=i -> is_sint64 x -> (bit_test x i) <-> x < 0
lemma to_sint64_extraction_inf_bool: forall x i:int [bit_testb (to_sint64 x) i].
0<=i<63 -> (bit_testb (to_sint64 x) i) = (bit_testb x i)
axiom to_sint64_extraction_inf: forall x i:int [bit_test (to_sint64 x) i].
0<=i<63 -> (bit_test (to_sint64 x) i) <-> (bit_test x i)
meta "remove_for_" lemma to_sint64_extraction_inf_bool
lemma is_sint64_ext : forall x y:int .
is_sint64 x -> is_sint64 y
-> (forall i: int. 0<=i<=63 -> (bit_test x i <-> bit_test y i))
-> x = y
meta "remove_for_" lemma is_sint64_ext
(** * Some C-Integer Bits Conversions are distributive *)
(** ** Unsigned conversions *)
lemma to_uint_lor : forall n x y:int.
to_uint n (lor x y) = lor (to_uint n x) (to_uint n y)
meta "remove_for_" lemma to_uint_lor
(** *** Cast to uint8 C type *)
lemma to_uint8_lor : forall x y:int [to_uint8 (lor x y)].
to_uint8 (lor x y) = lor (to_uint8 x) (to_uint 8 y)
meta "remove_for_" lemma to_uint8_lor
(** *** Cast to uint16 C type *)
lemma to_uint16_lor : forall x y:int [to_uint16 (lor x y)].
to_uint16 (lor x y) = lor (to_uint16 x) (to_uint16 y)
meta "remove_for_" lemma to_uint16_lor
(** *** Cast to uint32 C type *)
axiom to_uint32_lor : forall x y:int [to_uint32 (lor x y)].
to_uint32 (lor x y) = lor (to_uint32 x) (to_uint32 y)
meta "remove_for_" axiom to_uint32_lor
(** *** Cast to uint64 C type *)
lemma to_uint64_lor : forall x y:int [to_uint64 (lor x y)].
to_uint64 (lor x y) = lor (to_uint64 x) (to_uint64 y)
meta "remove_for_" lemma to_uint64_lor
(** * Some C-Integer Bits Conversions are identity *)
(** ** Unsigned conversions *)
lemma is_uint_lxor : forall n x y:int.
is_uint n x -> is_uint n y -> to_uint n (lxor x y) = lxor x y
lemma is_uint_lor : forall n x y:int.
is_uint n x -> is_uint n y -> to_uint n (lor x y) = lor x y
lemma is_uint_land : forall n x y:int.
is_uint n x -> is_uint n y -> to_uint n (land x y) = land x y
lemma is_uint_lsr : forall n x y:int.
0<=y -> is_uint n x -> to_uint n (lsr x y) = lsr x y
lemma is_uint_lsl1_inf : forall n y:int.
0<=y<n -> to_uint n (lsl 1 y) = lsl 1 y
lemma is_uint_lsl1_sup : forall n y:int.
0<=n<=y -> to_uint n (lsl 1 y) = 0
meta "remove_for_" lemma is_uint_lor
meta "remove_for_" lemma is_uint_land
meta "remove_for_" lemma is_uint_lsr
meta "remove_for_" lemma is_uint_lsl1_inf
meta "remove_for_" lemma is_uint_lsl1_sup
(** *** Cast to uint8 C type *)
axiom is_uint8_lxor : forall x y:int [to_uint8 (lxor x y)].
......@@ -473,29 +282,6 @@ theory Cbits
axiom is_uint64_lsl1_sup : forall y:int [to_uint64 (lsl 1 y)].
64<=y -> to_uint64 (lsl 1 y) = 0
(** ** Signed conversions *)
lemma is_sint_lnot: forall n x:int.
is_sint n x -> to_sint n (lnot x) = lnot x
lemma is_sint_lxor: forall n x y:int.
is_sint n x -> is_sint n y -> to_sint n (lxor x y) = lxor x y
lemma is_sint_lor: forall n x y:int.
is_sint n x -> is_sint n y -> to_sint n (lor x y) = lor x y
lemma is_sint_land: forall n x y:int.
is_sint n x -> is_sint n y -> to_sint n (land x y) = land x y
lemma is_sint_lsr: forall n x y:int.
0<=y -> is_sint n x -> to_sint n (lsr x y) = lsr x y
lemma is_sint_lsl1_inf : forall n y:int.
0<=y<n -> to_sint n (lsl 1 y) = (lsl 1 y)
lemma is_sint_lsl1_sup : forall n y:int.
0<=n<y -> to_sint n (lsl 1 y) = 0
meta "remove_for_" lemma is_sint_lnot
meta "remove_for_" lemma is_sint_lxor
meta "remove_for_" lemma is_sint_lor
meta "remove_for_" lemma is_sint_land
meta "remove_for_" lemma is_sint_lsr
meta "remove_for_" lemma is_sint_lsl1_inf
meta "remove_for_" lemma is_sint_lsl1_sup
(** *** Cast to sint8 C type *)
lemma is_sint8_lnot: forall x:int [to_sint8 (lnot x)].
is_sint8 x -> to_sint8 (lnot x) = lnot x
......@@ -596,27 +382,6 @@ theory Cbits
axiom is_sint64_lsl1_sup : forall y:int [to_sint64 (lsl 1 y)].
64<=y -> to_sint64 (lsl 1 y) = 0
(** * Range of some bitwise operations *)
lemma uint_land_range : forall x y: int .
0<=x -> 0 <= land x y <= x
meta "remove_for_" lemma uint_land_range
lemma uint_lor_inf : forall x y: int .
-1<=x -> 0<=y -> x <= lor x y
meta "remove_for_" lemma uint_lor_inf
lemma sint_land_inf : forall x y: int .
x<=0 -> y<0 -> land x y <= x
meta "remove_for_" lemma sint_land_inf
lemma sint_lor_range : forall x y: int .
x<0 -> x <= lor x y < 0
meta "remove_for_" lemma sint_lor_range
lemma is_uint_lor_distrib : forall n x y: int .
(is_uint n (lor x y)) <-> ((is_uint n x) && (is_uint n y))
meta "remove_for_" lemma is_uint_lor_distrib
(** * Link between bitwise operators and addition *)
axiom lor_addition : forall x y: int [(land x y), (lor x y) ].
land x y = 0 -> x + y = lor x y
......@@ -624,9 +389,4 @@ theory Cbits
axiom lxor_addition : forall x y: int [(land x y), (lxor x y) ].
land x y = 0 -> x + y = lxor x y
(** * Link between land and cast operator *)
lemma to_uint_land_edge : forall x n: int.
0<=n -> to_uint n x = land ((lsl 1 n) - 1) x
meta "remove_for_" lemma to_uint_land_edge
end
src/plugins/wp/share/why3/frama_c_wp/cint.mlw
+ 50
− 105
View file @ 8363a1f3
......@@ -44,28 +44,48 @@ theory Cint
(** * C-Integer Ranges * **)
predicate is_bool(x:int) = x = 0 \/ x = 1
predicate is_uint8(x:int) = 0 <= x < max_uint8
predicate is_sint8(x:int) = -max_sint8 <= x < max_sint8
predicate is_uint16(x:int) = 0 <= x < max_uint16
predicate is_sint16(x:int) = -max_sint16 <= x < max_sint16
predicate is_uint32(x:int) = 0 <= x < max_uint32
predicate is_sint32(x:int) = -max_sint32 <= x < max_sint32
predicate is_uint64(x:int) = 0 <= x < max_uint64
predicate is_sint64(x:int) = -max_sint64 <= x < max_sint64
lemma is_bool0: is_bool(0)
lemma is_bool1: is_bool(1)
(* meta "def_into_axiom" predicate is_bool *)
meta "def_into_axiom" predicate is_uint8
meta "def_into_axiom" predicate is_sint8
meta "def_into_axiom" predicate is_uint16
meta "def_into_axiom" predicate is_uint16
meta "def_into_axiom" predicate is_sint32
meta "def_into_axiom" predicate is_uint32
meta "def_into_axiom" predicate is_sint64
meta "def_into_axiom" predicate is_uint64
predicate is_bool (x:int) = x = 0 \/ x = 1
predicate is_uint8 int
axiom is_uint8_def :
forall x:int [is_uint8 x]. is_uint8 x <-> 0 <= x /\ x < max_uint8
predicate is_sint8 int
axiom is_sint8_def :
forall x:int [is_sint8 x]. is_sint8 x <-> (- max_sint8) <= x /\ x < max_sint8
predicate is_uint16 int
axiom is_uint16_def :
forall x:int [is_uint16 x]. is_uint16 x <-> 0 <= x /\ x < max_uint16
predicate is_sint16 (x:int) = (- max_sint16) <= x /\ x < max_sint16
predicate is_uint32 int
axiom is_uint32_def :
forall x:int [is_uint32 x]. is_uint32 x <-> 0 <= x /\ x < max_uint32
predicate is_sint32 int
axiom is_sint32_def :
forall x:int [is_sint32 x]. is_sint32 x <-> (- max_sint32) <= x /\ x < max_sint32
predicate is_uint64 int
axiom is_uint64_def :
forall x:int [is_uint64 x]. is_uint64 x <-> 0 <= x /\ x < max_uint64
predicate is_sint64 int
axiom is_sint64_def :
forall x:int [is_sint64 x]. is_sint64 x <-> (- max_sint64) <= x /\ x < max_sint64
lemma is_bool0 : is_bool 0
lemma is_bool1 : is_bool 1
(** * C-Integer Conversion * **)
......@@ -80,12 +100,6 @@ theory Cint
function to_sint64 int : int
function two_power_abs int : int
lemma two_power_abs_is_positive : forall n:int [ two_power_abs n ]. 0 < two_power_abs n
lemma two_power_abs_plus_pos : forall n m:int . 0 <= n -> 0 <= m -> two_power_abs (n+m) = (two_power_abs n) * (two_power_abs m)
lemma two_power_abs_plus_one : forall n:int . 0 <= n -> two_power_abs (n+1) = 2 * (two_power_abs n)
meta "remove_for_" lemma two_power_abs_is_positive
meta "remove_for_" lemma two_power_abs_plus_pos
meta "remove_for_" lemma two_power_abs_plus_one
predicate is_uint (n:int) (x:int) = 0 <= x < two_power_abs n
......@@ -97,11 +111,6 @@ theory Cint
(** * C-Integer Conversions are in-range * **)
lemma is_to_uint : forall n x:int [ is_uint n (to_uint n x) ]. is_uint n (to_uint n x)
lemma is_to_sint : forall n x:int [ is_sint n (to_sint n x) ]. is_sint n (to_sint n x)
meta "remove_for_" lemma is_to_uint
meta "remove_for_" lemma is_to_sint
axiom is_to_uint8 : forall x:int. is_uint8 (to_uint8 x)
axiom is_to_sint8 : forall x:int. is_sint8 (to_sint8 x)
axiom is_to_uint16 : forall x:int. is_uint16 (to_uint16 x)
......@@ -113,84 +122,20 @@ theory Cint
(** * C-Integer Conversions are identity when in-range * **)
lemma id_uint : forall n x:int [ to_uint n x ]. is_uint n x <-> (to_uint n x) = x
lemma id_sint : forall n x:int [ to_sint n x ]. is_sint n x <-> (to_sint n x) = x
meta "remove_for_" lemma id_uint
meta "remove_for_" lemma id_sint
axiom id_uint8 : forall x:int [ to_uint8 x ]. is_uint8 x -> (to_uint8 x) = x
axiom id_sint8 : forall x:int [ to_sint8 x ]. is_sint8 x -> (to_sint8 x) = x
axiom id_uint16 : forall x:int [ to_uint16 x ]. is_uint16 x -> (to_uint16 x) = x
axiom id_sint16 : forall x:int [ to_sint16 x ]. is_sint16 x -> (to_sint16 x) = x
axiom id_uint32 : forall x:int [ to_uint32 x ]. is_uint32 x -> (to_uint32 x) = x
axiom id_sint32 : forall x:int [ to_sint32 x ]. is_sint32 x -> (to_sint32 x) = x
axiom id_uint64 : forall x:int [ to_uint64 x ]. is_uint64 x -> (to_uint64 x) = x
axiom id_sint64 : forall x:int [ to_sint64 x ]. is_sint64 x -> (to_sint64 x) = x
meta "inline_in" predicate is_uint8, axiom id_uint8
meta "inline_in" predicate is_sint8, axiom id_sint8
meta "inline_in" predicate is_uint16, axiom id_uint16
meta "inline_in" predicate is_sint16, axiom id_sint16
meta "inline_in" predicate is_uint32, axiom id_uint32
meta "inline_in" predicate is_sint32, axiom id_sint32
meta "inline_in" predicate is_uint64, axiom id_uint64
meta "inline_in" predicate is_sint64, axiom id_sint64
(** * C-Integer Conversions are projections * **)
lemma proj_uint : forall n x:int . to_uint n (to_uint n x)= to_uint n x
lemma proj_sint : forall n x:int . to_sint n (to_sint n x)= to_sint n x
meta "remove_for_" lemma proj_uint
meta "remove_for_" lemma proj_sint
axiom proj_uint8 : forall x:int [ to_uint8(to_uint8 x) ]. to_uint8(to_uint8 x)=to_uint8 x
axiom proj_sint8 : forall x:int [ to_sint8(to_sint8 x) ]. to_sint8(to_sint8 x)=to_sint8 x
axiom proj_uint16 : forall x:int [ to_uint16(to_uint16 x) ]. to_uint16(to_uint16 x)=to_uint16 x
axiom proj_sint16 : forall x:int [ to_sint16(to_sint16 x) ]. to_sint16(to_sint16 x)=to_sint16 x
axiom proj_uint32 : forall x:int [ to_uint32(to_uint32 x) ]. to_uint32(to_uint32 x)=to_uint32 x
axiom proj_sint32 : forall x:int [ to_sint32(to_sint32 x) ]. to_sint32(to_sint32 x)=to_sint32 x
axiom proj_uint64 : forall x:int [ to_uint64(to_uint64 x) ]. to_uint64(to_uint64 x)=to_uint64 x
axiom proj_sint64 : forall x:int [ to_sint64(to_sint64 x) ]. to_sint64(to_sint64 x)=to_sint64 x
meta "remove_for_" axiom proj_uint8
meta "remove_for_" axiom proj_sint8
meta "remove_for_" axiom proj_uint16
meta "remove_for_" axiom proj_sint16
meta "remove_for_" axiom proj_uint32
meta "remove_for_" axiom proj_sint32
meta "remove_for_" axiom proj_uint64
meta "remove_for_" axiom proj_sint64
axiom id_uint8 : forall x:int [ to_uint8 x ]. 0 <= x < max_uint8 -> (to_uint8 x) = x
axiom id_sint8 : forall x:int [ to_sint8 x ]. -max_sint8 <= x < max_sint8 -> (to_sint8 x) = x
axiom id_uint16 : forall x:int [ to_uint16 x ]. 0 <= x < max_uint16 -> (to_uint16 x) = x
axiom id_sint16 : forall x:int [ to_sint16 x ]. -max_sint16 <= x < max_sint16 -> (to_sint16 x) = x
axiom id_uint32 : forall x:int [ to_uint32 x ]. 0 <= x < max_uint32 -> (to_uint32 x) = x
axiom id_sint32 : forall x:int [ to_sint32 x ]. -max_sint32 <= x < max_sint32 -> (to_sint32 x) = x
axiom id_uint64 : forall x:int [ to_uint64 x ]. 0 <= x < max_uint64 -> (to_uint64 x) = x
axiom id_sint64 : forall x:int [ to_sint64 x ]. -max_sint64 <= x < max_sint64 -> (to_sint64 x) = x
(** * Generalization for [to_sint _ (to_uint _ x)] * **)
lemma proj_su: forall n x:int . to_sint n (to_uint n x) = to_uint n x
lemma incl_su: forall n x:int . is_uint n x -> is_sint n x
meta "remove_for_" lemma proj_su
meta "remove_for_" lemma incl_su
lemma proj_su_uint: forall n m x:int . 0 <= n -> 0 <= m -> to_sint (m+n) (to_uint n x) = to_uint n x
lemma proj_su_sint: forall n m x:int . 0 <= n -> 0 <= m -> to_sint n (to_uint (m+(n+1)) x) = to_sint n x
meta "remove_for_" lemma proj_su_uint
meta "remove_for_" lemma proj_su_sint
axiom proj_int8 : forall x:int [ to_sint8(to_uint8 x) ]. to_sint8(to_uint8 x) =to_sint8 x
axiom proj_int16 : forall x:int [ to_sint16(to_uint16 x) ]. to_sint16(to_uint16 x)=to_sint16 x
axiom proj_int32 : forall x:int [ to_sint32(to_uint32 x) ]. to_sint32(to_uint32 x)=to_sint32 x
axiom proj_int64 : forall x:int [ to_sint64(to_uint64 x) ]. to_sint64(to_uint64 x)=to_sint64 x
(** * Generalization for [to_uint _ (to_sint _ x)] * **)
lemma proj_us_uint: forall n m x:int . 0 <= n -> 0 <= m -> to_uint (n+1) (to_sint (m+n) x) = to_uint (n+1) x
meta "remove_for_" lemma proj_us_uint
(** * C-Integer range inclusion * **)
lemma incl_uint : forall n x i:int . 0 <= n -> 0 <= i -> is_uint n x -> is_uint (n+i) x
lemma incl_sint : forall n x i:int . 0 <= n -> 0 <= i -> is_sint n x -> is_sint (n+i) x
lemma incl_int : forall n x i:int . 0 <= n -> 0 <= i -> is_uint n x -> is_sint (n+i) x
meta "remove_for_" lemma incl_uint
meta "remove_for_" lemma incl_sint
meta "remove_for_" lemma incl_int
end
src/plugins/wp/share/why3/frama_c_wp/qed.mlw
+ 0
− 3
View file @ 8363a1f3
......@@ -34,9 +34,6 @@ theory Qed
function eqb (x y : 'a) : bool (*= if x = y then True else False*)
axiom eqb : forall x:'a, y:'a. eqb x y = True <-> x = y
axiom eqb_false : forall x:'a, y:'a. eqb x y = False <-> x <> y
meta "remove_for_" axiom eqb_false
function neqb (x y : 'a) : bool(* = if x <> y then True else False*)
axiom neqb : forall x:'a, y:'a. neqb x y = True <-> x <> y
......
src/plugins/wp/wp.ml
+ 0
− 1
View file @ 8363a1f3
......@@ -170,7 +170,6 @@ module Filtering = Filtering
(** {2 Prover Interface} *)
module Why3Provers = Why3Provers
module Filter_axioms = Filter_axioms
module Prover = Prover
module ProverTask = ProverTask
module ProverWhy3 = ProverWhy3
......
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