Add conditional accesses to LibraryDsl

goblint · Sep 25, 2023 · 57c5c3f · 57c5c3f
1 parent 4bc0303
commit 57c5c3f
Show file tree

Hide file tree

Showing 2 changed files with 52 additions and 27 deletions.
diff --git a/src/analyses/libraryDsl.ml b/src/analyses/libraryDsl.ml
@@ -30,8 +30,20 @@ struct
     | [] -> fail "^::"
 end
 
+type access =
+  | Access of LibraryDesc.Access.t
+  | If of (unit -> bool) * access
+
+let rec eval_access = function
+  | Access acc -> Some acc
+  | If (p, access) ->
+    if p () then
+      eval_access access
+    else
+      None
+
 type ('k, 'l, 'r) arg_desc = {
-  accesses: Access.t list;
+  accesses: access list;
   match_arg: (Cil.exp, 'k, 'r) Pattern.t;
   match_var_args: (Cil.exp list, 'l, 'r) Pattern.t;
 }
@@ -51,15 +63,21 @@ let rec accs: type k r. (k, r) args_desc -> Accesses.t = fun args_desc args ->
   match args_desc, args with
   | [], [] -> []
   | VarArgs arg_desc, args ->
-    List.map (fun acc ->
-        (acc, args)
+    List.filter_map (fun access ->
+        match eval_access access with
+        | Some acc -> Some (acc, args)
+        | None -> None
       ) arg_desc.accesses
   | arg_desc :: args_desc, arg :: args ->
     let accs'' = accs args_desc args in
-    List.fold_left (fun (accs'': (Access.t * Cil.exp list) list) (acc: Access.t) ->
-        match List.assoc_opt acc accs'' with
-        | Some args -> (acc, arg :: args) :: List.remove_assoc acc accs''
-        | None -> (acc, [arg]) :: accs''
+    List.fold_left (fun (accs'': (Access.t * Cil.exp list) list) (access: access) ->
+        match eval_access access with
+        | Some acc ->
+          begin match List.assoc_opt acc accs'' with
+            | Some args -> (acc, arg :: args) :: List.remove_assoc acc accs''
+            | None -> (acc, [arg]) :: accs''
+          end
+        | None -> accs''
       ) accs'' arg_desc.accesses
   | _, _ -> invalid_arg "accs"
 
@@ -94,11 +112,13 @@ let drop (_name: string) accesses = { empty_drop_desc with accesses; }
 let drop' accesses = { empty_drop_desc with accesses; }
 
 
-let r = Access.{ kind = Read; deep = false; }
-let r_deep = Access.{ kind = Read; deep = true; }
-let w = Access.{ kind = Write; deep = false; }
-let w_deep = Access.{ kind = Write; deep = true; }
-let f = Access.{ kind = Free; deep = false; }
-let f_deep = Access.{ kind = Free; deep = true; }
-let s = Access.{ kind = Spawn; deep = false; }
-let s_deep = Access.{ kind = Spawn; deep = true; }
+let r = Access { kind = Read; deep = false; }
+let r_deep = Access { kind = Read; deep = true; }
+let w = Access { kind = Write; deep = false; }
+let w_deep = Access { kind = Write; deep = true; }
+let f = Access { kind = Free; deep = false; }
+let f_deep = Access { kind = Free; deep = true; }
+let s = Access { kind = Spawn; deep = false; }
+let s_deep = Access { kind = Spawn; deep = true; }
+
+let if_ p access = If (p, access)
diff --git a/src/analyses/libraryDsl.mli b/src/analyses/libraryDsl.mli
@@ -28,46 +28,51 @@ val special': ?attrs:LibraryDesc.attr list -> (LibraryDesc.special, LibraryDesc.
 (** Create unknown library function descriptor from arguments descriptor, which must {!drop} all arguments. *)
 val unknown: ?attrs:LibraryDesc.attr list -> (LibraryDesc.special, LibraryDesc.special) args_desc -> LibraryDesc.t
 
+(** Argument access descriptor. *)
+type access
 
 (** Argument descriptor, which captures the named argument with accesses for continuation function of {!special}. *)
-val __: string -> LibraryDesc.Access.t list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
+val __: string -> access list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
 
 (** Argument descriptor, which captures an unnamed argument with accesses for continuation function of {!special}. *)
-val __': LibraryDesc.Access.t list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
+val __': access list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
 
 (** Argument descriptor, which drops (does not capture) the named argument with accesses. *)
-val drop: string -> LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_desc
+val drop: string -> access list -> ('r, 'r, 'r) arg_desc
 
 (** Argument descriptor, which drops (does not capture) an unnamed argument with accesses. *)
-val drop': LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_desc
+val drop': access list -> ('r, 'r, 'r) arg_desc
 
 
 (** Shallow {!AccessKind.Read} access.
     All immediate arguments of function calls are always read, this specifies the reading of pointed-to values. *)
-val r: LibraryDesc.Access.t
+val r: access
 
 (** Deep {!AccessKind.Read} access.
     All immediate arguments of function calls are always read, this specifies the reading of pointed-to values.
     Rarely needed. *)
-val r_deep: LibraryDesc.Access.t
+val r_deep: access
 
 (** Shallow {!AccessKind.Write} access. *)
-val w: LibraryDesc.Access.t
+val w: access
 
 (** Deep {!AccessKind.Write} access.
     Rarely needed. *)
-val w_deep: LibraryDesc.Access.t
+val w_deep: access
 
 (** Shallow {!AccessKind.Free} access. *)
-val f: LibraryDesc.Access.t
+val f: access
 
 (** Deep {!AccessKind.Free} access.
     Rarely needed. *)
-val f_deep: LibraryDesc.Access.t
+val f_deep: access
 
 (** Shallow {!AccessKind.Spawn} access. *)
-val s: LibraryDesc.Access.t
+val s: access
 
 (** Deep {!AccessKind.Spawn} access.
     Rarely needed. *)
-val s_deep: LibraryDesc.Access.t
+val s_deep: access
+
+(** Conditional access, e.g. on an option. *)
+val if_: (unit -> bool) -> access -> access