Skip to content

Commit 45a201e

Browse files
emwintemwint
committed
Cleanup
- renamed: `src/analyses/wp_test.ml` -> `src/analyses/wp_analyses/liveness.ml` - modified `src/framework/control.ml` by replacing the standard AnalyzeCFG-module with the one from the upstream repository since I meddled in that one
1 parent 25845da commit 45a201e

File tree

2 files changed

+125
-229
lines changed

2 files changed

+125
-229
lines changed

src/analyses/wp_test.ml renamed to src/analyses/wp_analyses/liveness.ml

Lines changed: 1 addition & 155 deletions
Original file line numberDiff line numberDiff line change
@@ -1,160 +1,6 @@
11
open GoblintCil
22
open Analyses
33

4-
5-
module Spec : Analyses.Spec =
6-
struct
7-
let name () = "wp_test"
8-
9-
(* include Analyses.DefaultBackwSpec *)
10-
11-
include Analyses.IdentitySpec
12-
(*## context ##*)
13-
(*Idea: make context type passsable, so add parameter.*)
14-
module C = Printable.Unit
15-
16-
let context man _ _ = ()
17-
let startcontext () = ()
18-
19-
(*## end of context ##*)
20-
21-
22-
module LiveVariableSet = SetDomain.ToppedSet (Basetype.Variables) (struct let topname = "All variables" end)
23-
module D = LiveVariableSet (*Set of program variables as domain*)
24-
25-
let startstate v = D.empty()
26-
let exitstate v = D.empty()
27-
28-
let vars_from_lval (l: lval) =
29-
match l with
30-
| Var v, NoOffset when isIntegralType v.vtype && not (v.vglob || v.vaddrof) -> Some v (* local integer variable whose address is never taken *)
31-
| _, _ -> None (*do not know what to do here yet*)
32-
33-
let vars_from_expr (e: exp) : D.t=
34-
let rec aux acc e =
35-
match e with
36-
| Lval (Var v, _) -> D.add v acc
37-
| BinOp (_, e1, e2, _) ->
38-
let acc1 = aux acc e1 in
39-
aux acc1 e2
40-
| UnOp (_, e1, _) -> aux acc e1
41-
| SizeOfE e1 -> aux acc e1
42-
| AlignOfE e1 -> aux acc e1
43-
| Question (e1, e2, e3, _) ->
44-
let acc1 = aux acc e1 in
45-
let acc2 = aux acc1 e2 in
46-
aux acc2 e3
47-
| CastE (_, e1) -> aux acc e1
48-
| AddrOf (l1) -> (match vars_from_lval l1 with
49-
| None -> acc
50-
| Some v -> D.add v acc)
51-
| _ -> acc
52-
in
53-
aux (D.empty()) e
54-
55-
56-
let assign man (lval:lval) (rval:exp) =
57-
let v = vars_from_lval lval in
58-
59-
match v with
60-
| None -> D.join man.local (vars_from_expr rval) (*if I do not know what the value is assigned to, then all RHS-Variables might be relevant*)
61-
| Some v ->
62-
let l = (D.diff man.local (D.singleton v)) in
63-
if D.mem v man.local then D.join l (vars_from_expr rval)
64-
else l
65-
66-
let branch man (exp:exp) (tv:bool) =
67-
D.join man.local (vars_from_expr exp)
68-
69-
let body man (f:fundec) =
70-
man.local
71-
72-
let return man (exp:exp option) (f:fundec) =
73-
match exp with
74-
| None -> man.local
75-
| Some e -> D.join man.local (vars_from_expr e)
76-
77-
(* TODO *)
78-
let enter man (lval: lval option) (f:fundec) (args:exp list) =
79-
(* Logs.debug "=== enter function %s with args %s ===" f.svar.vname
80-
(String.concat ", " (List.map (CilType.Exp.show) args)); *)
81-
82-
let vars =
83-
match lval with
84-
| None -> man.local
85-
| Some lv -> man.local (*i have to check for every arg ... no wait... I do not care about the args here, i care about those at the combine!!!!*)
86-
87-
in
88-
89-
[man.local, vars]
90-
91-
(* TODO *)
92-
let combine_env man (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
93-
(* Logs.debug "=== combine_env of function %s ===" f.svar.vname;
94-
let args_pretty = String.concat ", " (List.map CilType.Exp.show args) in
95-
Logs.debug " args: %s" args_pretty;
96-
97-
let sformals_pretty = String.concat ", " (List.map (fun v -> v.vname) f.sformals) in
98-
Logs.debug " sformals: %s" sformals_pretty; *)
99-
100-
(*map relevant sformals in man.local to the corresponding variables contained in the argument*)
101-
let arg_formal_pairs = List.combine args f.sformals in
102-
let relevant_arg_vars =
103-
List.fold_left (fun acc (arg_exp, formal_var) ->
104-
if D.mem formal_var au then
105-
D.join acc (vars_from_expr arg_exp)
106-
else
107-
acc
108-
) (D.empty()) arg_formal_pairs
109-
in
110-
111-
(*join relevant*)
112-
D.join man.local relevant_arg_vars
113-
114-
let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
115-
(* Logs.debug "=== combine_assign of function %s ===" f.svar.vname;
116-
(*how do I know which args are important? i.e. how do I match the local name of the variable in the function with the passed parameters (if there are several)*)
117-
let args_pretty = String.concat ", " (List.map CilType.Exp.show args) in
118-
Logs.debug " args: %s" args_pretty; *)
119-
120-
let simple_assign lval exp acc =
121-
let v = vars_from_lval lval in
122-
123-
match v with
124-
| None -> acc (*D.join acc (vars_from_expr exp) if I do not know what the value is assigned to, then all RHS-Variables might be relevant *)
125-
| Some v ->
126-
let l = (D.diff acc (D.singleton v)) in
127-
(* if D.mem v acc then D.join l (vars_from_expr exp)
128-
else l *)
129-
l
130-
in
131-
132-
match lval with
133-
| Some lval -> List.fold_right (fun exp acc -> simple_assign lval exp acc) args man.local
134-
| _ -> man.local
135-
136-
137-
138-
(** A transfer function which handles the return statement, i.e.,
139-
"return exp" or "return" in the passed function (fundec) *)
140-
let return man (exp: exp option) (f:fundec) : D.t =
141-
let return_val_is_important = (not (D.is_bot man.local)) || (String.equal f.svar.vname "main") in (*this does not take globals int account, only checks for "temp"*)
142-
143-
match exp with
144-
| None -> D.empty()
145-
| Some e -> if return_val_is_important
146-
then D.join (D.empty()) (vars_from_expr e)
147-
else D.empty()
148-
149-
150-
let special man (lval: lval option) (f:varinfo) (arglist:exp list) =
151-
man.local
152-
153-
let threadenter man ~multiple lval f args = [man.local]
154-
let threadspawn man ~multiple lval f args fman = man.local
155-
end
156-
157-
1584
module BackwSpec : BackwAnalyses.BackwSpecSpec = functor (ForwSpec : Analyses.Spec) ->
1595
struct
1606

@@ -166,7 +12,7 @@ struct
16612
module G_forw = ForwSpec.G
16713
module V_forw = ForwSpec.V
16814
module P_forw = ForwSpec.P
169-
let name () = "wp_test"
15+
let name () = "liveness"
17016

17117
module G = Lattice.Unit
17218
module V = EmptyV

0 commit comments

Comments
 (0)