Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

main.ml 8.75 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
8 9 10 11 12 13 14 15 16 17 18 19
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software 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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
21
open Theory
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
22
open Driver
23

24
let files = Queue.create ()
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
25 26
let parse_only = ref false
let type_only = ref false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
27
let debug = ref false
28
let loadpath = ref []
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
29
let driver = ref None
30 31 32 33 34 35 36 37
type which_goals =
  | Gall
  | Gtheory of string
  | Ggoal of string
let which_goals = ref Gall
let timeout = ref 10
let call = ref false
let output = ref None
38

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
39 40 41 42
let () = 
  Arg.parse 
    ["--parse-only", Arg.Set parse_only, "stops after parsing";
     "--type-only", Arg.Set type_only, "stops after type-checking";
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
43
     "--debug", Arg.Set debug, "sets the debug flag";
44
     "-I", Arg.String (fun s -> loadpath := s :: !loadpath), 
45 46 47 48 49 50 51 52 53 54 55 56 57
     "<dir>  adds dir to the loadpath";
     "--all_goals", Arg.Unit (fun () -> which_goals := Gall), 
     "apply on all the goals of the file";
     "--goals_of", Arg.String (fun s -> which_goals := Gtheory s), 
     "apply on all the goals of the theory given (ex. --goal T)";
     "--goal", Arg.String (fun s -> which_goals := Ggoal s), 
     "apply only on the goal given (ex. --goal T.g)";
     "--output", Arg.String (fun s -> output := Some s), 
     "choose to output each goals in the directory given.\
 Can't be used with --call";
     "--call", Arg.Set call, 
     "choose to call the prover on each goals.\
 Can't be used with --output"; (* Why not? *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
58
     "--driver", Arg.String (fun s -> driver := Some s),
59
     "<file>  set the driver file";
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
60
    ]
61
    (fun f -> Queue.push f files)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
62
    "usage: why [options] files..."
63

64 65 66 67
let () = 
  match !output with
    | None when not !call -> type_only := true
    | _ -> ()
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
68

69
(*
70 71 72
let transformation l = 
  let t1 = Simplify_recursive_definition.t in
  let t2 = Inlining.all in
73 74
  List.map (fun (t,c) ->
              let c = if !simplify_recursive 
75
              then Transform.apply t1 c
76
              else c in
77
              let c = if !inlining then Transform.apply t2 c
78 79
              else c in
              (t,c)) l
80
*)
81
let rec report fmt = function
82
  | Lexer.Error e ->
83 84 85 86 87
      fprintf fmt "lexical error: %a" Lexer.report e;
  | Loc.Located (loc, e) ->
      fprintf fmt "%a%a" Loc.report_position loc report e
  | Parsing.Parse_error ->
      fprintf fmt "syntax error"
88 89
  | Typing.Error e ->
      Typing.report fmt e
90 91
  | Context.UnknownIdent i ->
      fprintf fmt "anomaly: unknownident %s" i.Ident.id_short
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
92 93
  | Driver.Error e ->
      Driver.report fmt e
94
  | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
95

96
(*
97
let transform env l =
98 99 100 101 102
  let l = 
    List.map 
      (fun t -> t, Context.use_export (Context.init_context env) t) 
      l
  in
103
  (*let l = transformation l in*)
104
  if !print_stdout then 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105
    List.iter 
106 107
      (fun (t,ctxt) -> Pretty.print_named_context
        std_formatter t.th_name.Ident.id_long ctxt) l
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108 109 110 111
  else match !driver with
    | None ->
	()
    | Some file ->
112

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113
	begin match l with
114
	  | (_,ctxt) :: _ -> begin match extract_goals ctxt with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
115 116 117 118 119 120 121
	      | g :: _ -> 
		  Driver.print_context drv std_formatter g
	      | [] -> 
		  eprintf "no goal@."
	    end
	  | [] -> ()
	end
122 123 124 125 126 127 128 129 130 131
*)


let extract_goals env acc th =
  let ctxt = Context.use_export (Context.init_context env) th in
  let l = Transform.apply Transform.split_goals ctxt in
  let l = List.rev_map (fun ctxt -> (th,ctxt)) l in
  List.rev_append l acc

let file_sanitizer = Ident.sanitizer Ident.char_to_alnumus Ident.char_to_alnumus
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
132

133
let do_file env drv filename_printer file =
134 135 136 137 138 139 140 141
  if !parse_only then begin
    let c = open_in file in
    let lb = Lexing.from_channel c in
    Loc.set_file file lb;
    let _ = Lexer.parse_logic_file lb in 
    close_in c
  end else begin
    let m = Typing.read_file env file in
142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202
    if not !type_only then
      let drv =  
        match drv with
          | None -> eprintf "a driver is needed@."; exit 1
          | Some drv -> drv in
      let goals = 
        match !which_goals with
          | Gall ->  Mnm.fold (fun _ th acc -> extract_goals env acc th) m []
          | Gtheory s ->  
              begin
                try 
                  extract_goals env [] (Mnm.find s m)
                with Not_found -> 
                  eprintf "File %s : --goals_of : Unknown theory %s@." file s; exit 1
              end
          | Ggoal s ->
              let l = Str.split (Str.regexp "\\.") s in
              let tname, l = 
                match l with
                  | [] | [_] -> 
                      eprintf "--goal : Must be a qualified name (%s)@." s;
                      exit 1
                  | a::l -> a,l in
              let rec find_pr ns = function
                | [] -> assert false
                | [a] -> Mnm.find a ns.ns_pr
                | a::l -> find_pr (Mnm.find a ns.ns_ns) l in
              let th =try Mnm.find tname m with Not_found -> 
                eprintf "File %s : --goal : Unknown theory %s@." file tname; exit 1 in
              let pr = try find_pr th.th_export l with Not_found ->
                eprintf "File %s : --goal : Unknown goal %s@." file s ; exit 1 in
              let goals = extract_goals env [] th in
              List.filter (fun (_,ctxt) ->
                             match ctxt.ctxt_decl.d_node with
                               | Dprop (_,{pr_name = pr_name}) -> 
                                   Ident.derived_from pr_name pr.pr_name
                               | _ -> assert false) goals in
      let file = 
        let file = Filename.basename file in
        let file = Filename.chop_extension file in
        Ident.id_unique filename_printer 
          (Ident.id_register (Ident.id_fresh file)) in
      match !output with
        | None -> ()
        | Some dir -> 
            let ident_printer = Ident.create_ident_printer 
              ~sanitizer:file_sanitizer [] in
            List.iter 
              (fun (th,ctxt) ->
                 let cout = 
                   if dir = "-" 
                   then stdout
                   else
                     let filename = 
                       Driver.filename_of_goal drv ident_printer 
                         file th.th_name.Ident.id_short ctxt in
                     let filename = Filename.concat dir filename in
                     open_out filename in
                 let fmt = formatter_of_out_channel cout in
                 fprintf fmt "%a@?" (Driver.print_context drv) ctxt;
                 close_out cout) goals
203 204
  end

205 206
let () =
  try
207
    let env = create_env (Typing.retrieve !loadpath) in
208 209 210 211 212 213
    let drv = match !driver with
      | None -> None
      | Some file -> Some (load_driver file env) in
    let filename_printer = Ident.create_ident_printer 
      ~sanitizer:file_sanitizer [] in
    Queue.iter (do_file env drv filename_printer) files
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
214
  with e when not !debug ->
215 216
    eprintf "%a@." report e;
    exit 1
217

218 219 220 221 222 223
(*
Local Variables: 
compile-command: "unset LANG; make -C .. test"
End: 
*)

224 225
(****

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
226 227 228 229 230 231 232 233 234
#load "hashcons.cmo";;
#load "name.cmo";;
#load "term.cmo";;
#load "pp.cmo";;
#load "pretty.cmo";;
#install_printer Name.print;;
#install_printer Pretty.print_ty;;
#install_printer Pretty.print_term;;

Johannes Kanig's avatar
Johannes Kanig committed
235 236 237
open Term

let alpha = Name.from_string "alpha"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
238
let var_alpha = Ty.ty_var alpha
Johannes Kanig's avatar
Johannes Kanig committed
239

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
240
let list = Ty.create_tysymbol (Name.from_string "list") [alpha] None
Johannes Kanig's avatar
Johannes Kanig committed
241

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
242 243
let list_alpha = Ty.ty_app list [var_alpha]
let list_list_alpha = Ty.ty_app list [list_alpha]
Johannes Kanig's avatar
Johannes Kanig committed
244

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
245 246 247
let nil = create_fsymbol (Name.from_string "nil") ([], list_alpha)
let t_nil = t_app nil [] list_alpha
let tt_nil = t_app nil [] list_list_alpha
Johannes Kanig's avatar
Johannes Kanig committed
248

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
249 250
let cons = create_fsymbol (Name.from_string "cons") 
  ([var_alpha; list_alpha], list_alpha)
Johannes Kanig's avatar
Johannes Kanig committed
251

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
252
let int_ = Ty.create_tysymbol (Name.from_string "int") [] None
Johannes Kanig's avatar
Johannes Kanig committed
253

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
254
let _ = t_app cons [t_nil; tt_nil] list_list_alpha
Johannes Kanig's avatar
Johannes Kanig committed
255

256
****)