[gen] Minor change on functions in code.ml

- Remove `assert false` in `code.ml`.
- Introduce `is_diff_loc`
- Change `seq_sd` return `option`.

Author: Shale Xiong

gen/alt.ml

@@ -70,6 +70,10 @@ module Make(C:Builder.S)
           (fun f -> List.exists (equal_fence f) fs)
 
     let choice_sc po_safe e1 e2 =
+      let seq_sd e1 e2 =
+        match Code.seq_sd e1 e2 with
+        | None -> Warn.user_error "Unexpected UnspecLoc"
+        | Some b -> b in
       let r = match e1.edge,e2.edge with
 (*
   Now accept internal with internal composition
@@ -564,7 +568,7 @@ module Make(C:Builder.S)
 
     let count_ext es = count_e 0 es
 
-    let change_loc e = not @@ Code.is_same_loc @@ loc_sd e
+    let change_loc e = Code.is_diff_loc @@ loc_sd e
 
     let count_p p =
       List.fold_left ( fun acc x -> if p x then acc + 1 else acc ) 0

gen/common/code.ml

@@ -97,18 +97,21 @@ let pp_sd = function
 
 let is_same_loc = function
   | Same -> true
-  | Diff -> false
-  | UnspecLoc -> assert false
+  | _ -> false
+
+let is_diff_loc = function
+  | Diff -> true
+  | _ -> false
 
-let is_both_loc = function
+let is_unspec_loc = function
   | UnspecLoc -> true
   | _ -> false
 
 let seq_sd sd1 sd2 =
   match sd1,sd2 with
-  | UnspecLoc,_|_, UnspecLoc -> assert false
-  | Same,Same -> Same
-  | Diff,_|_,Diff -> Diff
+  | UnspecLoc,_|_, UnspecLoc -> None
+  | Same,Same -> Some Same
+  | Diff,_|_,Diff -> Some Diff
 
 let fold_ie wildcard f r = let r = if wildcard then (f UnspecCom r) else r in f Ext (f Int r)
 let fold_sd wildcard f r = let r = if wildcard then (f UnspecLoc r) else r in f Diff (f Same r)

gen/common/code.mli

@@ -55,9 +55,10 @@ val pp_ie : ie -> string
 val pp_dir : dir -> string
 val pp_extr : extr -> string
 val pp_sd : sd -> string
-val seq_sd : sd -> sd -> sd
+val seq_sd : sd -> sd -> sd option
 val is_same_loc : sd -> bool
-val is_both_loc : sd -> bool
+val is_diff_loc : sd -> bool
+val is_unspec_loc : sd -> bool
 (* The first boolean indicates whether wildcard syntax is included in the fold *)
 val fold_ie : bool -> (ie -> 'a -> 'a) -> 'a -> 'a
 val fold_extr : bool -> (extr -> 'a -> 'a) -> 'a -> 'a

gen/common/edge.ml

@@ -388,7 +388,7 @@ let pp_dp_default tag sd e = sprintf "%s%s%s" tag (pp_sd sd) (pp_extr e)
   | Po (sd,_,_) | Fenced (_,sd,_,_) | Dp (_,sd,_) -> sd
   | Insert _|Store|Node _|Fr _|Ws _|Rf _|Hat|Rmw _|Id|Leave _|Back _ -> Same
 
-  let do_is_diff e = not @@ Code.is_same_loc @@ do_loc_sd e
+  let do_is_diff e = Code.is_diff_loc @@ do_loc_sd e
 
 let fold_tedges_compat f r =
   let r = fold_ie wildcard (fun ie -> f (Ws ie)) r in
@@ -445,7 +445,7 @@ let fold_tedges f r =
   let ok_non_rmw e a1 a2 =
     (* `do_is_diff` is safe to call when `e` is not
        wildcard `*`/UnspecLoc location. *)
-    Code.is_both_loc @@ do_loc_sd e ||
+    Code.is_unspec_loc @@ do_loc_sd e ||
     do_is_diff e || do_disjoint ||
     (overlap_atoms a1 a2 &&
      not (do_strict_overlap && same_access_atoms a1 a2))
@@ -1039,7 +1039,11 @@ let fold_tedges f r =
 
 (* compact *)
 
-  let seq_sd e1 e2 = Code.seq_sd (loc_sd e1) (loc_sd e2)
+  let seq_sd e1 e2 =
+    match Code.seq_sd (loc_sd e1) (loc_sd e2) with
+    | None -> Warn.user_error "Unexpected UnspecLoc"
+    | Some b -> b
+
 
   let fst_dp e1 e2 k = match e1.edge with
   | Dp (d,_,_) ->

gen/cycle.ml

@@ -470,7 +470,7 @@ let next_loc e ((loc0,lab0),vs) = match E.is_fetch e with
 
 let same_loc e = Code.is_same_loc @@ E.loc_sd e
 
-let diff_loc e = not (same_loc e)
+let diff_loc e = Code.is_diff_loc @@ E.loc_sd e
 
 let same_proc e = E.get_ie e = Int
 let diff_proc e = E.get_ie e = Ext