Merge branch 'issue_346' into 'master'

Unused variables message

See merge request !198

bench/ce/double_projection.mlw

@@ -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

bench/ce/if_assign.mlw

@@ -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;

bench/programs/good/346_unused_variables_2.mlw

+use int.Int
+
+(* Should not output any unused variable *)
+val v (x : int) (y : int) : bool
+  ensures {x = y <-> result}
+  ensures {x = y}

bench/programs/good/346_unused_variables_9.mlw

+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 }

bench/programs/good/complex_arg_1.mlw

@@ -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 ())
-

bench/programs/good/complex_arg_2.mlw

@@ -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)
-

bench/programs/good/loops.mlw

@@ -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
-

bench/programs/good/mutual_exns.mlw

@@ -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

bench/programs/good/recfun.mlw

@@ -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
-

bench/programs/warn-typing/346_unused_warning.mlw

+use int.Int
+
+(* result unused *)
+val eq (x: int) (y: int) : bool
+    ensures { x = y }

bench/programs/warn-typing/346_unused_warning_1.mlw

+use int.Int
+
+(* z unused *)
+function f (x : int) (y : int) : bool = forall z:int. x = y

bench/programs/warn-typing/346_unused_warning_3.mlw

+use int.Int
+
+(* y unused *)
+function g (x: int) (y: int) : bool = forall z:int. x = z

bench/programs/warn-typing/346_unused_warning_4.mlw

+use int.Int
+
+(* result unused *)
+let eq1 (x : int) (y : int) : bool
+    ensures { x = y }
+= true

bench/programs/warn-typing/346_unused_warning_5.mlw

+use int.Int
+
+(* y unused *)
+let eq2 (x: int) (y : int) : bool
+    ensures { result <-> (x = x) }
+= true

bench/programs/warn-typing/346_unused_warning_6.mlw

+use int.Int
+
+(* y is unused *)
+goal h : forall y x: int. x = 42

bench/programs/warn-typing/346_unused_warning_7.mlw

+use int.Int
+
+(* x is unused *)
+predicate p (x: int) (y: int) = y = 0

bench/programs/warn-typing/346_unused_warning_8.mlw

+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   }

bench/typing/good/20610.mlw

@@ -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 }
           =

examples/arm.mlw

@@ -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 *)

examples/avl/tables.mlw

@@ -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
-

examples/bellman_ford.mlw

@@ -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 }

examples/bts/13853.mlw

@@ -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

examples/bts/13853a.mlw

@@ -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

examples/bts/13853b.mlw

@@ -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
 

examples/dijkstra.mlw

@@ -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 ->

examples/hillel_challenge.mlw

@@ -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

examples/in_progress/course.mlw

@@ -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 }
 
 (*

examples/in_progress/union_find.mlw

@@ -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)

examples/logic/isa_planner.why

@@ -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

examples/patience.mlw

@@ -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 *)

examples/simple_queue.mlw

@@ -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..]) }

examples/verifythis_2018_le_rouge_et_le_noir_1.mlw

@@ -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

examples/verifythis_2018_mind_the_gap_1.mlw

@@ -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

examples/vstte10_queens.mlw

@@ -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 }
   =

examples/vstte12_tree_reconstruction.mlw

@@ -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))))
 

src/core/dterm.mli

@@ -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
 

src/mlw/dexpr.ml

@@ -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 =

src/parser/typing.ml

@@ -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