diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index 2fac146d0..b76474c34 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -771,7 +771,7 @@ module Make >>= fun v -> write_reg_op op sz rd v ii >>= fun () -> B.nextT - let do_read_mem sz = do_read_mem_op (M.op1 (Op.Mask sz)) sz + let do_read_mem sz = do_read_mem_op (uxt_op sz) sz let read_mem_acquire sz = do_read_mem sz Annot.A let read_mem_acquire_pc sz = do_read_mem sz Annot.Q diff --git a/herd/Pretty.ml b/herd/Pretty.ml index f77678bca..8ccdafa87 100644 --- a/herd/Pretty.ml +++ b/herd/Pretty.ml @@ -395,7 +395,8 @@ module Make (S:SemExtra.S) : S with module S = S = struct (fun ess iico -> let r = S.unions (iico::order_one_proc ess) and es = E.EventSet.unions ess in - E.EventRel.topo es r) + try E.EventRel.topo es r + with E.EventRel.Cyclic -> assert false) by_proc_and_poi iicos in let max = List.fold_left diff --git a/herd/eventsMonad.ml b/herd/eventsMonad.ml index 3d5098ff6..aa5a04517 100644 --- a/herd/eventsMonad.ml +++ b/herd/eventsMonad.ml @@ -45,6 +45,7 @@ and type evt_struct = E.event_structure) = let hexa = C.hexa let debug = C.debug let keep_failed_as_undetermined = C.variant Variant.ASL_AArch64 + let old_solver = C.variant Variant.OldSolver end) (A) diff --git a/herd/mem.ml b/herd/mem.ml index a9c1ee92d..39a236567 100644 --- a/herd/mem.ml +++ b/herd/mem.ml @@ -164,6 +164,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S = let kvm = C.variant Variant.VMSA let self = C.variant Variant.Ifetch let asl = C.variant Variant.ASL + let oota = C.variant Variant.OOTA let unroll = match C.unroll with | None -> Opts.unroll_default A.arch @@ -835,6 +836,8 @@ let match_reg_events es = (A.V.pp_v v_stored) ; assert false) rfm csn in + if C.debug.Debug_herd.solver then + prerr_endline "++ Solve registers" ; match VC.solve csn with | VC.NoSolns -> if C.debug.Debug_herd.solver then @@ -1077,6 +1080,8 @@ let match_reg_events es = loads stores cns in if dbg then eprintf "\n%!" ; (* And solve *) + if C.debug.Debug_herd.solver then + prerr_endline "++ Solve memory" ; match VC.solve cns with | VC.NoSolns -> if C.debug.Debug_herd.solver then begin @@ -1119,7 +1124,6 @@ let match_reg_events es = let module PP = Pretty.Make(S) in prerr_endline "Unsolvable system" ; PP.show_es_rfm test es rfm ; - prerr_endline "Unsolvable system" end ; assert (true || rfmap_is_cyclic es rfm); res @@ -2068,7 +2072,8 @@ Please use `-variant self` as an argument to herd7 to enable it." match cs with | _::_ when - (not C.initwrites || not do_deps) + (not oota) + && (not C.initwrites || not do_deps) && not asl && Misc.is_none ofail -> diff --git a/herd/partition.ml b/herd/partition.ml index 5b077a553..080b19b93 100644 --- a/herd/partition.ml +++ b/herd/partition.ml @@ -21,7 +21,7 @@ module Make (O:Set.OrderedType) : sig (* All creation steps must preceed union/find operations *) val create : unit -> t - val add : t -> O.t -> t + val add : O.t -> t -> t (* Union/Find *) val find : t -> O.t -> O.t @@ -44,7 +44,7 @@ end = struct (* Creation *) let create () = M.empty - let add m x = + let add x m = let rec c = { value=x; rank=0; parent=c; } in M.add x c m diff --git a/herd/partition.mli b/herd/partition.mli index e25cdba43..b9bc5db70 100644 --- a/herd/partition.mli +++ b/herd/partition.mli @@ -21,7 +21,7 @@ module Make (O:Set.OrderedType) : sig (* All creation steps must precede union/find operations *) val create : unit -> t - val add : t -> O.t -> t + val add : O.t -> t -> t (* Union/Find *) val find : t -> O.t -> O.t diff --git a/herd/tests/instructions/C/C13.litmus b/herd/tests/instructions/C/C13.litmus new file mode 100644 index 000000000..ebe5d1626 --- /dev/null +++ b/herd/tests/instructions/C/C13.litmus @@ -0,0 +1,22 @@ +C C13 +(* Forbidden by rc11, allowed by most C11 models that tolerate oota *) +{ +x = 0; +y = 0; +} + +P0(atomic_int *x, atomic_int *y) { + int r1 = atomic_load_explicit(y, memory_order_relaxed); + atomic_store_explicit(x, r1, memory_order_relaxed); + int r2 = (r1^r1)+r1; +} + +P1(atomic_int *x, atomic_int *y) { + int r4 = atomic_load_explicit(x, memory_order_relaxed); + atomic_store_explicit(y, r4, memory_order_relaxed); +} + +locations [0:r2; 1:r4;] +exists 0:r1 != 0 + + diff --git a/herd/tests/instructions/C/C13.litmus.expected b/herd/tests/instructions/C/C13.litmus.expected new file mode 100644 index 000000000..fb445e2de --- /dev/null +++ b/herd/tests/instructions/C/C13.litmus.expected @@ -0,0 +1,10 @@ +Test C13 Allowed +States 1 +0:r1=0x0; 0:r2=0x0; 1:r4=0x0; +No +Witnesses +Positive: 0 Negative: 3 +Condition exists (not (0:r1=0x0)) +Observation C13 Never 0 3 +Hash=45b06aedc4caf5ef4fdf494a986f8199 + diff --git a/herd/valconstraint.ml b/herd/valconstraint.ml index a768ecab3..670a1fb41 100644 --- a/herd/valconstraint.ml +++ b/herd/valconstraint.ml @@ -1,5 +1,5 @@ (****************************************************************************) -(* the diy toolsuite *) +(* The diy toolsuite *) (* *) (* Jade Alglave, University College London, UK. *) (* Luc Maranget, INRIA Paris-Rocquencourt, France. *) @@ -14,7 +14,14 @@ (* "http://www.cecill.info". We also give a copy in LICENSE.txt. *) (****************************************************************************) -(** A simple constraint solver *) +(** A simple constraint solver. The default solver + * [solve_topo] proceeds by one pass by following dependencies, while + * the previous solver [solve_std] proceeds by iterating substitution + * and computation steps untill stabilisation. + * Both solvers are invoked after a "normalisation" step that + * identifies classes of equivant variables resulting from equations + * of the form [x := y], see [normalise_vars] below. + *) (* Constraints: v is any value: a constant cst or a variable S. Possible constraints are @@ -68,6 +75,7 @@ module type Config = sig val hexa : bool val debug : Debug_herd.t val keep_failed_as_undetermined : bool + val old_solver : bool end module Make (C:Config) (A:Arch_herd.S) : S @@ -190,28 +198,33 @@ and type state = A.state = type t = V.csym let compare = V.compare_csym end + module Part = Partition.Make (OV) - let add_var t v = match v with - | V.Val _ -> t - | V.Var x -> Part.add t x + let fold_var f = function + | V.Val _ -> Fun.id + | V.Var x -> f x - let add_var_loc t loc = match A.undetermined_vars_in_loc_opt loc with - | None -> t - | Some v -> add_var t v + let fold_loc f loc = + match A.undetermined_vars_in_loc_opt loc with + | None -> Fun.id + | Some v -> fold_var f v - let add_vars_expr t e = match e with - | Atom v -> add_var t v - | ReadInit (loc,_) -> add_var_loc t loc - | Unop (_,v) -> add_var t v - | Binop (_,v1,v2) -> - add_var (add_var t v1) v2 - | Terop (_,v1,v2,v3) -> - add_var (add_var (add_var t v1) v2) v3 + let fold_vars_expr f e t = match e with + | Atom v -> fold_var f v t + | ReadInit (loc,_) -> fold_loc f loc t + | Unop (_,v) -> fold_var f v t + | Binop (_,v1,v2) -> + fold_var f v1 t |> fold_var f v2 + | Terop (_,v1,v2,v3) -> + fold_var f v1 t |> fold_var f v2 |> fold_var f v3 + + let add_vars_expr = fold_vars_expr Part.add + and add_var = fold_var Part.add let add_vars_cn t cn = match cn with | Assign (v,e) -> - add_vars_expr (add_var t v) e + add_var v t |> add_vars_expr e | Failed _ | Warn _ -> t let add_vars_cns cns = List.fold_left add_vars_cn (Part.create ()) cns @@ -252,6 +265,14 @@ and type state = A.state = (* All together *) + (** [normalise cns], where [cns] is a list of equations, + * that is, compute equivalence classes of variables and + * replace variables by their representative. + * The function returns a pair [(m,cns)], where cns collects + * the new equations, with equations [x := y] removed and + * variables replaced by representative. The mapping [m] + * is from variables to representative. + *) let normalize_vars cns = let t = add_vars_cns cns in let m = uf_cns t cns in @@ -261,7 +282,6 @@ and type state = A.state = end ; m,cns - (*****************) (* Solver proper *) (*****************) @@ -287,6 +307,7 @@ and type state = A.state = | A.LocUndetermined | V.Undetermined -> e + let check_true_false cn k = match cn with | Assign (v,e) -> begin @@ -299,8 +320,8 @@ and type state = A.state = else raise Contradiction else Assign (v,e)::k - | ReadInit _ - | Unop _|Binop _|Terop _ -> Assign (v,e)::k + | ReadInit _| Unop _|Binop _|Terop _ -> + Assign (v,e)::k end (* Delay failure to preserve potential contradiction *) with @@ -324,12 +345,12 @@ and type state = A.state = (* Phase 3, substitution *) + let simplify_vars_in_var soln x = + try V.Val (V.Solution.find x soln) + with Not_found -> V.Var x + let simplify_vars_in_atom soln v = - V.map_csym - (fun x -> - try V.Val (V.Solution.find x soln) - with Not_found -> V.Var x) - v + V.map_csym (simplify_vars_in_var soln) v let simplify_vars_in_expr soln = map_expr (simplify_vars_in_atom soln) @@ -341,7 +362,6 @@ and type state = A.state = Assign (v,rval) | Failed _ | Warn _ -> cn - let simplify_vars_in_cnstrnts soln cs = List.map (simplify_vars_in_cnstrnt soln) cs @@ -363,22 +383,20 @@ and type state = A.state = | Failed _ | Warn _ -> empty (* merge of solutions, with consistency check *) - let merge sol1 sol2 = - V.Solution.fold - (fun v i k -> - try - let i' = V.Solution.find v sol2 in - if V.Cst.compare i i' = 0 then - V.Solution.add v i k - else - raise Contradiction - with Not_found -> V.Solution.add v i k) - sol1 sol2 + let add_sol x cst sol = + try + let cst' = V.Solution.find x sol in + if V.Cst.eq cst cst' then sol + else raise Contradiction + with + | Not_found -> V.Solution.add x cst sol -let solve_cnstrnts = - List.fold_left - (fun solns cnstr -> merge (solve_cnstrnt cnstr) solns) - V.Solution.empty + let merge sol1 sol2 = V.Solution.fold add_sol sol1 sol2 + + let solve_cnstrnts = + List.fold_left + (fun solns cnstr -> merge (solve_cnstrnt cnstr) solns) + V.Solution.empty (************************) (* Raise exceptions now *) @@ -424,7 +442,7 @@ let get_failed cns = m (V.Solution.map (fun x -> V.Val x) solns0) - let solve lst = + let solve_std lst = if debug_solver then begin prerr_endline "** Solve **" ; eprintf "%s\n" (pp_cnstrnts lst) ; flush stderr @@ -445,4 +463,213 @@ let get_failed cns = (* Topological sort-based solver *) (*********************************) + module OrderedEq = struct + type t = cnstrnt + + let atom_compare = A.V.compare + + let atom2_compare p1 p2 = + Misc.pair_compare atom_compare atom_compare p1 p2 + + let atom3_compare (e1,e2,e3) (f1,f2,f3) = + Misc.pair_compare + atom_compare atom2_compare (e1,(e2,e3)) (f1,(f2,f3)) + + let expr_compare e1 e2 = match e1,e2 with + | Atom v1,Atom v2 -> atom_compare v1 v2 + | ReadInit (loc1,_),ReadInit (loc2,_) -> + A.location_compare loc1 loc2 (* second componant is fixed *) + | Unop (op1,e1),Unop (op2,e2) -> + Misc.pair_compare + Misc.polymorphic_compare + atom_compare + (op1,e1) (op2,e2) + | Binop (o,e1,e2),Binop (p,f1,f2) -> + Misc.pair_compare + Misc.polymorphic_compare + atom2_compare + (o,(e1,e2)) (p,(f1,f2)) + | Terop (o,e1,e2,e3),Terop (p,f1,f2,f3) -> + Misc.pair_compare + Misc.polymorphic_compare + atom3_compare + (o,(e1,e2,e3)) (p,(f1,f2,f3)) + | (Atom _,(ReadInit _|Unop _|Binop _|Terop _)) + | (ReadInit _,(Unop _|Binop _|Terop _)) + | (Unop _,(Binop _|Terop _)) + | (Binop _,Terop _) + -> -1 + | ((ReadInit _|Unop _|Binop _|Terop _),Atom _) + | ((Unop _|Binop _|Terop _),ReadInit _) + | ((Binop _|Terop _),Unop _) + | (Terop _,Binop _) + -> 1 + + let compare c1 c2 = match c1,c2 with + | Assign (v1,e1),Assign (v2,e2) -> + Misc.pair_compare + atom_compare + expr_compare + (v1,e1) (v2,e2) + | Failed exn1,Failed exn2 -> + Misc.polymorphic_compare exn1 exn2 + | Warn w1,Warn w2 -> + String.compare w1 w2 + | (Assign _,(Failed _|Warn _)) + | (Failed _,Warn _) + -> -1 + | ((Failed _|Warn _),Assign _) + | (Warn _,Failed _) + -> 1 + end + + module EqSet = MySet.Make(OrderedEq) + + module VarEnv = A.V.Solution + + let env_find csym m = + try VarEnv.find csym m with Not_found -> EqSet.empty + + let env_add csym c = + VarEnv.update csym @@ + function + | None -> Some (EqSet.singleton c) + | Some old -> Some (EqSet.add c old) + + let var2eq cs = + (* Construct the map from x to all equations of the form [x = ] *) + List.fold_left + (fun m c -> + match c with + | Assign (V.Var csym,_) -> env_add csym c m + | Assign (V.Val _,_)|Warn _|Failed _ -> m) + VarEnv.empty cs + + module EqRel = InnerRel.Make(OrderedEq) + + let debug_topo chan ns r = + EqRel.scc_kont + (fun cs () -> + Printf.fprintf chan "{%s}\n%!" + (List.map pp_cnstrnt cs |> String.concat ", ")) + () + ns r + + let eq2g cs = + let cs = + List.map + (fun c -> + match c with + | Assign (V.Val _ as c,Atom (V.Var _ as y)) -> + Assign (y,Atom c) + | _ -> c) + cs in + let m = var2eq cs in + let add_rels eq0 e g = + let add_rel csym g = + let eqs = env_find csym m in + EqSet.fold (fun eq g -> EqRel.add (eq0,eq) g) eqs g in + fold_vars_expr add_rel e g in + + let rel = + List.fold_left + (fun rel c -> + match c with + | Assign (_,e) -> add_rels c e rel + | Warn _|Failed _ -> rel) + EqRel.empty cs in + let cs = EqSet.of_list cs in + cs,rel + + (** [solv_one c sol eqs], where c is an equation, [sol] is a solution + * (map from variables to constants) and [eqs] is a list of equations, + * evaluates the equation [c] w.r.t. to solution [sol] + * and returns [(sol,eqs)] updated, with: + * - [sol] updated to add all the variable affections found; + * - [eqs] updated to add the unsolved equations. + *) + let solve_one c sol eqs = + match c with + | Warn _|Failed _ -> sol,c::eqs + | Assign (v0,e) -> + begin + try + let v = simplify_vars_in_atom sol v0 + and e = simplify_vars_in_expr sol e |> mk_atom_from_expr in + match v,e with + | V.Var x,Atom (V.Val atom) -> + add_sol x atom sol,eqs + | V.Val c1,Atom (V.Val c2) -> + if V.Cst.eq c1 c2 then sol,eqs + else raise Contradiction + (* Last case below can occur when called on a + strongly connected component. *) + | _,_ -> sol,Assign (v,e)::eqs + with + | Contradiction|Misc.Timeout as exn -> raise exn + | exn -> (sol,Failed exn::eqs) + end + + let topo_step cs (sol,eqs) = + match cs with + | [] -> assert false + | [c] -> solve_one c sol eqs + | scc -> + (* Attempt to partial solve *) + List.fold_left + (fun (sol,scc) c -> solve_one c sol scc) + (sol,eqs) scc + + (** [solve_top_step [cs] tries to solve the system [cs] by sorting [cs] + * topologically, returns [(sol,cs,sccs)], where + * - [sol] is the "solution" resulting from the propagation of + * solved equations x = cst; + * - [cs] are fake equations such as delayed warnings; + * - [sccs] are unsolved recusive equations at the end. + * Raises `Contradiction` in case solving equations results in + * some contradictory equation cst = cst` + *) + let solve_topo_step cs = + let ns,r = eq2g cs in + if debug_solver then begin + if false then begin + prerr_endline "** Solve topo **" ; + eprintf "%s\n%!" (pp_cnstrnts cs) ; + prerr_endline "** Graph **" ; + EqRel.pp stderr "" + (fun chan (c1,c2) -> + fprintf chan "(%s) <- (%s)\n" + (pp_cnstrnt c1) (pp_cnstrnt c2)) + r + end ; + eprintf "** Equations **\n%!" ; + eprintf "%s\n" (pp_cnstrnts cs) ; flush stderr ; + eprintf "** Equations ordered**\n%!" ; + debug_topo stderr ns r + end ; + EqRel.scc_kont topo_step (V.Solution.empty,[]) ns r + + let solve_topo cs = + (* Replace equivalent variables by a class representative *) + let m,cs = normalize_vars cs in + let sol = + try + (* Solve in one scan *) + let sol,cs = solve_topo_step cs in + (* Add solutions of the form x := y *) + let sol = add_vars_solns m sol in + Maybe (sol,cs) + with + | Contradiction -> NoSolns in + if debug_solver then begin + eprintf "Solutions: %s\n" (pp_answer sol) ; flush stderr + end ; + sol + + let solve cs = + if C.old_solver then + solve_std cs + else + solve_topo cs + end diff --git a/herd/variant.ml b/herd/variant.ml index 14ccf60e7..6809bb543 100644 --- a/herd/variant.ml +++ b/herd/variant.ml @@ -97,6 +97,10 @@ type t = (* Telechat variant - implements unconditional branches as exit, and any other optional quirks*) | Telechat | NV2 +(* Old solver, replaced by substitution following toplogical sort *) + | OldSolver + (* Accept cyclic equation sets as being solvable *) + | OOTA let tags = ["success";"instr";"specialx0";"normw";"acqrelasfence";"backcompat"; @@ -107,7 +111,7 @@ let tags = "pte-squared"; "PhantomOnLoad"; "OptRfRMW"; "ConstrainedUnpredictable"; "exp"; "self"; "cos-opt"; "test"; "T[0-9][0-9]"; "asl"; "strict"; "warn"; "S128"; "ASLType+Warn"; "ASLType+Silence"; "ASLType+Check"; - "ASL+Experimental";] + "ASL+Experimental"; "telechat"; "OldSolver"; "oota";] let parse s = match Misc.lowercase s with | "success" -> Some Success @@ -162,6 +166,8 @@ let parse s = match Misc.lowercase s with | "warn" -> Some Warn | "telechat" -> Some Telechat | "nv2" | "NV2" -> Some NV2 +| "oldsolver" -> Some OldSolver +| "oota" -> Some OOTA | s -> begin match Fault.Handling.parse s with @@ -237,6 +243,8 @@ let pp = function | ASLExperimental -> "ASL+Experimental" | Telechat -> "telechat" | NV2 -> "NV2" + | OldSolver -> "OldSolver" + | OOTA -> "oota" let compare = compare let equal v1 v2 = compare v1 v2 = 0 diff --git a/herd/variant.mli b/herd/variant.mli index f26bb65d1..9a704db89 100644 --- a/herd/variant.mli +++ b/herd/variant.mli @@ -95,8 +95,14 @@ type t = | Strict (* Semi-strict interpretation of variant, e.g. -variant asl,warn *) | Warn +(* Telechat variant - implements unconditional branches as exit, and any other optional quirks*) | Telechat | NV2 +(* Old solver, new solver proceeds by substitution following toplogical sort *) + | OldSolver +(* Accept cyclic equation sets as being solvable *) + | OOTA + val compare : t -> t -> int val equal : t -> t -> bool diff --git a/lib/innerRel.ml b/lib/innerRel.ml index b401c9bb9..a91d27782 100644 --- a/lib/innerRel.ml +++ b/lib/innerRel.ml @@ -92,10 +92,12 @@ module type S = sig val cycle_to_rel : elt0 list -> t val cycle_option_to_rel : elt0 list option -> t - exception Cyclic (* Topological sort *) + exception Cyclic + val topo_kont : (elt0 -> 'a -> 'a) -> 'a -> Elts.t -> t -> 'a val topo : Elts.t -> t -> elt0 list + val pseudo_topo_kont : (elt0 -> 'a -> 'a) -> 'a -> Elts.t -> t -> 'a (****************************************************) (* Continuation based all_topos (see next function) *) @@ -114,6 +116,10 @@ module type S = sig val all_topos : bool (* verbose *)-> Elts.t -> t -> elt0 list list +(* Strongly connected compoments, processed in inverse dependency order. *) + val scc_kont : (elt0 list -> 'a -> 'a) -> 'a -> Elts.t -> t -> 'a + + (* Is the parent relation of a hierarchy *) val is_hierarchy : Elts.t -> t -> bool @@ -365,7 +371,6 @@ and module Elts = MySet.Make(O) = None with Cycle e -> Some (List.rev e) - let fold = ME.fold (***************) (* Reachablity *) @@ -491,29 +496,45 @@ and module Elts = MySet.Make(O) = | None -> empty | Some cy -> cycle_to_rel cy - +(********************) (* Topological sort *) +(********************) exception Cyclic - let topo all_nodes t = + let topo_kont kont res all_nodes t = let m = M.to_map t in let rec dfs above n (o,seen as r) = if Elts.mem n above then raise Cyclic else if Elts.mem n seen then r else - let o,seen = + let res,seen = Elts.fold (dfs (Elts.add n above)) (M.succs n m) (o,Elts.add n seen) in - n::o,seen in - let all_succs = - Elts.unions - (M.fold (fun _ ns k -> ns::k) m []) in - let ns = Elts.diff all_nodes all_succs in - let o,_ = + kont n res,seen in + let ns = all_nodes in + let o,_seen = Elts.fold - (dfs Elts.empty) ns ([],Elts.empty) in + (dfs Elts.empty) ns (res,Elts.empty) in + (* Some node has not been visited, we have a cycle *) o + let topo all_nodes t = topo_kont Misc.cons [] all_nodes t + + + let pseudo_topo_kont kont res all_nodes t = + let m = M.to_map t in + let rec dfs n (res,seen as r) = + if Elts.mem n seen then r + else + let res,seen = + Elts.fold dfs + (M.succs n m) (res,Elts.add n seen) in + kont n res,seen in + (* Search graph from non-successors *) + let ns = all_nodes in + let res,_ = Elts.fold dfs ns (res,Elts.empty) in + res + (* New version of all_topos *) module EMap = Map.Make @@ -599,6 +620,71 @@ and module Elts = MySet.Make(O) = end ; nss +(* + * Strongly connected compponets, Tarjan's algorithm. + * From R. Sedgwick's book "Algorithms". + *) + module SCC = struct + module NodeMap = M.ME + + type state = + { id : int; + visit : int NodeMap.t; + stack : elt0 list; } + + let rec pop_until n ns = + match ns with + | [] -> assert false + | m::ns -> + if O.compare n m = 0 then [m],ns + else + let ms,ns = pop_until n ns in + m::ms,ns + + let zyva kont res nodes edges = + + let m = M.to_map edges in + + let rec dfs n ((res,s) as r) = + try + NodeMap.find n s.visit,r + with + | Not_found -> + let min = s.id in + let s = { + id = min + 1; + visit = NodeMap.add n min s.visit; + stack = n :: s.stack; + } in + let min,(res,s) as r = + Elts.fold + (fun n (m0,r) -> + let m1,r = dfs n r in Misc.min_int m0 m1,r) + (M.succs n m) + (min,(res,s)) in + let valk = + try NodeMap.find n s.visit with Not_found -> assert false in + if not (Misc.int_eq min valk) then + r (* n is part of previously returned scc *) + else + let scc,stack = pop_until n s.stack in + let visit = + List.fold_left + (fun visit n -> NodeMap.add n max_int visit) + s.visit scc in + let res = kont scc res in + min,(res,{ s with stack; visit; }) in + + let (res,_) = + Elts.fold + (fun n r -> let _,r = dfs n r in r) + nodes + (res,{id=0; visit=NodeMap.empty; stack=[];} ) in + res + end + + let scc_kont kont res nodes edges = SCC.zyva kont res nodes edges + (* Is the parent relation of a hierarchy *) let is_hierarchy nodes edges = is_acyclic edges && diff --git a/lib/innerRel.mli b/lib/innerRel.mli index 3532ce2a6..8951b9c50 100644 --- a/lib/innerRel.mli +++ b/lib/innerRel.mli @@ -94,16 +94,27 @@ module type S = sig val cycle_option_to_rel : elt0 list option -> t -(* All toplogical orders, raises Cyclic in case of cycle - Enhancement: all_topos nodes edges still works - when edges relates elts not in nodes *) + (* All toplogical order computing functions + raise Cyclic in case of cycle *) exception Cyclic + (* One topoligical order *) + val topo_kont : (elt0 -> 'a -> 'a) -> 'a -> Elts.t -> t -> 'a val topo : Elts.t -> t -> elt0 list + +(* By exception to the general rule, + The function [pseudo_topo_kont] does not + fail. Instead, it acts as if the backward edge + it discovers is non-existent *) + val pseudo_topo_kont : (elt0 -> 'a -> 'a) -> 'a -> Elts.t -> t -> 'a + (****************************************************) (* Continuation based all_topos (see next function) *) (****************************************************) +(* Enhancement: all_topos nodes edges still works + when edges relates elts not in nodes *) + (* Orders as a lists *) val all_topos_kont : Elts.t -> t -> (elt0 list -> 'a -> 'a) -> 'a -> 'a (* Orders as relations *) @@ -115,6 +126,9 @@ module type S = sig when edges relates elts not in nodes *) val all_topos : bool (* verbose *)-> Elts.t -> t -> elt0 list list +(* Strongly connected components, processed in inverse dependency order. *) + val scc_kont : (elt0 list -> 'a -> 'a) -> 'a -> Elts.t -> t -> 'a + (* Is the parent relation of a hierarchy *) val is_hierarchy : Elts.t -> t -> bool diff --git a/lib/misc.ml b/lib/misc.ml index da5bdf8dd..d39dee724 100644 --- a/lib/misc.ml +++ b/lib/misc.ml @@ -47,6 +47,7 @@ let polymorphic_compare = compare let int_compare = Int.compare let int_eq = Int.equal let max_int (x:int) (y:int) = if x >= y then x else y +let min_int (x:int) (y:int) = if x <= y then x else y let string_eq = String.equal let bool_eq = Bool.equal let identity = Fun.id diff --git a/lib/misc.mli b/lib/misc.mli index d3ccf04ca..6c3d33019 100644 --- a/lib/misc.mli +++ b/lib/misc.mli @@ -48,6 +48,7 @@ val polymorphic_compare : 'a -> 'a -> int val int_compare : int -> int -> int val int_eq : int -> int -> bool val max_int : int -> int -> int +val min_int : int -> int -> int val string_eq : string -> string -> bool val bool_eq : bool -> bool -> bool diff --git a/lib/symbValue.ml b/lib/symbValue.ml index 0a9b4caea..bd9d5926c 100644 --- a/lib/symbValue.ml +++ b/lib/symbValue.ml @@ -50,8 +50,9 @@ module type csym = int let pp_csym i = sprintf "S%i" i - let compare_csym v1 v2 = Misc.int_compare v1 v2 let equal_csym v1 v2 = v1 == v2 + let compare_csym v1 v2 = Misc.int_compare v1 v2 + type cst = Cst.v diff --git a/lib/value.mli b/lib/value.mli index b2ec9ceff..9636a03f5 100644 --- a/lib/value.mli +++ b/lib/value.mli @@ -34,6 +34,7 @@ module type S = (* flexible variables *) type csym = int (* Opened by Susmit, lose pointless abstraction *) val pp_csym : csym -> string + val equal_csym : csym -> csym -> bool val compare_csym : csym -> csym -> int (* Values, ie constants + variables, that should be instanciated