plugins/cfg/cfg_paths.ml

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 open Why3
  13 open Cfg_ast
  14 open Ptree
  15
  16 let warn_deprecated_named_invariant =
  17   Loc.register_warning "deprecated_named_invariant"
  18     "Named invariants in MLCFG are deprecated. Use hyp_name: attribute to provide hypothesis names instead"
  19
  20 let debug = Debug.register_flag "cfg" ~desc:"CFG plugin debug flag"
  21 let unit_type = PTtuple []
  22 let mk_id ~loc name = { id_str = name; id_ats = []; id_loc = loc }
  23 let mk_expr ~loc d = { expr_desc = d; expr_loc = loc }
  24 let mk_unit ~loc = mk_expr ~loc (Etuple [])
  25 let mk_check ~loc t = mk_expr ~loc (Eassert (Expr.Check, t))
  26 let mk_assume ~loc t = mk_expr ~loc (Eassert (Expr.Assume, t))
  27 let mk_seq ~loc e1 e2 = mk_expr ~loc (Esequence (e1, e2))
  28 let mk_pat ~loc d = { pat_desc = d; pat_loc = loc }
  29 let pat_wild ~loc = mk_pat ~loc Pwild
  30
  31 let empty_spec =
  32   {
  33     sp_pre = [];
  34     sp_post = [];
  35     sp_xpost = [];
  36     sp_reads = [];
  37     sp_writes = [];
  38     sp_alias = [];
  39     sp_variant = [];
  40     sp_checkrw = false;
  41     sp_diverge = false;
  42     sp_partial = false;
  43   }
  44
  45 let pp_id fmt id = Format.pp_print_string fmt id.id_str
  46
  47 let rec pp_qid fmt qid =
  48   match qid with Qident id -> pp_id fmt id | Qdot (q, id) -> Format.fprintf fmt "%a.%a" pp_qid q pp_id id
  49
  50 let rec pp_pty fmt t =
  51   match t with
  52   | PTtyapp (qid, l) -> Format.fprintf fmt "@[%a %a@]" pp_qid qid (Pp.print_list Pp.semi pp_pty) l
  53   | _ -> Format.pp_print_string fmt "<unknown pp_pty>"
  54
  55 let divergent_attr = ATstr (Ident.create_attribute "vc:divergent")
  56
  57 exception CFGError of string
  58
  59 let () =
  60   Exn_printer.register (fun fmt exn ->
  61       match exn with CFGError msg -> Format.fprintf fmt "CFG translation error: %s" msg | _ -> raise exn)
  62
  63 let translate_cfg preconds block (blocks : (label * block) list) =
  64   let invcounter = ref 0 in
  65   let blocks = List.fold_left (fun acc (l, b) -> Wstdlib.Mstr.add l.id_str b acc) Wstdlib.Mstr.empty blocks in
  66   let thestartlabel = "start" in
  67   let visited_entry_points = ref [ thestartlabel ] in
  68   let funs = ref [] in
  69
  70   let rec translate_term startlabel visited_terms (t : cfg_term) : Ptree.expr =
  71     let loc = t.cfg_term_loc in
  72     if List.memq t visited_terms then begin
  73       let msg = "cycle without invariant" in
  74       let msg = if startlabel = thestartlabel then msg else msg ^ " starting from `" ^ startlabel ^ "`" in
  75       raise (Loc.Located (loc, CFGError msg))
  76     end;
  77     match t.cfg_term_desc with
  78     | CFGgoto l -> translate_goto startlabel (t :: visited_terms) l
  79     | CFGreturn e -> e
  80     | CFGabsurd -> mk_expr ~loc:t.cfg_term_loc Eabsurd
  81     | CFGswitch (e, cases) ->
  82         let branches =
  83           List.map
  84             (fun (pat, l) ->
  85               let e = translate_term startlabel (t :: visited_terms) l in
  86               (pat, e))
  87             cases
  88         in
  89         mk_expr ~loc (Ematch (e, branches, []))
  90   and translate_goto startlabel visited_terms (l : label) : Ptree.expr =
  91     let bl =
  92       try Wstdlib.Mstr.find l.id_str blocks
  93       with Not_found -> raise (Loc.Located (l.id_loc, CFGError ("label " ^ l.id_str ^ " not found for goto")))
  94     in
  95     traverse_block startlabel visited_terms bl
  96   and traverse_block startlabel visited_terms (blk : block) : Ptree.expr =
  97     let instrs, term = blk in
  98     begin
  99       match instrs with
 100       | [] -> translate_term startlabel visited_terms term
 101       | i :: rem ->
 102           let loc = i.cfg_instr_loc in
 103           let traverse_block = traverse_block startlabel visited_terms in
 104           begin
 105             match (i.cfg_instr_desc, rem) with
 106             | CFGinvariant l1, { cfg_instr_desc = CFGinvariant l2 } :: rem ->
 107                 traverse_block ({ i with cfg_instr_desc = CFGinvariant (l1 @ l2) } :: rem, term)
 108             | CFGinvariant l, _ ->
 109                 let id =
 110                   match l with
 111                   | (_, _, _, { contents = Some id }) :: _ -> id
 112                   | (_, _, _, idr) :: _ ->
 113                      let i = !invcounter in invcounter := !invcounter + 1;
 114                      idr := Some i;
 115                      i
 116                   | _ -> assert false
 117                 in
 118                 let id = Printf.sprintf "invariant_%d" id in
 119                 let l =
 120                   List.map
 121                     (fun (k, id, t, _) ->
 122                       if k = Variant then
 123                         Loc.errorm ~loc:t.term_loc "`variant` clauses are not supported in the Paths backend";
 124                       if id <> None then
 125                         Loc.warning ~loc:t.term_loc warn_deprecated_named_invariant
 126                           "Named invariants are deprecated. Please use the `hyp_name` attribute directly";
 127                       t)
 128                     l
 129                 in
 130                 if not (List.mem id !visited_entry_points) then begin
 131                   visited_entry_points := id :: !visited_entry_points;
 132                   traverse_from_entry_point id l (rem, term)
 133                 end;
 134                 let k = mk_expr ~loc (Eidapp (Qident (mk_id ~loc ("_from_" ^ id)), [ mk_unit ~loc ])) in
 135                 List.fold_right
 136                   (fun t acc ->
 137                     let e = mk_check ~loc:t.term_loc t in
 138                     mk_seq ~loc e acc)
 139                   l k
 140             | CFGexpr e1, _ ->
 141                 let e2 = traverse_block (rem, term) in
 142                 mk_seq ~loc e1 e2
 143           end
 144     end
 145   and traverse_from_entry_point startlabel preconds (block : block) =
 146     let e = traverse_block startlabel [] (block : block) in
 147     funs := (startlabel, preconds, e) :: !funs
 148   in
 149
 150   traverse_from_entry_point thestartlabel preconds (block : block);
 151   !funs
 152
 153 let e_ref = mk_expr ~loc:Loc.dummy_position Eref
 154
 155 let declare_local (ghost, id, ty, init) body =
 156   let loc = id.id_loc in
 157   Debug.dprintf debug "declaring local variable %a of type %a@." pp_id id pp_pty ty;
 158   let e : expr =
 159     match init with
 160     | Some e -> e
 161     | None -> mk_expr ~loc (Eany ([], Expr.RKnone, Some ty, pat_wild ~loc, Ity.MaskVisible, empty_spec))
 162   in
 163   let e = mk_expr ~loc (Eapply (e_ref, e)) in
 164   let id = { id with id_ats = ATstr Pmodule.ref_attr :: id.id_ats } in
 165   mk_expr ~loc:id.id_loc (Elet (id, ghost, Expr.RKnone, e, body))
 166
 167 let build_path_function retty pat mask postconds (startlabel, preconds, body) : Ptree.fundef =
 168   let body =
 169     List.fold_left
 170       (fun acc t ->
 171         let loc = t.term_loc in
 172         let e = mk_assume ~loc t in
 173         mk_seq ~loc e acc)
 174       body preconds
 175   in
 176   let loc = Loc.dummy_position in
 177   let spec = { empty_spec with sp_post = postconds } in
 178   let id = mk_id ~loc ("_from_" ^ startlabel) in
 179   let arg = (loc, None, false, Some unit_type) in
 180   (id, false, Expr.RKnone, [ arg ], Some retty, pat, mask, spec, body)
 181
 182 let translate_cfg_fundef cf =
 183   Debug.dprintf debug "translating cfg function `%s`@." cf.cf_name.id_str;
 184   Debug.dprintf debug "return type is `%a`@." pp_pty cf.cf_retty;
 185   let funs = translate_cfg cf.cf_spec.sp_pre cf.cf_block0 cf.cf_blocks in
 186   let loc = Loc.dummy_position in
 187   let body = mk_expr ~loc (Eidapp (Qident (mk_id ~loc "_from_start"), [ mk_unit ~loc ])) in
 188   let defs = List.map (build_path_function cf.cf_retty cf.cf_pat cf.cf_mask cf.cf_spec.sp_post) funs in
 189   let body = mk_expr ~loc (Erec (defs, body)) in
 190   let body = List.fold_right declare_local cf.cf_locals body in
 191   (* ignore termination *)
 192   let body = mk_expr ~loc (Eattr (divergent_attr, body)) in
 193   let body = List.fold_right (fun a e -> mk_expr ~loc (Eattr (a, e))) cf.cf_attrs body in
 194   (cf.cf_name, false, Expr.RKnone, cf.cf_args, Some cf.cf_retty, cf.cf_pat, cf.cf_mask, cf.cf_spec, body)