Add some symb_locks documentation

Author: sim642

src/analyses/symbLocks.ml

@@ -1,4 +1,6 @@
-(** Symbolic lock-sets for use in per-element patterns. *)
+(** Symbolic lock-sets for use in per-element patterns.
+
+    See Section 5 and 6 in https://dl.acm.org/doi/10.1145/2970276.2970337 for more details. *)
 
 module LF = LibraryFunctions
 module LP = SymbLocksDomain.LockingPattern

src/cdomains/symbLocksDomain.ml

@@ -274,14 +274,17 @@ struct
   let printXml f (x,y,z) = BatPrintf.fprintf f "<value>\n<map>\n<key>1</key>\n%a<key>2</key>\n%a<key>3</key>\n%a</map>\n</value>\n" Exp.printXml x Exp.printXml y Exp.printXml z
 end
 
+(** Index-based symbolic lock *)
 module ILock =
 struct
+
+  (** Index in index-based symbolic lock *)
   module Idx =
   struct
     include Printable.Std
     type t =
-      | Unknown
-      | Star
+      | Unknown (** Unknown index. Mutex index not synchronized with access index. *)
+      | Star (** Star index. Mutex index synchronized with access index. Corresponds to star_0 in ASE16 paper, multiple star indices not supported in this implementation. *)
     [@@deriving eq, ord, hash]
     let name () = "i-lock index"