Commit 24f77deb authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] linting files

parent 4d6b7476
......@@ -73,17 +73,17 @@ let real = Str.regexp (mantissa ^ comma ^ exponent ^ "$")
let parse_literal v r =
try
if Str.string_match real r 0 then
let ma = Str.matched_group 1 r in
let mb = try Str.matched_group 3 r with Not_found -> "" in
let me = try Str.matched_group 6 r with Not_found -> "0" in
let n = int_of_string me - String.length mb in
let d n =
let s = Bytes.make (succ n) '0' in
Bytes.set s 0 '1' ; Q.of_string (Bytes.to_string s) in
let m = Q.of_string (ma ^ mb) in
if n < 0 then Q.div m (d (-n)) else
if n > 0 then Q.mul m (d n) else m
if Str.string_match real r 0 then
let ma = Str.matched_group 1 r in
let mb = try Str.matched_group 3 r with Not_found -> "" in
let me = try Str.matched_group 6 r with Not_found -> "0" in
let n = int_of_string me - String.length mb in
let d n =
let s = Bytes.make (succ n) '0' in
Bytes.set s 0 '1' ; Q.of_string (Bytes.to_string s) in
let m = Q.of_string (ma ^ mb) in
if n < 0 then Q.div m (d (-n)) else
if n > 0 then Q.mul m (d n) else m
else Q.of_float v
with Failure _ ->
Warning.error ~source:"acsl" "Unexpected real literal %S" r
......@@ -195,9 +195,9 @@ let builtin_error = function
(* -------------------------------------------------------------------------- *)
let float_of_real f a =
match Context.get model with
| Real -> a
| Float -> e_fun (flt_rnd f) [a]
match Context.get model with
| Real -> a
| Float -> e_fun (flt_rnd f) [a]
let float_of_int f a = float_of_real f (Cmath.real_of_int a)
let real_of_float _f a = a
......
......@@ -48,15 +48,15 @@ struct
F.is_primitive e ||
begin
try Tmap.find e env.ground with Not_found ->
let r = match F.repr e with
| Rdef fvs -> List.for_all (fun (_,e) -> is_ground env e) fvs
| Fun(f,es) ->
begin match Fun.category f with
| Constructor -> List.for_all (is_ground env) es
| _ -> false
end
| _ -> false in
env.ground <- Tmap.add e r env.ground ; r
let r = match F.repr e with
| Rdef fvs -> List.for_all (fun (_,e) -> is_ground env e) fvs
| Fun(f,es) ->
begin match Fun.category f with
| Constructor -> List.for_all (is_ground env) es
| _ -> false
end
| _ -> false in
env.ground <- Tmap.add e r env.ground ; r
end
let merge a b =
......@@ -75,7 +75,7 @@ struct
| Model { m_category = Injection } -> 1
| Model { m_category = Operator _ } -> 2
| Model { m_category = Constructor } -> 3
let add_reduce env a b =
env.domain <- Tmap.add a b env.domain
......@@ -83,18 +83,18 @@ struct
if F.is_subterm a b then add_reduce env b a else
if F.is_subterm b a then add_reduce env a b else
begin
match F.repr a , F.repr b with
| Fun(f,_) , Fun(g,_) when Wp_parameters.Reduce.get () ->
let cmp = frank f - frank g in
match F.repr a , F.repr b with
| Fun(f,_) , Fun(g,_) when Wp_parameters.Reduce.get () ->
let cmp = frank f - frank g in
if cmp < 0 then add_reduce env a b else
if cmp > 0 then add_reduce env b a
| Fun(f,_) , _ when frank f = 0 ->
| Fun(f,_) , _ when frank f = 0 ->
add_reduce env a b
| _ , Fun(f,_) when frank f = 0 ->
| _ , Fun(f,_) when frank f = 0 ->
add_reduce env b a
| _ -> ()
| _ -> ()
end
let rec walk env h =
match F.repr h with
| True | False -> ()
......@@ -128,7 +128,7 @@ struct
let e_apply env =
let sigma = F.sigma () in
F.e_subst ~sigma (lookup env.domain)
let p_apply env =
let sigma = F.sigma () in
F.p_subst ~sigma (lookup env.domain)
......@@ -145,12 +145,12 @@ struct
[@@@ warning "+32"]
let pretty fmt env = pp_sigma fmt env.domain
let assume env p =
let p = F.p_subst (lookup env.domain) p in
walk env (F.e_prop p) ; p
let top () = { ground = Tmap.empty ; domain = Tmap.empty }
let top () = { ground = Tmap.empty ; domain = Tmap.empty }
let copy env = { domain = env.domain ; ground = env.ground }
let compute seq =
......@@ -200,7 +200,7 @@ struct
match F.p_expr p with
| And ps -> F.p_all (assume env) (List.rev ps)
| _ -> assume env p
end
(* -------------------------------------------------------------------------- *)
......@@ -402,7 +402,7 @@ struct
end
let is_kint e = match F.repr e with Qed.Logic.Kint _ -> true | _ -> false
let rec add_pred sigma p = match F.repr p with
| And ps -> List.fold_left add_pred sigma ps
| Eq(a,b) ->
......
......@@ -265,7 +265,7 @@ let is_separated args = F.is_true (r_separated args)
logic a : int
logic b : int
predicate R = p.base = q.base
predicate R = p.base = q.base
/\ (q.offset <= p.offset)
/\ (p.offset + a <= q.offset + b)
......@@ -368,19 +368,19 @@ let phi_addr_of_int p =
(* -------------------------------------------------------------------------- *)
let () = Context.register
begin fun () ->
F.set_builtin_1 f_base phi_base ;
F.set_builtin_1 f_offset phi_offset ;
F.set_builtin_2 f_shift (phi_shift f_shift) ;
F.set_builtin_eqp f_shift eq_shift ;
F.set_builtin_eqp f_global eq_shift ;
F.set_builtin p_separated r_separated ;
F.set_builtin p_included r_included ;
F.set_builtin f_havoc r_havoc ;
F.set_builtin_get f_havoc r_get_havoc ;
F.set_builtin_1 a_addr_of_int phi_addr_of_int ;
F.set_builtin_1 a_int_of_addr phi_int_of_addr ;
end
begin fun () ->
F.set_builtin_1 f_base phi_base ;
F.set_builtin_1 f_offset phi_offset ;
F.set_builtin_2 f_shift (phi_shift f_shift) ;
F.set_builtin_eqp f_shift eq_shift ;
F.set_builtin_eqp f_global eq_shift ;
F.set_builtin p_separated r_separated ;
F.set_builtin p_included r_included ;
F.set_builtin f_havoc r_havoc ;
F.set_builtin_get f_havoc r_get_havoc ;
F.set_builtin_1 a_addr_of_int phi_addr_of_int ;
F.set_builtin_1 a_int_of_addr phi_int_of_addr ;
end
(* -------------------------------------------------------------------------- *)
(* --- Model Parameters --- *)
......@@ -707,7 +707,7 @@ module STRING = Model.Generator(LITERAL)
let fresh () =
let eid = succ (EID.get ()) in
EID.set eid ; eid
let compile (_,cst) =
let eid = fresh () in
let lfun = Lang.generated_f ~result:L.Int "Str_%d" eid in
......@@ -875,7 +875,7 @@ struct
[Trigger.of_pred eqmem ; Trigger.of_term phi ] ;
[Trigger.of_pred eqmem ; Trigger.of_term phi'] ;
] ;
l_forall = F.p_vars lemma ;
l_forall = F.p_vars lemma ;
l_lemma = lemma ;
l_cluster = cluster_memory () ;
}
......@@ -1274,7 +1274,7 @@ let stored s obj l v =
| C_float _ -> updated s M_float l v
| C_pointer _ -> updated s M_pointer l v
| C_comp _ | C_array _ ->
Set(loadvalue s.post obj l, v) ::
Set(loadvalue s.post obj l, v) ::
(List.map (fun p -> Assert p) (havoc s obj l))
let copied s obj p q = stored s obj p (loadvalue s.pre obj q)
......@@ -1288,7 +1288,7 @@ let assigned_loc s obj l =
| C_int _ | C_float _ | C_pointer _ ->
let x = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
List.map Cvalues.equation (stored s obj l (e_var x))
| C_comp _ | C_array _ ->
| C_comp _ | C_array _ ->
havoc s obj l
let equal_loc s obj l =
......@@ -1462,7 +1462,7 @@ and lookup_f f es =
| RS_Field(fd,_) , [e] -> Mstate.field (lookup_lv e) fd
| RS_Shift _ , [e;k] -> Mstate.index (lookup_lv e) k
| _ -> raise Not_found
with Not_found when es = [] ->
with Not_found when es = [] ->
Sigs.(Mvar (RegisterBASE.find f),[])
and lookup_lv e = try lookup_a e with Not_found -> Sigs.(Mmem e,[])
......
......@@ -105,7 +105,7 @@ let register ~id ?(descr=id) ?(tuning=[]) ?(hypotheses=nohyp) () =
let get_id m = m.id
let get_descr m = m.descr
let get_hypotheses m = m.hypotheses
type scope = Kernel_function.t option
let scope : scope Context.value = Context.create "Wp.Scope"
let model : model Context.value = Context.create "Wp.Model"
......@@ -232,7 +232,7 @@ struct
e.index <- MAP.remove k e.index ;
e.lock <- SET.remove k e.lock ;
end
let mem k = let e = entries () in MAP.mem k e.index || SET.mem k e.lock
let find k = let e = entries () in MAP.find k e.index
......@@ -338,7 +338,7 @@ struct
e.index <- MAP.remove k e.index ;
e.lock <- SET.remove k e.lock ;
end
let mem k = let e = entries () in MAP.mem k e.index || SET.mem k e.lock
let find k = let e = entries () in MAP.find k e.index
......@@ -366,7 +366,7 @@ struct
e.index <- MAP.add k d e.index ;
fire k d ;
end
let memoize f k =
let e = entries () in
try MAP.find k e.index
......
......@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
open Format
open Format
open Qed.Logic
open Qed.Engine
open Lang
......@@ -37,7 +37,7 @@ type pool = {
let pool () = { vars = Vars.empty ; mark = Tset.empty }
let alloc_domain p = p.vars
let rec walk p f e =
if not (Tset.mem e p.mark) &&
not (Vars.subset (F.vars e) p.vars)
......@@ -75,7 +75,7 @@ class engine =
inherit E.engine as super
inherit Lang.idprinting
method infoprover w = w.altergo
val mutable iformat : iformat = `Dec
method get_iformat = iformat
method set_iformat (f : iformat) = iformat <- f
......@@ -97,7 +97,7 @@ class engine =
fprintf fmt "@[<hov 2>%a[%a]@]" self#pp_subtau t self#pp_tau k
method pp_datatype a fmt ts =
Qed.Plib.pp_call_var ~f:(self#datatype a) self#pp_tau fmt ts
(* --- Primitives --- *)
method e_true _ = "true"
......@@ -128,9 +128,9 @@ class engine =
Format.fprintf fmt "%s.0" (Z.to_string num)
else
Format.fprintf fmt "(%s.0/%s)" (Z.to_string num) (Z.to_string den)
(* --- Atomicity --- *)
method callstyle = CallVar
method is_atomic e =
match F.repr e with
......@@ -139,7 +139,7 @@ class engine =
| Apply _ -> true
| Aset _ | Aget _ | Fun _ -> true
| _ -> F.is_simple e
(* --- Operators --- *)
method op_spaced = Qed.Export.is_identifier
......@@ -172,7 +172,7 @@ class engine =
fprintf fmt "@ else %a" self#pp_atom pelse ;
fprintf fmt "@]" ;
end
(* --- Arrays --- *)
method pp_array_cst fmt (_ : F.tau) v =
......@@ -189,7 +189,7 @@ class engine =
method pp_get_field fmt a fd =
Format.fprintf fmt "%a.%s" self#pp_atom a (self#field fd)
method pp_def_fields fmt fvs =
let base,fvs = match F.record_with fvs with
| None -> None,fvs | Some(r,fvs) -> Some r,fvs in
......@@ -225,7 +225,7 @@ class engine =
method pp_apply (_:cmode) (_:term) (_:formatter) (_:term list) =
failwith "Qed: higher-order application"
method pp_lambda (_:formatter) (_: (string * tau) list) =
failwith "Qed: lambda abstraction"
......@@ -253,5 +253,5 @@ class engine =
(* --- Predicates --- *)
method pp_pred fmt p = self#pp_prop fmt (F.e_prop p)
end
......@@ -118,7 +118,7 @@ struct
mutable backtrack : int ;
mutable backtracking : backtracking option ;
}
and backtracking = {
bk_node : ProofEngine.node ;
bk_depth : int ; (* depth of search *)
......@@ -181,7 +181,7 @@ struct
bk_depth = depth ;
bk_pending = pending env ;
}
let search env node ~depth =
if env.auto <> [] && depth < env.depth && pending env < env.width
then
......@@ -211,7 +211,7 @@ struct
with None -> None | Some fork -> Some (point.bk_depth,fork)
let provers env = env.provers
let make tree
~valid ~failed ~provers
~depth ~width ~backtrack ~auto
......@@ -246,11 +246,11 @@ let reconcile nodes scripts =
| [] , [] -> ()
| [_,n] , [_,s] -> ProofEngine.bind n s
| _ ->
if List.for_all (fun (k,_) -> k = "") scripts
then zip fst_order nodes scripts
else zip key_order
(List.stable_sort key_order nodes)
(List.stable_sort key_order scripts)
if List.for_all (fun (k,_) -> k = "") scripts
then zip fst_order nodes scripts
else zip key_order
(List.stable_sort key_order nodes)
(List.stable_sort key_order scripts)
let rec forall phi = function
| x::xs ->
......@@ -277,35 +277,35 @@ let prove_node env node prv =
let rec auto env ?(depth=0) node : bool Task.task =
exists (prove_node env node) (Env.provers env) >>= fun ok ->
if ok then Task.return true else
if depth > 0 then
autosearch env ~depth node
else
begin
autosearch env ~depth node >>= fun ok ->
if ok then Task.return true else
match Env.backtrack env with
| Some (depth,fork) ->
Env.progress env "Backtracking" ;
autofork env ~depth fork
| None ->
Task.return false
end
if depth > 0 then
autosearch env ~depth node
else
begin
autosearch env ~depth node >>= fun ok ->
if ok then Task.return true else
match Env.backtrack env with
| Some (depth,fork) ->
Env.progress env "Backtracking" ;
autofork env ~depth fork
| None ->
Task.return false
end
and autosearch env ~depth node : bool Task.task =
match Env.search env node ~depth with
| None -> Task.return false
| None -> Task.return false
| Some fork -> autofork env ~depth fork
and autofork env ~depth fork =
let _,children = ProofEngine.commit ~resolve:true fork in
let pending = Env.pending env in
if pending > 0 then
begin
Env.progress env (Printf.sprintf "Auto %d" pending) ;
let depth = succ depth in
forall (auto env ~depth) (List.map snd children)
end
else
let _,children = ProofEngine.commit ~resolve:true fork in
let pending = Env.pending env in
if pending > 0 then
begin
Env.progress env (Printf.sprintf "Auto %d" pending) ;
let depth = succ depth in
forall (auto env ~depth) (List.map snd children)
end
else
( Env.validate env ; Task.return true )
(* -------------------------------------------------------------------------- *)
......@@ -313,13 +313,13 @@ and autofork env ~depth fork =
(* -------------------------------------------------------------------------- *)
let rec crawl env on_child node = function
| [] ->
let node = ProofEngine.anchor (Env.tree env) ?node () in
auto env node >>= fun ok ->
if ok then Env.validate env else Env.stuck env ;
Task.return ()
| Error(msg,json) :: alternative ->
Wp_parameters.error "@[<hov 2>Script Error %S: %a@]@." msg Json.pp json ;
crawl env on_child node alternative
......@@ -461,7 +461,7 @@ let has_proof wpo =
try Hashtbl.find proofs wid
with Not_found ->
if ProofSession.exists wpo then
let ok =
let ok =
try
let script = ProofScript.decode (ProofSession.load wpo) in
ProofScript.status script = 0
......
......@@ -80,7 +80,7 @@ struct
let flow =
List.fold_left (fun flow (l, n) -> LabelMap.add l n flow) env.flow lns
in { env with flow }
let (@:) env lbl =
try
LabelMap.find lbl env.flow
......@@ -103,7 +103,7 @@ struct
(* -------------------------------------------------------------------------- *)
(* --- Paths & Cfg Utilities --- *)
(* -------------------------------------------------------------------------- *)
let paths_of_cfg cfg = {
paths_cfg = cfg;
paths_goals = Bag.empty;
......@@ -140,9 +140,9 @@ struct
| [] -> goto (env @: Clabels.here) (env @: Clabels.next)
| [ elt ] -> f env elt
| stmt :: stmts ->
let n = Cfg.node () in
let paths = f (bind Clabels.next n env) stmt in
paths @^ (sequence f (bind Clabels.here n env) stmts)
let n = Cfg.node () in
let paths = f (bind Clabels.next n env) stmt in
paths @^ (sequence f (bind Clabels.here n env) stmts)
let choice ?(pre=Clabels.here) ?(post=Clabels.next) f env =
let pre_node = env @: pre in
......@@ -152,11 +152,11 @@ struct
let rec aux env ns = function
| [] -> goto (env @: pre) (env @: post)
| [ elt ] ->
let n, paths = apply f env elt in
paths @^ either pre_node (n :: ns)
let n, paths = apply f env elt in
paths @^ either pre_node (n :: ns)
| elt :: elts ->
let n, paths = apply f env elt in
paths @^ (aux env (n :: ns) elts)
let n, paths = apply f env elt in
paths @^ (aux env (n :: ns) elts)
in
aux env []
......@@ -169,11 +169,11 @@ struct
let rec aux env ns = function
| [] -> goto (env @: pre) (env @: post)
| [ elt ] ->
let n, (c,paths) = apply f env elt in
paths @^ implies pre_node ((c,n) :: ns)
let n, (c,paths) = apply f env elt in
paths @^ implies pre_node ((c,n) :: ns)
| elt :: elts ->
let n, (c,paths) = apply f env elt in
paths @^ (aux env ((c,n) :: ns) elts)
let n, (c,paths) = apply f env elt in
paths @^ (aux env ((c,n) :: ns) elts)
in
aux env []
......@@ -455,7 +455,7 @@ struct
(** TODO: Kglobal is it always Kglobal ? *)
let prop_id = WpPropId.mk_pre_id env.kf Kglobal b ip in
pre_cond env ip prop_id)
(env @* [Clabels.next, nrequires]) b.b_requires
(env @* [Clabels.next, nrequires]) b.b_requires
@^ assigns (env @* [Clabels.here, nrequires; Clabels.next, nassigns]) b.b_assigns
@^ either nassigns [post_normal_behavior;post_at_exit_behavior]
@^ List.fold_left
......@@ -517,39 +517,39 @@ struct
let transition
: env -> nodes -> Automata.t Interpreted_automata.transition -> paths
= fun env nodes tr ->
let open Interpreted_automata in
match tr with
| Skip | Enter { blocals = [] } | Leave { blocals = [] } ->
goto (env @: Clabels.here) (env @: Clabels.next)
| Enter {blocals} -> scope env Sigs.Enter blocals
| Leave {blocals} -> scope env Sigs.Leave blocals
| Return (r,_) -> return env r
let open Interpreted_automata in
match tr with
| Skip | Enter { blocals = [] } | Leave { blocals = [] } ->
goto (env @: Clabels.here) (env @: Clabels.next)
| Enter {blocals} -> scope env Sigs.Enter blocals
| Leave {blocals} -> scope env Sigs.Leave blocals
| Return (r,_) -> return env r
| Prop ({kind = Assert|Invariant} as a, _) ->
let env = Logic_label.Map.fold
(fun logic_label vertex acc ->
let c_label = Clabels.of_logic logic_label in
let node = get_node nodes vertex in
bind c_label node acc
let env = Logic_label.Map.fold
(fun logic_label vertex acc ->
let c_label = Clabels.of_logic logic_label in
let node = get_node nodes vertex in
bind c_label node acc
) a.labels env in
assert_ env a.predicate (WpPropId.mk_property a.property)
| Prop ({kind = Assume} as a, _)->
let env = Logic_label.Map.fold
(fun logic_label vertex acc ->
let c_label = Clabels.of_logic logic_label in
let node = get_node nodes vertex in
bind c_label node acc
let env = Logic_label.Map.fold
(fun logic_label vertex acc ->
let c_label = Clabels.of_logic logic_label in
let node = get_node nodes vertex in
bind c_label node acc
) a.labels env in
assume (pred env `Negative a.predicate.ip_content) @^
goto (env @: Clabels.here) (env @: Clabels.next)
goto (env @: Clabels.here) (env @: Clabels.next)
| Prop _ ->
not_yet "[StmtSemantics] Annots other than 'assert'"
| Guard (exp,b,_) ->
let here = Sigma.create () in
let cond = C.cond here exp in
let condition = Cfg.C.create here cond in
(if b = Then then guard else guard')
(env @: Clabels.here) condition (env @: Clabels.next)
| Instr (i,_) -> instr env i
not_yet "[StmtSemantics] Annots other than 'assert'"
| Guard (exp,b,_) ->
let here = Sigma.create () in
let cond = C.cond here exp in