Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 06c1a5a5 authored by MARCHE Claude's avatar MARCHE Claude

make usage of concrete file paths more robust

parent 255164f9
......@@ -4,11 +4,15 @@
<why3session shape_version="5">
<prover id="0" name="Z3" version="4.6.0" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="11" steplimit="0" memlimit="1000"/>
<file name="../isqrt.mlw" proved="true">
<file proved="true">
<path name=".."/>
<path name="isqrt.mlw"/>
<theory name="Square" proved="true">
<goal name="sqr_non_neg" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="sqr_increasing" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
......
......@@ -10,11 +10,14 @@
<!ATTLIST prover memlimit CDATA #IMPLIED>
<!ATTLIST prover steplimit CDATA #IMPLIED>
<!ELEMENT file (theory*)>
<!ATTLIST file name CDATA #REQUIRED>
<!ELEMENT file (path*) (theory*)>
<!ATTLIST file name CDATA #IMPLIED>
<!ATTLIST file verified CDATA #IMPLIED>
<!ATTLIST file proved CDATA #IMPLIED>
<!ELEMENT path EMPTY>
<!ATTLIST path name CDATA #REQUIRED>
<!ELEMENT theory (label*,goal*)>
<!ATTLIST theory name CDATA #REQUIRED>
<!ATTLIST theory verified CDATA #IMPLIED>
......
......@@ -514,7 +514,7 @@ let call_on_buffer ~command ~limit ~res_parser ~filename ~printer_mapping
Filename.open_temp_file "why_" ("_" ^ filename)
else
begin
let filename = Sysutil.absolutize_filename (Sys.getcwd ()) filename in
let filename = Sysutil.absolutize_path (Sys.getcwd ()) [filename] in
if inplace then
Sys.rename filename (backup_file filename);
filename, open_out filename
......
......@@ -123,7 +123,7 @@ rule token = parse
match tok with
| INPUT filename ->
let dirname = Filename.dirname lexbuf.lex_curr_p.pos_fname in
let filename = Sysutil.absolutize_filename dirname filename in
let filename = Sysutil.absolutize_path dirname [filename] in
Stack.push (input_lexbuf filename) s;
multifile lex_dumb
| EOF -> ignore (Stack.pop s);
......
......@@ -530,7 +530,7 @@ let load_main dirname section =
raise WrongMagicNumber;
{ libdir = get_string ~default:default_main.libdir section "libdir";
datadir = get_string ~default:default_main.datadir section "datadir";
loadpath = List.map (Sysutil.absolutize_filename dirname)
loadpath = List.map (fun f -> Sysutil.absolutize_path dirname [f])
(get_stringl ~default:[] section "loadpath");
timelimit = get_int ~default:default_main.timelimit section "timelimit";
memlimit = get_int ~default:default_main.memlimit section "memlimit";
......@@ -556,7 +556,7 @@ let read_config_rc conf_file =
exception ConfigFailure of string (* filename *) * string
let get_dirname filename =
Filename.dirname (Sysutil.absolutize_filename (Sys.getcwd ()) filename)
Filename.dirname (Sysutil.absolutize_path (Sys.getcwd ()) [filename])
let get_config (filename,rc) =
let dirname = get_dirname filename in
......@@ -688,7 +688,7 @@ let merge_config config filename =
let main = match get_section rc "main" with
| None -> config.main
| Some rc ->
let loadpath = (List.map (Sysutil.absolutize_filename dirname)
let loadpath = (List.map (fun f -> Sysutil.absolutize_path dirname [f])
(get_stringl ~default:[] rc "loadpath")) @ config.main.loadpath in
let plugins =
(get_stringl ~default:[] rc "plugin") @ config.main.plugins in
......
......@@ -176,9 +176,9 @@ module PSession = struct
let s = x.tcont.controller_session in
let n y acc = { x with tkind = y } :: acc in
match x.tkind with
| Session -> "", Hstr.fold (fun _ f -> n (File f)) (get_files s) []
| Session -> "", Hfile.fold (fun _ f -> n (File f)) (get_files s) []
| File f ->
(file_name f),
string_of_file_path (file_path f),
List.fold_right (fun th -> n (Theory th)) (file_theories f) []
| Theory th ->
let id = theory_name th in
......@@ -607,12 +607,14 @@ let create_file_rel_path c pr pn =
let th = get_encapsulating_theory session (APn pn) in
let th_name = (Session_itp.theory_name th).Ident.id_string in
let f = get_encapsulating_file session (ATh th) in
let fn = Filename.chop_extension (Filename.basename (file_name f)) in
let fn = Filename.chop_extension (Session_itp.basename (file_path f)) in
let file = Driver.file_of_task driver fn th_name task in
let file = Filename.concat session_dir file in
let file = Sysutil.uniquify file in
let file = Sysutil.relativize_filename session_dir file in
file
match file with
| [f] -> f
| _ -> assert false
let prepare_edition c ?file pn pr ~notification =
let session = c.controller_session in
......
......@@ -348,13 +348,13 @@ let () =
let pn_to_node_ID : node_ID Hpn.t = Hpn.create 17
let tn_to_node_ID : node_ID Htn.t = Htn.create 17
let th_to_node_ID : node_ID Ident.Hid.t = Ident.Hid.create 7
let file_to_node_ID : node_ID Hstr.t = Hstr.create 3
let file_to_node_ID : node_ID Hfile.t = Hfile.create 3
let node_ID_from_pan pan = Hpan.find pan_to_node_ID pan
let node_ID_from_pn pn = Hpn.find pn_to_node_ID pn
let node_ID_from_tn tn = Htn.find tn_to_node_ID tn
let node_ID_from_th th = Ident.Hid.find th_to_node_ID (theory_name th)
let node_ID_from_file file = Hstr.find file_to_node_ID (file_name file)
let node_ID_from_file file = Hfile.find file_to_node_ID (file_id file)
let node_ID_from_any any =
match any with
......@@ -367,9 +367,9 @@ let () =
let remove_any_node_ID any =
match any with
| AFile file ->
let nid = Hstr.find file_to_node_ID (file_name file) in
let nid = Hfile.find file_to_node_ID (file_id file) in
Hint.remove model_any nid;
Hstr.remove file_to_node_ID (file_name file)
Hfile.remove file_to_node_ID (file_id file)
| ATh th ->
let nid = Ident.Hid.find th_to_node_ID (theory_name th) in
Hint.remove model_any nid;
......@@ -389,7 +389,7 @@ let () =
let add_node_to_table node new_id =
match node with
| AFile file -> Hstr.add file_to_node_ID (file_name file) new_id
| AFile file -> Hfile.add file_to_node_ID (file_id file) new_id
| ATh th -> Ident.Hid.add th_to_node_ID (theory_name th) new_id
| ATn tn -> Htn.add tn_to_node_ID tn new_id
| APn pn -> Hpn.add pn_to_node_ID pn new_id
......@@ -413,7 +413,8 @@ let get_locations (task: Task.task) =
let relativize f =
try Hstr.find file_cache f
with Not_found ->
let g = Sysutil.relativize_filename session_dir f in
(* FIXME: this an abusive use of Sysutil.absolutize_path *)
let g = Sysutil.absolutize_path "" (Sysutil.relativize_filename session_dir f) in
Hstr.replace file_cache f g;
g in
let color_loc ~color ~loc =
......@@ -543,27 +544,32 @@ end
try
let d = get_server_data() in
if d.send_source then
let fn = Sysutil.absolutize_filename
(*
let fn = Sysutil.absolutize_path
(Session_itp.get_dir d.cont.controller_session) f in
let s = Sysutil.file_contents fn in
*)
let s = Sysutil.file_contents f in
P.notify (File_contents (f, s))
with Invalid_argument s ->
P.notify (Message (Error s))
let save_file f file_content =
try
(*
let d = get_server_data() in
let fn = Sysutil.absolutize_filename
(Session_itp.get_dir d.cont.controller_session) f in
Sysutil.backup_file fn;
Sysutil.write_file fn file_content;
*)
Sysutil.backup_file f;
Sysutil.write_file f file_content;
P.notify (Message (File_Saved f))
with Invalid_argument s ->
P.notify (Message (Error s))
let relativize_location s loc =
let f, l, b, e = Loc.get loc in
let f = Sysutil.relativize_filename (Session_itp.get_dir s) f in
(* FIXME: this an abusive use of Sysutil.absolutize_path *)
let f = Sysutil.absolutize_path "" (Sysutil.relativize_filename (Session_itp.get_dir s) f) in
Loc.user_position f l b e
let capture_parse_or_type_errors f cont =
......@@ -608,7 +614,7 @@ end
let get_node_name (node: any) =
let d = get_server_data () in
match node with
| AFile file -> file_name file
| AFile file -> Session_itp.basename (file_path file)
| ATh th -> (theory_name th).Ident.id_string
| ATn tn ->
let name = get_transf_name d.cont.controller_session tn in
......@@ -787,7 +793,7 @@ end
let d = get_server_data () in
let ses = d.cont.controller_session in
let files = get_files ses in
Hstr.iter
Hfile.iter
(fun _ file ->
on_file file;
iter_subtree_from_file on_subtree file)
......@@ -807,9 +813,12 @@ end
let reset_and_send_the_whole_tree (): unit =
P.notify Reset_whole_tree;
iter_on_files
~on_file:(fun file -> read_and_send (file_name file))
~on_subtree:create_node
let d = get_server_data () in
let ses = d.cont.controller_session in
let on_file f =
read_and_send (Session_itp.system_path ses f)
in
iter_on_files ~on_file ~on_subtree:create_node
let unfocus () =
focused_node := Unfocused;
......@@ -830,12 +839,10 @@ end
let create_ce_tab ~print_attrs s res any list_loc =
let f = get_encapsulating_file s any in
let filename = Sysutil.absolutize_filename
(Session_itp.get_dir s) (file_name f)
in
let filename = Session_itp.system_path s f in
let source_code = Sysutil.file_contents filename in
Model_parser.interleave_with_source ~print_attrs ?start_comment:None ?end_comment:None
?me_name_trans:None res.Call_provers.pr_model ~rel_filename:(file_name f)
?me_name_trans:None res.Call_provers.pr_model ~rel_filename:filename
~source_code:source_code ~locations:list_loc
let send_task nid show_full_context loc =
......@@ -858,7 +865,7 @@ end
let prover_text = "Detached prover\n====================> Prover: " ^ name ^ "\n" in
P.notify (Task (nid, prover_text, []))
| AFile f ->
P.notify (Task (nid, "Detached file " ^ file_name f, []))
P.notify (Task (nid, "Detached file " ^ (basename (file_path f)), []))
| ATn tid ->
let name = get_transf_name d.cont.controller_session tid in
let args = get_transf_args d.cont.controller_session tid in
......@@ -909,7 +916,7 @@ end
| None -> P.notify (Task (nid, "Result of the prover not available.\n", old_list_loc))
end
| AFile f ->
P.notify (Task (nid, "File " ^ file_name f, []))
P.notify (Task (nid, "File " ^ (basename (file_path f)), []))
| ATn tid ->
let name = get_transf_name d.cont.controller_session tid in
let args = get_transf_args d.cont.controller_session tid in
......@@ -927,31 +934,31 @@ end
(* Note that f is the path from execution directory to the file and fn is the
path from the session directory to the file. *)
let add_file_to_session cont f =
let fn = Sysutil.relativize_filename
(get_dir cont.controller_session) f in
let dir = get_dir cont.controller_session in
let fn = Sysutil.relativize_filename dir f in
try
let (_ : file) = get_file cont.controller_session fn in
P.notify (Message (Information ("File already in session: " ^ fn)))
let (_ : file) = find_file_from_path cont.controller_session fn in
P.notify (Message (Information ("File already in session: " ^ f)))
with Not_found ->
if (Sys.file_exists f) then
begin
match add_file cont f with
| [] ->
if (Sys.file_exists f) then
begin
match add_file cont f with
| [] ->
session_needs_saving := true;
let file = get_file cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (file_name file);
P.notify (Message (Information "file added in session"))
| l ->
read_and_send fn;
List.iter
(function
| (loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s))))
l
end
else
P.notify (Message (Open_File_Error ("File not found: " ^ f)))
let file = find_file_from_path cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (Sysutil.absolutize_path dir fn);
P.notify (Message (Information "file added in session"))
| l ->
read_and_send (Sysutil.absolutize_path dir fn);
List.iter
(function
| (loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s))))
l
end
else
P.notify (Message (Open_File_Error ("File not found: " ^ f)))
(* ------------ init server ------------ *)
......@@ -1266,7 +1273,7 @@ end
Hpn.clear pn_to_node_ID;
Htn.clear tn_to_node_ID;
Ident.Hid.clear th_to_node_ID;
Hstr.clear file_to_node_ID
Hfile.clear file_to_node_ID
let reload_session () : unit =
let d = get_server_data () in
......
......@@ -24,6 +24,7 @@ let debug_stack_trace = Debug.lookup_flag "stack_trace"
type transID = int
type proofNodeID = int
type proofAttemptID = int
type fileID = int
let print_proofNodeID fmt id =
Format.fprintf fmt "proofNodeID<%d>" id
......@@ -34,7 +35,7 @@ let print_proofAttemptID fmt id =
type theory = {
theory_name : Ident.ident;
mutable theory_goals : proofNodeID list;
mutable theory_parent_name : string;
mutable theory_parent_name : fileID;
mutable theory_is_detached : bool;
}
......@@ -73,14 +74,21 @@ type transformation_node = {
transf_is_detached : bool;
}
type file_path = string list
let string_of_file_path p = String.concat "/" p
type file = {
file_name : string;
file_id : int;
mutable file_path : file_path;
(* access path to the source, in the normal order
i.e. ["..";"foo.mlw"] *)
file_format : string option;
file_is_detached : bool;
mutable file_theories : theory list;
}
let file_name f = f.file_name
let file_id f = f.file_id
let file_path f = f.file_path
let file_format f = f.file_format
let file_theories f = f.file_theories
......@@ -91,9 +99,17 @@ type any =
| APn of proofNodeID
| APa of proofAttemptID
let rec basename p =
match p with
| [] -> raise Not_found
| [f] -> f
| _ :: tl -> basename tl
let print_file_path fmt p = Format.fprintf fmt "%a" (Pp.print_list Pp.slash Pp.string) p
let fprintf_any fmt a =
match a with
| AFile f -> Format.fprintf fmt "<AFile %s>" f.file_name
| AFile f -> Format.fprintf fmt "<AFile [%a]>" print_file_path f.file_path
| ATh th -> Format.fprintf fmt "<ATh %s>" th.theory_name.Ident.id_string
| ATn trid -> Format.fprintf fmt "<ATn %d>" trid
| APn pnid -> Format.fprintf fmt "<APn %d>" pnid
......@@ -102,6 +118,7 @@ let fprintf_any fmt a =
module Hpn = Hint
module Htn = Hint
module Hpan = Hint
module Hfile = Hint
type session = {
proofAttempt_table : proof_attempt_node Hint.t;
......@@ -110,26 +127,28 @@ type session = {
mutable next_proofNodeID : int;
trans_table : transformation_node Hint.t;
mutable next_transID : int;
mutable next_fileID : int;
session_dir : string; (** Absolute path *)
session_files : file Hstr.t;
session_files : file Hfile.t;
session_sum_shape_table : (Termcode.checksum * Termcode.shape) Hpn.t;
session_prover_ids : int Hprover.t;
(* tasks *)
session_raw_tasks : Task.task Hpn.t;
session_task_tables : Trans.naming_table Hpn.t;
(* proved status *)
file_state: bool Hstr.t;
file_state: bool Hfile.t;
th_state: bool Ident.Hid.t;
tn_state: bool Htn.t;
pn_state : bool Hpn.t;
}
let system_path s f =
Sysutil.absolutize_path s.session_dir f.file_path
let theory_parent s th =
Debug.dprintf debug "[Session_itp.theory_parent] th.parent_name = %s@."
Debug.dprintf debug "[Session_itp.theory_parent] th.parent_name = %d@."
th.theory_parent_name;
Hstr.find s.session_files th.theory_parent_name
Hfile.find s.session_files th.theory_parent_name
let session_iter_proof_attempt f s =
Hint.iter f s.proofAttempt_table
......@@ -176,7 +195,7 @@ let get_theories s =
*)
let get_files s = s.session_files
let get_file s name = Hstr.find s.session_files name
(* let get_file s name = Hstr.find s.session_files name *)
let get_dir s = s.session_dir
(*
......@@ -203,6 +222,11 @@ let gen_proofAttemptID (s : session) =
s.next_proofAttemptID <- id + 1;
id
let gen_fileID (s : session) =
let id = s.next_fileID in
s.next_fileID <- id + 1;
id
(* Get elements of the session tree *)
exception BadID
......@@ -373,7 +397,7 @@ let fold_all_any s f acc any =
let fold_all_session s f acc =
let files = get_files s in
Hstr.fold (fun _key file acc -> fold_all_any s f acc (AFile file)) files acc
Hfile.fold (fun _key file acc -> fold_all_any s f acc (AFile file)) files acc
let rec fold_all_sub_goals_of_proofn s f acc pnid =
......@@ -495,14 +519,14 @@ let print_theory s fmt th : unit =
(Pp.print_list Pp.semi (fun fmt a -> print_proof_node s fmt a)) th.theory_goals
let print_file s fmt (file, thl) =
fprintf fmt "@[<hv 2> File %s;@ [%a]@]" file.file_name
fprintf fmt "@[<hv 2> File [%a];@ [%a]@]" print_file_path file.file_path
(Pp.print_list Pp.semi (print_theory s)) thl
let print_s s fmt =
fprintf fmt "@[%a@]" (Pp.print_list Pp.semi (print_file s))
let _print_session fmt s =
let l = Hstr.fold (fun _ f acc -> (f,f.file_theories) :: acc) (get_files s) [] in
let l = Hfile.fold (fun _ f acc -> (f,f.file_theories) :: acc) (get_files s) [] in
fprintf fmt "%a@." (print_s s) l;;
......@@ -518,13 +542,14 @@ let empty_session ?from dir =
next_proofNodeID = 0;
trans_table = Hint.create 97;
next_transID = 0;
next_fileID = 0;
session_dir = dir;
session_files = Hstr.create 3;
session_files = Hfile.create 3;
session_prover_ids = prover_ids;
session_raw_tasks = Hpn.create 97;
session_task_tables = Hpn.create 97;
session_sum_shape_table = Hpn.create 97;
file_state = Hstr.create 3;
file_state = Hfile.create 3;
th_state = Ident.Hid.create 7;
tn_state = Htn.create 97;
pn_state = Hpn.create 97;
......@@ -657,10 +682,10 @@ let th_proved s th =
b
let file_proved s f =
try Hstr.find s.file_state f.file_name
try Hfile.find s.file_state f.file_id
with Not_found ->
let b = f.file_theories = [] in
Hstr.add s.file_state f.file_name b;
Hfile.add s.file_state f.file_id b;
b
let pa_proved s paid =
......@@ -711,7 +736,7 @@ let update_file_node notification s f =
in
if proved <> file_proved s f then
begin
Hstr.replace s.file_state f.file_name proved;
Hfile.replace s.file_state f.file_id proved;
notification (AFile f);
end
......@@ -838,7 +863,7 @@ let remove_subtree ~(notification:notifier) ~(removed:notifier) s (n: any) =
match n with
| ATn tn -> remove_transformation s tn
| APa pa -> remove_proof_attempt_pa s pa
| AFile f -> Hstr.remove s.session_files f.file_name
| AFile f -> Hfile.remove s.session_files f.file_id
| APn pn ->
let node = Hint.find s.proofNode_table pn in
Hint.remove s.proofNode_table pn;
......@@ -1068,7 +1093,7 @@ and load_proof_or_transf session old_provers pid a =
"[Warning] Session.load_proof_or_transf: unexpected element '%s'@."
s
let load_theory session parent_name old_provers acc th =
let load_theory session parent_name old_provers (path,acc) th =
match th.Xml.name with
| "theory" ->
let thname = load_ident th in
......@@ -1085,26 +1110,40 @@ let load_theory session parent_name old_provers acc th =
th.Xml.elements goals;
let proved = bool_attribute "proved" th false in
Hid.add session.th_state thname proved;
mth::acc
(path,mth::acc)
| "path" ->
let fn = string_attribute "name" th in
(fn::path,acc)
| s ->
Warning.emit "[Warning] Session.load_theory: unexpected element '%s'@."
s;
acc
(path,acc)
let load_file session old_provers f =
match f.Xml.name with
| "file" ->
let fn = string_attribute "name" f in
let fn = string_attribute_opt "name" f in
let fmt = load_option "format" f in
let ft = List.rev
(List.fold_left
(load_theory session fn old_provers) [] f.Xml.elements) in
let mf = { file_name = fn;
let fid = gen_fileID session in
let path,ft =
List.fold_left
(load_theory session fid old_provers) ([],[]) f.Xml.elements
in
let path = match path,fn with
| [], Some fn ->
let l = Sysutil.system_independent_path_of_file fn in
Debug.dprintf debug "Loaded path from concrete file name: %a@." print_file_path l;
l
| [],None -> assert false
| p,_ -> List.rev p
in
let mf = { file_id = fid;
file_path = path;
file_format = fmt;
file_is_detached = true;
file_theories = ft;
file_theories = List.rev ft;
} in
Hstr.add session.session_files fn mf;
Hfile.add session.session_files fid mf;
old_provers
| "prover" ->
(* The id is just for the session file *)
......@@ -1553,21 +1592,25 @@ let make_theory_section ?merge ~detached (s:session) parent_name (th:Theory.theo
let add_file_section (s:session) (fn:string) ~file_is_detached
(theories:Theory.theory list) format : file =
let fn = Sysutil.relativize_filename s.session_dir fn in
Debug.dprintf debug "[Session_itp.add_file_section] fn = %s@." fn;
if Hstr.mem s.session_files fn then
Debug.dprintf debug "[Session_itp.add_file_section] fn = %a@." print_file_path fn;
(*
if Hfile.mem s.session_files fn then
begin
Printexc.print_backtrace stderr;
Format.eprintf "[session] FATAL: file %s already in database@." fn;
exit 2
end
else
let f = { file_name = fn;
*)
let fid = gen_fileID s in
let f = { file_id = fid;
file_path = fn;
file_format = format;
file_is_detached = file_is_detached;
file_theories = [] }
in
Hstr.add s.session_files fn f;
let theories = List.map (make_theory_section ~detached:false s fn) theories in