Commit f91bb58b authored by DAILLER Sylvain's avatar DAILLER Sylvain Committed by MARCHE Claude

Generalization of check_unused_vars to logic and program decl

Description:
- Choice was made to not add unused variables when there is no contract
  and no body (no pre/(x)post, and no body).
- For postcondition variable result, we only check variables that are not
  of unit type. And, we report a warning only if the variable is not present
  in all the ensures.
- For result variable, with several imbricated raise, it seems possible to
  have false positive with no location. Removing the no location case which
  seems unhelpful anyway
parent e0a8f060
......@@ -6,17 +6,17 @@ module Test
type t
function d (x : t) : int
meta "model_projection" function d
function c (x : t) : int
meta "model_projection" function c
(* Here the counterexample should not be a record *)
let f (x: t) : t
let f (x: t) : (_t: t)
requires { c x > 0 }
ensures { d x < 0 }
ensures { d x < 0 }
=
x
end
......@@ -6,13 +6,13 @@ use ref.Ref
val x : ref int
let f (a : int) : int
let f (_a : int) : int
ensures { result = 0}
=
x := 42;
!x
let f2 (a : int) : int
let f2 (_a : int) : int
ensures { result = 0}
=
x := 42;
......
use int.Int
(* Should not output any unused variable *)
val v (x : int) (y : int) : bool
ensures {x = y <-> result}
ensures {x = y}
use int.Int
exception E
exception F
exception G
exception H int
val f (x y z: int) : int
ensures { x = 42 }
ensures { result = 43 }
ensures { x = 45 }
raises { F -> x = -42 }
raises { E -> x <> x }
raises { G -> x = z }
raises { H res -> y = 42 }
......@@ -3,9 +3,8 @@ exception Exception
val f0 (tt:unit) : unit
val f1 (tt:unit) : unit raises { Exception }
val f1 (_tt:unit) : unit raises { Exception }
let f ()
raises { Exception -> true }
= f0 (f1 ())
......@@ -5,7 +5,6 @@ use ref.Ref
val t : ref int
val m (a:int) (b:int) : unit raises { Exception }
val m (_a:int) (_b:int) : unit raises { Exception }
let test () raises { Exception } = (m ( assert { true } ; 0) 0)
......@@ -7,7 +7,7 @@ use ref.Ref
val i : ref int
let loop1 (u:unit) requires { !i <= 10 } ensures { !i = 10 }
let loop1 (_u:unit) requires { !i <= 10 } ensures { !i = 10 }
= while !i < 10 do
invariant { !i <= 10 } variant { 10 - !i }
i := !i + 1
......@@ -18,9 +18,9 @@ let loop1 (u:unit) requires { !i <= 10 } ensures { !i = 10 }
val x: ref int
let negate (u:unit) ensures { !x = - (old !x) } = x := - !x
let negate (_u:unit) ensures { !x = - (old !x) } = x := - !x
let loop2 (u:unit) requires { !x <= 10 }
let loop2 (_u:unit) requires { !x <= 10 }
= begin
while !x < 10 do invariant { !x <= 10 } variant { 10 - !x }
x := !x + 1
......@@ -31,4 +31,3 @@ let loop2 (u:unit) requires { !x <= 10 }
end
end
......@@ -6,7 +6,7 @@ module T
(* g can raise MyExc *)
let rec f (x: int) : int raises {MyExc} = raise MyExc
with g (x: int) : int raises {MyExc} = f x
let rec f (_x: int) : int raises {MyExc} = raise MyExc
with g (x : int) : int raises {MyExc} = f x
end
......@@ -15,7 +15,7 @@ module M
val x : ref int
let rec f2 (u:unit) : unit variant { !x }
let rec f2 (_u:unit) : unit variant { !x }
requires { !x >= 0 } ensures { !x = 0 }
= if !x > 0 then begin x := !x - 1; f2 () end
......@@ -42,4 +42,3 @@ module M
= let b = ref 0 in let f = f5 x in f b
end
use int.Int
(* result unused *)
val eq (x: int) (y: int) : bool
ensures { x = y }
use int.Int
(* z unused *)
function f (x : int) (y : int) : bool = forall z:int. x = y
use int.Int
(* y unused *)
function g (x: int) (y: int) : bool = forall z:int. x = z
use int.Int
(* result unused *)
let eq1 (x : int) (y : int) : bool
ensures { x = y }
= true
use int.Int
(* y unused *)
let eq2 (x: int) (y : int) : bool
ensures { result <-> (x = x) }
= true
use int.Int
(* y is unused *)
goal h : forall y x: int. x = 42
use int.Int
(* x is unused *)
predicate p (x: int) (y: int) = y = 0
use int.Int
exception E
exception F
exception G
exception H
val f (x: int) : int
ensures { x = 42 }
raises { F -> x = -42 }
raises { E -> x <> x }
raises { G -> x = x }
raises { H -> false }
......@@ -14,7 +14,7 @@ module M
| Some b ->
if b then
(
let rec aux (x: unit) : unit
let rec aux (_x: unit) : unit
diverges
raises { A -> true }
=
......
......@@ -48,7 +48,7 @@ module ARM
(* memory *)
val mem : ref (map int int)
val mem_ldr (a:int) : int ensures { result = !mem[a] }
val mem_str (a:int) (v:int) : int writes { mem }
val mem_str (a:int) (v:int) : (_r: int) writes { mem }
ensures { !mem = (old !mem)[a <- v] }
(* data segment *)
......
......@@ -34,7 +34,7 @@ module MapBase
scope M
type t = unit
constant zero : unit = ()
function op (x y:unit) : unit = ()
function op (_x _y:unit) : unit = ()
let lemma neutral_ (x:unit) : unit
ensures { op zero x = x = op x zero }
= match x with _ -> () end
......@@ -43,7 +43,7 @@ module MapBase
clone export monoid.MonoidSumDef with type M.t = t,
constant M.zero = zero,function M.op = op,goal M.assoc,goal M.neutral
let zero () : unit ensures { result = () } = ()
let op (x y:unit) : unit ensures { result = () } = ()
let op (_x _y:unit) : unit ensures { result = () } = ()
end
(** In associative tables, elements are selected
......@@ -74,7 +74,7 @@ module MapBase
(** Comparison-based binary search *)
let selected_part (ghost lseq rseq:seq (D.t 'a))
(k:K.t) (l:'e) (d:D.t 'a) (r:'f) : part_base K.t
(k:K.t) (_l:'e) (d:D.t 'a) (_r:'f) : part_base K.t
requires { selection_possible k (lseq ++ cons d rseq) }
returns { Here -> let e2 = { left = lseq;
middle = Some d;
......@@ -937,4 +937,3 @@ module IMapAndSet
val CO.compare = compare
end
......@@ -119,7 +119,7 @@ theory Graph
requires { path s l v /\ path_weight l v < n }
(* then there exists a negative cycle. *)
ensures { exists u. negative_cycle u }
= let rec aux (m: int) : 'a
= let rec aux (m: int) : (_a: 'a)
requires { forall u. not negative_cycle u }
requires { exists l. path s l v /\ path_weight l v < n /\ length l <= m }
ensures { false }
......
......@@ -13,7 +13,7 @@ use int.Int
exception MyExc
let rec f (x:int) : int variant { 0 } raises { MyExc } = raise MyExc
let rec f (_x:int) : int variant { 0 } raises { MyExc } = raise MyExc
with g (x:int) : int variant { 1 } raises { MyExc } = f x
end
......@@ -13,7 +13,7 @@ module T
exception MyExc
let rec f (a:t) : t raises { MyExc } = raise MyExc
let rec f (_a:t) : t raises { MyExc } = raise MyExc
with g (a:t) : t = try (f a) with MyExc -> a end
end
......@@ -14,7 +14,7 @@ module T
exception MyExc
let rec f (x:t) : t raises { MyExc } = raise MyExc
with g (x:t) : t raises { MyExc } ensures { true } = f x
let rec f (_x:t) : t raises { MyExc } = raise MyExc
with g (x:t) : (_r: t) raises { MyExc } ensures { true } = f x
end
......@@ -22,7 +22,7 @@ module DijkstraShortestPath
constant v: fset vertex
val ghost function g_succ (x: vertex) : fset vertex
val ghost function g_succ (_x: vertex) : fset vertex
ensures { subset result v }
val get_succs (x: vertex): set
......@@ -151,13 +151,13 @@ module DijkstraShortestPath
(* there are paths for vertices in Q *)
(forall v: vertex. mem v q -> path src v d[v])
predicate inv_succ (src: vertex) (s q: set) (d: t int) =
predicate inv_succ (_src: vertex) (s q: set) (d: t int) =
(* successors of vertices in S are either in S or in Q *)
forall x: vertex. mem x s ->
forall y: vertex. mem y (g_succ x) ->
(mem y s \/ mem y q) /\ d[y] <= d[x] + weight x y
predicate inv_succ2 (src: vertex) (s q: set) (d: t int) (u: vertex) (su: set) =
predicate inv_succ2 (_src: vertex) (s q: set) (d: t int) (u: vertex) (su: set) =
(* successors of vertices in S are either in S or in Q,
unless they are successors of u still in su *)
forall x: vertex. mem x s ->
......
......@@ -170,7 +170,7 @@ module FulcrumNoOverflow
meta coercion function v
predicate biginv (b: big) = 89>55 (* used to enforce the type invariant *)
predicate biginv (_b: big) = 89>55 (* used to enforce the type invariant *)
constant min_big : int = -m*m
constant max_big : int = m*m - 1
......
......@@ -30,7 +30,7 @@ module M
val alloc : ref first_free_addr
val new_pointer (tt:unit) : pointer writes { alloc }
val new_pointer (_tt:unit) : pointer writes { alloc }
ensures { !alloc = old !alloc + 1 /\ result = old !alloc }
(*
......
......@@ -91,7 +91,7 @@ module Impl
(forall i. 0 <= i < size -> path size link i (dist i) (repr i))
} by {
size = 0; link = Array.make 0 0; rank = Array.make 0 0;
repr = (fun i -> i); dist = (fun i -> 0)
repr = (fun i -> i); dist = (fun _i -> 0)
}
let create (n: int) : t
......@@ -105,7 +105,7 @@ module Impl
done;
let rank = Array.make n 0 in
{ size = n; link = link; rank = rank;
repr = (fun i -> i); dist = (fun i -> 0) }
repr = (fun i -> i); dist = (fun _i -> 0) }
let rec lemma path_dist (size: int) (link: array int) (dist: int -> int)
(x d y: int)
......
......@@ -150,14 +150,14 @@ theory List
| Cons x xs -> if p x then (dropWhile p xs) else (Cons x xs)
end
predicate pfalse (x: 'a) = false
predicate pfalse (_x: 'a) = false
function dropWhile_False (l : list 'a) : list 'a = match l with
| Nil -> Nil
| Cons x xs -> if pfalse x then (dropWhile_False xs) else (Cons x xs)
end
predicate ptrue (x: 'a) = true
predicate ptrue (_x: 'a) = true
function takeWhile_True (l : list 'a) : list 'a = match l with
| Nil -> Nil
......
......@@ -512,7 +512,7 @@ module PatienceAbstract
let stack_i,_ = s.positions[si] in
0 <= stack_i < s.num_stacks
)
so range f sigma.seqlen s.num_stacks
so range f sigma.seqlen s.num_stacks
so not (injective f sigma.seqlen)
};
assert { (* contradiction from non-injectivity *)
......
......@@ -33,7 +33,7 @@ module SimpleQueue
m = 0; n = 0;
contents = S.empty; }
let dequeue (q: t 'a) : 'a
let dequeue (q: t 'a) : (_r: 'a)
requires { S.length q.contents > 0 }
writes { q.m, q.contents }
ensures { S.(q.contents == (old q.contents)[1..]) }
......
......@@ -24,8 +24,8 @@ predicate tworedneighbors (c: coloring) (i:int)
predicate valid (c:coloring) =
forall i. 0 <= i < length c -> c[i] = Red -> tworedneighbors c i
function black (n:int) : color = Black
function red (n:int) : color = Red
function black (_n:int) : color = Black
function red (_n:int) : color = Red
function colorings0 : fset coloring = add (create 0 black) Fset.empty
function colorings1 : fset coloring = add (create 1 black) Fset.empty
......
......@@ -57,7 +57,7 @@ let delete (g:gap_buffer) : unit
Implemented by a constant (K) in the problem statement.
This version is more general and account for the standard doubling pattern
as well. *)
val growth (g:gap_buffer) : int ensures { result > 0 }
val growth (_g:gap_buffer) : int ensures { result > 0 }
(* Since it is an internal primitive, it is fine to refer to r as well. *)
let grow (g:gap_buffer) : unit
......
......@@ -116,7 +116,7 @@ module NQueens
use ref.Refint
let rec count_bt_queens (board: array int) (n: int) (pos: int) : int
let rec count_bt_queens (board: array int) (n: int) (pos: int) : (_r: int)
variant { n - pos }
requires { length board = n /\ 0 <= pos <= n /\ solution board pos }
ensures { eq_board board (old board) pos }
......@@ -133,7 +133,7 @@ module NQueens
!s
end
let count_queens (board: array int) (n: int) : int
let count_queens (board: array int) (n: int) : (_r: int)
requires { length board = n }
ensures { true }
= count_bt_queens board n 0
......@@ -204,7 +204,7 @@ module NQueens63
i := !i + 1
done
let count_queens (n: int63) : P.t
let count_queens (n: int63) : (_p: P.t)
requires { n >= 0 }
ensures { true }
=
......
......@@ -118,7 +118,7 @@ module Harness
raises { Failure -> false }
= build (Cons 1 (Cons 3 (Cons 3 (Cons 2 Nil))))
let harness2 ()
let harness2 () : (_t : tree)
ensures { false } raises { Failure -> true }
= build (Cons 1 (Cons 3 (Cons 2 (Cons 2 Nil))))
......
......@@ -115,10 +115,14 @@ val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern
val dterm : Coercion.t -> ?loc:Loc.position -> dterm_node -> dterm
(** Final stage *)
(** Unused variables *)
val debug_ignore_unused_var : Debug.flag
val attr_w_unused_var_no : Ident.attribute
val attr_w_unused_var_no : attribute
(* Emit a warning if the variable is unused *)
val check_used_var: term -> vsymbol -> unit
(** Final stage *)
val term : ?strict:bool -> ?keep_loc:bool -> dterm -> term
......
......@@ -1189,6 +1189,96 @@ let add_binders env pvl = List.fold_left add_pvsymbol env pvl
let add_xsymbol ({xsm = xsm} as env) xs =
{ env with xsm = Mstr.add xs.xs_name.id_string xs xsm }
(** Check usage of variables *)
exception Unused of Loc.position option * string
(* Check that [pv] is used according to [check_present] *)
let check_used_gen ~check_present pv =
if not (Sattr.mem Dterm.attr_w_unused_var_no pv.pv_vs.vs_name.id_attrs) &&
Debug.test_noflag Dterm.debug_ignore_unused_var then
begin
let s = pv.pv_vs.vs_name.id_string in
if (s = "" || s.[0] <> '_') && not (check_present pv) then
raise (Unused (pv.pv_vs.vs_name.id_loc, "unused variable " ^ s))
end
(* Check usage of [pv] in [e] *)
let check_used_pv e pv =
let check_present pv = Spv.mem pv e.e_effect.eff_reads in
try check_used_gen ~check_present pv with
| Unused (loc, msg) -> Warning.emit ?loc "%s" msg
(* Return warnings if unused variables are found in functions spec/body:
[bl] is the list of arguments,
[dsp] is the spec of the function,
[eff_reads] are the read effects of the body of the function (if any)
No warnings are returned on result variables of type [unit].
No warnings are returned if there are no body, no pre, and no (x)post.
*)
let check_unused_vars_fun (bl: Ity.pvsymbol list) (dsp: dspec_final) eff_reads =
(* TBD: When there is no pre/post contract and body, no warnings. *)
if dsp.ds_pre = [] && dsp.ds_post = [] && Ity.Mxs.is_empty dsp.ds_xpost &&
eff_reads = None then
()
else begin
let aggregate_post res_var fvars_uc post =
(* Calculate free vars of postconditions list *)
List.fold_left
(fun (res_var, fvars_uc) (v,t) ->
(* Do not collect result variables of type unit: they can be unused *)
let res_var = if Ity.ity_equal Ity.ity_unit v.pv_ity then res_var
else v :: res_var in
(res_var, t_freevars fvars_uc t))
(res_var, fvars_uc) post in
(* Generate freevars of (x)postconditions before the rest *)
let res_var, fvars_uc_post =
aggregate_post [] Mvs.empty dsp.ds_post in
(* Collect exceptional postcondition freevars and result vars *)
let res_var, fvars_uc_post =
Mxs.fold (fun _ xposts (res_var, fvars_uc) ->
aggregate_post res_var fvars_uc xposts) dsp.ds_xpost (res_var, fvars_uc_post)
in
(* Collect preconditions freevars *)
let fvars_uc = List.fold_left t_freevars fvars_uc_post dsp.ds_pre in
(* Add variables that are marked read by the function. Those are considered
used in particular when we only have the spec of a function. *)
let fvars_uc =
List.fold_left (fun fvars_uc pv -> Mvs.add pv.pv_vs 1 fvars_uc)
fvars_uc dsp.ds_reads in
(* Add terms that are marked writes *)
let fvars_uc =
List.fold_left t_freevars fvars_uc dsp.ds_writes in
(* Add variables used in the body of the function (if there is one) *)
let fvars_uc =
Opt.fold (fun fvars_uc eff ->
List.fold_left (fun fvars_uc pv -> Mvs.add pv.pv_vs 1 fvars_uc)
fvars_uc eff) fvars_uc eff_reads in
let check_present pv = Mvs.mem pv.pv_vs fvars_uc in
let check_used pv =
try check_used_gen ~check_present pv with
| Unused (loc, msg) -> Warning.emit ?loc "%s" msg
in
(* Check the usage of normal arguments *)
List.iter check_used bl;
(* The case is different for result variables of postcondition. Those can
occur only in postconditions but each "post" is newly quantified on a
new result variable. In this case, we report an unused variables only if
all the generated result variables are unused. *)
try
let unused =
List.fold_left (fun _ pv ->
(* Exit if we find a result variable that is used *)
try check_used_gen ~check_present pv; raise Exit with
| Unused (loc, msg) -> Some (loc, msg)) None res_var
in
match unused with
| Some (loc, msg) when loc <> None
(* loc = None not supported for results *) -> Warning.emit ?loc "%s" msg
| _ -> ()
with Exit -> ()
end
(** Abstract values *)
let cty_of_spec env bl mask dsp dity =
......@@ -1204,19 +1294,12 @@ let cty_of_spec env bl mask dsp dity =
let p = rebase_pre env preold old dsp.ds_pre in
let q = create_post ity dsp.ds_post in
let xq = create_xpost dsp.ds_xpost in
(* Check for unused variables *)
check_unused_vars_fun bl dsp None;
create_cty_defensive ~mask bl p q xq (get_oldies old) eff ity
(** Expressions *)
let check_used_pv e pv =
if not (Sattr.mem Dterm.attr_w_unused_var_no pv.pv_vs.vs_name.id_attrs) &&
Debug.test_noflag Dterm.debug_ignore_unused_var then
begin
let s = pv.pv_vs.vs_name.id_string in
if (s = "" || s.[0] <> '_') && not (Spv.mem pv e.e_effect.eff_reads) then
Warning.emit ?loc:pv.pv_vs.vs_name.id_loc "unused variable %s" s
end
let e_let_check e ld = match ld with
| LDvar (v,_) -> check_used_pv e v; e_let ld e
| _ -> e_let ld e
......@@ -1652,6 +1735,8 @@ and lambda uloc env pvl mask dsp dvl de =
let xq = create_xpost dsp.ds_xpost in
let e = if not dsp.ds_diverge then e
else e_attr_add Vc.nt_attr e in
(* Check for unused variables *)
check_unused_vars_fun pvl dsp (Some (Ity.Spv.elements e.e_effect.eff_reads));
c_fun ~mask pvl p q xq (get_oldies old) e, dsp, dvl
let rec_defn ?(keep_loc=true) drdf =
......
......@@ -1304,6 +1304,14 @@ let tyl_of_params {muc_theory = tuc} pl =
ty_of_pty tuc ty in
List.map ty_of_param pl
(* Used to check unused variables in logic declarations *)
let check_unused_vars ldl =
List.iter
(fun (_name, ld) ->
let (vsl, t) = open_ls_defn ld in
List.iter (Dterm.check_used_var t) vsl)
ldl
let add_logics muc dl =
let lsymbols = Hstr.create 17 in
(* 1. create all symbols and make an environment with these symbols *)
......@@ -1339,7 +1347,10 @@ let add_logics muc dl =
abst, (make_ls_defn ls vl t) :: defn in
let abst,defn = List.fold_right type_decl dl ([],[]) in
let add_param muc s = add_decl muc (create_param_decl s) in
let add_logic muc l = add_decl muc (create_logic_decl l) in
let add_logic muc l =
(* Check for unused vars in logic declaration *)
check_unused_vars l;
add_decl muc (create_logic_decl l) in
let muc = List.fold_left add_param muc abst in
if defn = [] then muc else add_logic muc defn
......
......@@ -18,7 +18,7 @@ module Multiplication