package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file libraryDsl.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
open LibraryDesc
module Access = LibraryDesc.Access (* avoid spurious dependency cycle due to ocamldep overapprox ambiguity between Access and LibraryDesc.Access *)

(** First-class patterns for arguments matching.
    @see <https://github.com/ocaml-ppx/ppxlib/blob/main/src/ast_pattern.ml> for inspiration from ppxlib. *)
module Pattern =
struct
  (** @param a Type of value to match.
      @param k Type of continuation function.
      @param r Return type of match. *)
  type ('a, 'k, 'r) t = 'a -> 'k -> 'r

  exception Expected of string
  let fail s = raise (Expected s)

  let __: _ t = fun x k -> k x
  let drop: _ t = fun _ k -> k

  let nil: _ t = fun x k ->
    match x with
    | [] -> k
    | _ -> fail "Library function is called with more arguments than expected."

  let ( ^:: ) (p1: _ t) (p2: _ t): _ t = fun x k ->
    match x with
    | x1 :: x2 ->
      let k = p1 x1 k in
      let k = p2 x2 k in
      k
    | [] -> 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 list;
  match_arg: (Cil.exp, 'k, 'r) Pattern.t;
  match_var_args: (Cil.exp list, 'l, 'r) Pattern.t;
}

type ('k, 'r) args_desc =
  | []: ('r, 'r) args_desc
  | VarArgs: (_, 'l, 'r) arg_desc -> ('l, 'r) args_desc
  | (::): ('k, _, 'm) arg_desc * ('m, 'r) args_desc -> ('k, 'r) args_desc

let rec match_args: type k r. (k, r) args_desc -> (Cil.exp list, k, r) Pattern.t = function
  | [] -> Pattern.nil
  | VarArgs {match_var_args; _} -> match_var_args
  | {match_arg; _} :: args -> Pattern.(match_arg ^:: match_args args)


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.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) (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"

let special ?(attrs:attr list=[]) args_desc special_cont = {
  special = Fun.flip (match_args args_desc) special_cont;
  accs = accs args_desc;
  attrs;
}

let special' ?(attrs:attr list=[]) args_desc special_cont = {
  special = (fun args -> Fun.flip (match_args args_desc) (special_cont ()) args); (* eta-expanded such that special_cont is re-executed on each call instead of once during LibraryFunctions construction *)
  accs = accs args_desc;
  attrs;
}

let unknown ?attrs args_desc = special ?attrs args_desc Unknown

let empty____desc = {
  match_arg = Pattern.(__);
  match_var_args = Pattern.(__);
  accesses = [];
}
let __ (_name: string) accesses = { empty____desc with accesses; }
let __' accesses = { empty____desc with accesses; }

let empty_drop_desc = {
  match_arg = Pattern.drop;
  match_var_args = Pattern.drop;
  accesses = [];
}
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 c = Access { kind = Spawn; deep = false; } (* TODO: Sound, but very imprecise hack for calls to function pointers given as arguments. *)
let c_deep = Access { kind = Spawn; deep = true; }

let if_ p access = If (p, access)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct