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 493c10c5 authored by MARCHE Claude's avatar MARCHE Claude

Removed the offending Obj.magic

parent 208b5f5a
......@@ -2022,57 +2022,14 @@ let print_external_proof fmt p =
(** Pairing *)
module AssoGoals : sig
val set_use_shapes : bool -> unit
val associate :
'a goal list -> 'b goal list ->
('b goal * ('a goal * bool) option) list * 'a goal list
end = struct
(** When Why3 will require 3.12 put all of that in a function using
explicit type argument "(type t)" and remove all the Obj.magic *)
module ToGoal = struct
(** The functor can't be instantiated with an 'a t so we will give
a t *)
type tto (** will represent any type *)
type t = tto goal
let checksum g = g.goal_checksum
let shape g = g.goal_shape
let name g = g.goal_name
module Goal = struct
type 'a t = 'a goal
let checksum g = g.goal_checksum
let shape g = g.goal_shape
let name g = g.goal_name
end
module FromGoal = struct
(** The functor can't be instantiated with an 'a t so we will give
a t *)
type ffrom (** will represent any type *)
type t = ffrom goal
let checksum g = g.goal_checksum
let shape g = g.goal_shape
let name g = g.goal_name
end
module AssoGoals = Tc.Pairing(FromGoal)(ToGoal)
open ToGoal
open FromGoal
let use_shapes = ref true
let set_use_shapes b = use_shapes := b
let associate
(from_goals: 'ffrom goal list) (to_goals: 'tto goal list) :
('tto goal * ('ffrom goal * bool) option) list * 'ffrom goal list =
let from_goals : ffrom goal list =
Obj.magic (from_goals : 'ffrom goal list) in
let to_goals : tto goal list =
Obj.magic (to_goals : 'tto goal list) in
let associated :
(tto goal * (ffrom goal * bool) option) list * ffrom goal list =
AssoGoals.associate
~use_shapes:!use_shapes from_goals to_goals
in
(Obj.magic associated :
('tto goal * ('ffrom goal * bool) option) list * ('ffrom goal list))
end
module AssoGoals = Tc.Pairing(Goal)(Goal)
(**********************************)
(* merge a file into another *)
......@@ -2328,7 +2285,7 @@ and merge_trans ~ctxt ~theories env to_goal _ from_transf =
let associated,detached =
Debug.dprintf debug "[Info] associate_subgoals, shape_version = %d@\n"
env.session.session_shape_version;
AssoGoals.associate
AssoGoals.associate ~use_shapes:ctxt.use_shapes_for_pairing_sub_goals
from_transf.transf_goals to_transf.transf_goals
in
List.iter (function
......@@ -2500,7 +2457,9 @@ let recompute_all_shapes ~release session =
let update_session ~ctxt old_session env whyconf =
Debug.dprintf debug "[Info] update_session: shape_version = %d@\n"
old_session.session_shape_version;
(*
AssoGoals.set_use_shapes ctxt.use_shapes_for_pairing_sub_goals;
*)
let new_session =
create_session ~shape_version:old_session.session_shape_version
old_session.session_dir
......@@ -2666,7 +2625,7 @@ and add_transf_to_goal ~keygen env to_goal from_transf =
let associated,detached =
Debug.dprintf debug "[Info] associate_subgoals, shape_version = %d@\n"
env.session.session_shape_version;
AssoGoals.associate
AssoGoals.associate ~use_shapes:false
from_transf.transf_goals to_transf.transf_goals in
List.iter (function
| (to_goal, Some (from_goal, _obsolete)) ->
......
......@@ -676,10 +676,10 @@ let theory_checksum ?(version=current_shape_version) t =
*)
module type S = sig
type t
val checksum : t -> checksum option
val shape : t -> string
val name : t -> Ident.ident
type 'a t
val checksum : 'a t -> checksum option
val shape : 'a t -> string
val name : 'a t -> Ident.ident
end
module Pairing(Old: S)(New: S) = struct
......@@ -691,21 +691,30 @@ module Pairing(Old: S)(New: S) = struct
open Ident
type any_goal = Old of Old.t | New of New.t
type goal_index = Old of int | New of int
type ('a,'b) goal_table = {
table_old : 'a Old.t array;
table_new : 'b New.t array;
}
(* doubly linked lists; left and right bounds point to themselves *)
type node = {
mutable prev: node;
shape: string;
elt: any_goal;
elt: goal_index;
mutable valid: bool;
mutable next: node;
}
let mk_node g =
let s = match g with Old g -> Old.shape g | New g -> New.shape g in
let rec n = { prev = n; shape = s; elt = g; next = n; valid = true } in n
let mk_node table g =
let s = match g with
| Old g -> Old.shape table.table_old.(g)
| New g -> New.shape table.table_new.(g)
in
let rec n = { prev = n; shape = s; elt = g; next = n; valid = true }
in n
let rec iter_pairs f = function
| [] | [_] -> ()
......@@ -731,39 +740,52 @@ module Pairing(Old: S)(New: S) = struct
let dprintf = Debug.dprintf debug
let associate oldgoals newgoals =
let table = {
table_old = Array.of_list oldgoals;
table_new = Array.of_list newgoals;
}
in
(* set up an array [result] containing the solution
[new_goal_index g] returns the index of goal [g] in that array *)
let new_goal_index = Hid.create 17 in
let result =
let make i newg =
Hid.add new_goal_index (New.name newg) i; (newg, None) in
Array.mapi make (Array.of_list newgoals) in
Hid.add new_goal_index (New.name newg) i; (newg, None)
in
Array.mapi make table.table_new
in
let new_goal_index newg =
try Hid.find new_goal_index (New.name newg)
with Not_found -> assert false in
(* phase 1: pair goals with identical checksums *)
let old_checksums = Hashtbl.create 17 in
let add acc oldg = match Old.checksum oldg with
| None -> mk_node (Old oldg) :: acc
| Some s -> Hashtbl.add old_checksums s oldg; acc
in
let old_goals_without_checksum =
List.fold_left add [] oldgoals
let acc =ref [] in
for oldg = 0 to Array.length table.table_old - 1 do
match Old.checksum table.table_old.(oldg) with
| None -> acc := mk_node table (Old oldg) :: !acc
| Some s -> Hashtbl.add old_checksums s oldg
done;
!acc
in
let collect acc newg =
try
match New.checksum newg with
| None -> raise Not_found
| Some c ->
let oldg = Hashtbl.find old_checksums c in
Hashtbl.remove old_checksums c;
result.(new_goal_index newg) <- (newg, Some (oldg, false));
acc
with Not_found ->
mk_node (New newg) :: acc
let newgoals =
let acc = ref old_goals_without_checksum in
for newi = 0 to Array.length table.table_new - 1 do
try
let newg = table.table_new.(newi) in
match New.checksum newg with
| None -> raise Not_found
| Some c ->
let oldi = Hashtbl.find old_checksums c in
let oldg = table.table_old.(oldi) in
Hashtbl.remove old_checksums c;
result.(new_goal_index newg) <- (newg, Some (oldg, false))
with Not_found ->
acc := mk_node table (New newi) :: !acc
done;
!acc
in
let newgoals = List.fold_left collect old_goals_without_checksum newgoals in
let add _ oldg acc = mk_node (Old oldg) :: acc in
let add _ oldg acc = mk_node table (Old oldg) :: acc in
let allgoals = Hashtbl.fold add old_checksums newgoals in
Hashtbl.clear old_checksums;
(* phase 2: pair goals according to shapes *)
......@@ -784,7 +806,9 @@ module Pairing(Old: S)(New: S) = struct
let o, n = match x.elt, y.elt with
| New n, Old o | Old o, New n -> o, n | _ -> assert false in
dprintf "[assoc] new pairing@.";
result.(new_goal_index n) <- n, Some (o, true);
let newg = table.table_new.(n) in
let oldg = table.table_old.(o) in
result.(new_goal_index newg) <- newg, Some (oldg, true);
if x.prev != x && y.next != y then add x.prev y.next;
remove x;
remove y
......@@ -796,7 +820,7 @@ module Pairing(Old: S)(New: S) = struct
(fun acc x ->
if x.valid then
match x.elt with
| Old g -> g :: acc
| Old g -> table.table_old.(g) :: acc
| New _ -> acc
else acc)
[] allgoals
......
......@@ -46,23 +46,19 @@ val buffer_checksum : Buffer.t -> checksum
val task_checksum : ?version:int -> Task.task -> checksum
(* not used anymore
val theory_checksum : ?version:int -> Theory.theory -> checksum
*)
(** Pairing algorithm *)
module type S = sig
type t
val checksum : t -> checksum option
val shape : t -> shape
val name : t -> Ident.ident
type 'a t
val checksum : 'a t -> checksum option
val shape : 'a t -> shape
val name : 'a t -> Ident.ident
end
module Pairing(Old: S)(New: S) : sig
val associate:
use_shapes:bool -> Old.t list -> New.t list ->
(New.t * (Old.t * bool) option) list * Old.t list
use_shapes:bool -> 'a Old.t list -> 'b New.t list ->
('b New.t * ('a Old.t * bool) option) list * 'a Old.t list
(** Associate new goals to (possibly) old goals
Each new goal is mapped either to
- [None]: no old goal associated
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment