package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file logic_simplification.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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Aorai plug-in of Frama-C.                        *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*    INRIA (Institut National de Recherche en Informatique et en         *)
(*           Automatique)                                                 *)
(*    INSA  (Institut National des Sciences Appliquees)                   *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Automaton_ast

let pretty_clause fmt l =
  Format.fprintf fmt "@[<2>[%a@]]@\n"
    (Pretty_utils.pp_list ~sep:",@ " Pretty_automaton.Typed.print_condition) l

let pretty_dnf fmt l =
  Format.fprintf fmt "@[<2>[%a@]]@\n"
    (Pretty_utils.pp_list pretty_clause) l

let opposite_rel =
  function
  | Rlt -> Rge
  | Rgt -> Rle
  | Rge -> Rlt
  | Rle -> Rgt
  | Req -> Rneq
  | Rneq -> Req

let rec condToDNF cond =
  (*Typing : condition --> list of list of terms (disjunction of conjunction of terms)
    DNF(term)   = {{term}}
    DNF(a or b)  = DNF(a) \/ DNF(b)
    DNF(a and b) = Composition (DNF(a),DNF(b))
    DNF(not a)   = tmp = DNF(a)
                   composition (tmp)
                   negation of each term
  *)
  match cond with
  | TOr  (c1, c2) -> (condToDNF c1)@(condToDNF c2)
  | TAnd (c1, c2) ->
    let d1,d2=(condToDNF c1), (condToDNF c2) in
    List.rev
      (List.fold_left
         (fun lclause clauses1 ->
            (List.map (fun clauses2 -> clauses1@clauses2) d2) @ lclause
         )
         [] d1)
  | TNot (c) ->
    begin
      match c with
      | TOr  (c1, c2) -> condToDNF (TAnd(TNot(c1),TNot(c2)))
      | TAnd (c1, c2) -> condToDNF (TOr (TNot(c1),TNot(c2)))
      | TNot (c1) -> condToDNF c1
      | TTrue -> condToDNF TFalse
      | TFalse -> condToDNF TTrue
      | TRel(rel,t1,t2) -> [[TRel(opposite_rel rel,t1,t2)]]
      | _ as t -> [[TNot(t)]]
    end
  | TTrue -> [[TTrue]]
  | TFalse -> []
  | _ as t -> [[t]]

let removeTerm term lterm =
  List.fold_left
    (fun treated t ->
       match term,t with
       | TCall (kf1,None), TCall (kf2,_)
       | TReturn kf1, TReturn kf2
         when Kernel_function.equal kf1 kf2 -> treated
       | TCall(kf1,Some b1), TCall(kf2, Some b2)
         when Kernel_function.equal kf1 kf2 &&
              Datatype.String.equal b1.b_name b2.b_name -> treated
       | _  -> t::treated)
    []
    lterm

(** Given a list of terms (representing a conjunction),
    if a positive call or return is present,
    then all negative ones are obvious and removed *)
let positiveCallOrRet clause =
  try
    (* Step 1: find a positive information TCall or TReturn. *)
    let positive, computePositive=
      List.fold_left
        (fun (positive,treated as res) term ->
           match term with
           | TCall (kf1,None) ->
             begin match positive with
               | None -> (Some term, term::treated)
               | Some (TCall (kf2,None)) ->
                 if Kernel_function.equal kf1 kf2 then res else raise Exit
               | Some (TReturn _) -> raise Exit
               | Some(TCall (kf2,Some _) as term2) ->
                 if Kernel_function.equal kf1 kf2 then
                   Some term, term :: removeTerm term2 treated
                 else raise Exit
               | _ ->
                 Aorai_option.fatal
                   "inconsistent environment in positiveCallOrRet"
             end
           | TCall (kf1, Some b1) ->
             begin match positive with
               | None -> (Some term, term::treated)
               | Some (TCall (kf2,None)) ->
                 if Kernel_function.equal kf1 kf2 then res else raise Exit
               | Some (TReturn _) -> raise Exit
               | Some(TCall (kf2,Some b2)) ->
                 if Kernel_function.equal kf1 kf2 then
                   if Datatype.String.equal b1.b_name b2.b_name then
                     res
                   else
                     positive, term :: treated
                 else raise Exit
               | _ ->
                 Aorai_option.fatal
                   "inconsistent environment in positiveCallOrRet"
             end
           | TReturn kf1 ->
             begin match positive with
               | None -> (Some term, term::treated)
               | Some (TReturn kf2) ->
                 if Kernel_function.equal kf1 kf2 then res else raise Exit
               | Some (TCall _) -> raise Exit
               | _ ->
                 Aorai_option.fatal
                   "inconsistent environment in positiveCallOrRet"
             end
           | _  -> positive, term::treated
        )
        (None, [])
        clause
    in
    let computePositive = List.rev computePositive in
    (* Step 2 : Remove negatives not enough expressive *)
    match positive with
    | None -> computePositive
    | Some (TCall (kf1,None)) ->
      List.rev
        (List.fold_left
           (fun treated term ->
              match term with
              | TNot(TCall (kf2,_)) ->
                if Kernel_function.equal kf1 kf2 then raise Exit
                (* Positive information more specific than negative *)
                else treated
              | TNot(TReturn _) -> treated
              | _  -> term::treated
           )
           [] computePositive)
    | Some (TCall (kf1, Some b1)) ->
      List.rev
        (List.fold_left
           (fun treated term ->
              match term with
              | TNot(TCall (kf2,None)) ->
                if Kernel_function.equal kf1 kf2 then raise Exit
                (* Positive information more specific than negative *)
                else treated
              | TNot(TCall(kf2, Some b2)) ->
                if Kernel_function.equal kf1 kf2 then
                  if Datatype.String.equal b1.b_name b2.b_name then
                    raise Exit
                  else term :: treated
                else treated
              | TNot(TReturn _) -> treated
              | _  -> term::treated
           )
           [] computePositive)
    | Some (TReturn kf1) ->
      List.rev
        (List.fold_left
           (fun treated term ->
              match term with
              | TNot(TCall _) -> treated
              | TNot(TReturn kf2) ->
                (* Two opposite information *)
                if Kernel_function.equal kf1 kf2 then raise Exit
                else treated
              | _ -> term::treated
           )
           [] computePositive)
    | _ ->
      Aorai_option.fatal "inconsistent environment in positiveCallOrRet"
  with Exit -> [TFalse] (* contradictory requirements for current event. *)

let rel_are_equals (rel1,t11,t12) (rel2,t21,t22) =
  rel1 = rel2
  && Logic_utils.is_same_term t11 t21
  && Logic_utils.is_same_term t12 t22

let swap_rel (rel,t1,t2) =
  let rel = match rel with
    | Rlt -> Rgt
    | Rle -> Rge
    | Rge -> Rle
    | Rgt -> Rlt
    | Req -> Req
    | Rneq -> Rneq
  in (rel,t2,t1)

let contradict_rel r1 (rel2,t21,t22) =
  rel_are_equals r1 (opposite_rel rel2, t21,t22)
  || rel_are_equals (swap_rel r1) (opposite_rel rel2, t21, t22)

let rec termsAreEqual term1 term2 =
  match term1,term2 with
  | TTrue,TTrue
  | TFalse,TFalse -> true
  | TCall (a,None), TCall (b,None)
  | TReturn a, TReturn b -> Kernel_function.equal a b
  | TCall (f1,Some b1), TCall(f2, Some b2) ->
    Kernel_function.equal f1 f2 && Datatype.String.equal b1.b_name b2.b_name
  | TNot(TRel(rel1,t11,t12)), TRel(rel2,t21,t22)
  | TRel(rel1,t11,t12), TNot(TRel(rel2,t21,t22)) ->
    contradict_rel (rel1,t11,t12) (rel2,t21,t22)
  | TNot(a),TNot(b) -> termsAreEqual a b
  | TRel(rel1,t11,t12), TRel(rel2,t21,t22) ->
    rel_are_equals (rel1,t11,t12) (rel2,t21,t22)
  | _  -> false

let negative_term term =
  match term with
  | TNot(c) -> c
  | TCall _ | TReturn _ | TRel _ -> TNot term
  | TTrue -> TFalse
  | TFalse -> TTrue
  | TAnd (_,_) | TOr (_,_) -> Aorai_option.fatal "not a term of DNF clause"

(** Simplify redundant relations. *)
let simplify clause =
  try
    List.rev
      (List.fold_left
         (fun clause term ->
            match term with
            | TTrue | TNot(TFalse) -> clause
            | TFalse | TNot(TTrue) -> raise Exit
            | _ ->
              if List.exists (termsAreEqual (negative_term term)) clause
              then raise Exit;
              if List.exists (termsAreEqual term) clause then clause
              else term :: clause)
         [] clause)
  with Exit -> [TFalse]

(** true iff clause1  <: clause2*)
let clausesAreSubSetEq clause1 clause2 =
  (List.for_all
     (fun t1 ->List.exists ( fun t2 -> termsAreEqual t1 t2) clause2)
     clause1)


(** true iff clause1  <: clause2 and clause2  <: clause1 *)
let clausesAreEqual clause1 clause2 =
  clausesAreSubSetEq clause1 clause2 && clausesAreSubSetEq clause2 clause1

(** return the clauses list named lclauses without any clause c such as  cl <: c *)
let removeClause lclauses cl =
  List.filter (fun c -> not (clausesAreSubSetEq cl c)) lclauses

(* Obvious version. *)
let negativeClause clause = List.map negative_term clause

let simplifyClauses clauses =
  try
    List.rev
      (List.fold_left
         (fun acc c ->
            (* If 2 clauses are C and not C then their disjunction implies true *)
            if List.exists (clausesAreEqual (negativeClause c)) acc then
              raise Exit
              (* If an observed clause c2 is included inside the current clause
                 then the current is not added *)
            else if (List.exists (fun c2 -> clausesAreSubSetEq c2 c) acc) then
              acc
              (* If the current clause is included inside an observed clause
                 c2 then the current is added and c2 is removed *)
            else if (List.exists (fun c2 -> clausesAreSubSetEq c c2) acc) then
              c::(removeClause acc c)
              (* If no simplification then c is add to the list *)
            else c::acc
         )
         [] clauses)
  with Exit -> [[]]

let tor t1 t2 =
  match t1,t2 with
    TTrue,_ | _,TTrue -> TTrue
  | TFalse,t | t,TFalse -> t
  | _,_ -> TOr(t1,t2)

let tand t1 t2 =
  match t1,t2 with
    TTrue,t | t,TTrue -> t
  | TFalse,_ | _,TFalse -> TFalse
  | _,_ -> TAnd(t1,t2)

let rec tnot t =
  match t with
  | TTrue -> TFalse
  | TFalse -> TTrue
  | TNot t -> t
  | TAnd (TCall (c,b), t) ->
    TOr (TNot (TCall (c,b)), TAnd(TCall (c,b), tnot t))
  | TAnd (TReturn c, t) ->
    TOr (TNot (TReturn c), TAnd(TReturn c, tnot t))
  | TAnd (t1,t2) -> TOr(tnot t1, tnot t2)
  | TOr (t1,t2) -> TAnd(tnot t1, tnot t2)
  | TRel(rel,t1,t2) -> TRel(opposite_rel rel, t1, t2)
  | TCall _ | TReturn _ -> TNot t

let tands l = List.fold_right tand l TTrue

let tors l = List.fold_right tor l TFalse

(** Given a DNF condition, it returns a condition in Automaton_ast.condition form.
    WARNING : empty lists not supported
*)
let dnfToCond d = tors (List.map tands d)

let simplClause clause dnf =
  match clause with
  | [] | [TTrue] | [TNot TFalse]-> [[]]
  | [TFalse] | [TNot TTrue] -> dnf
  | _ -> clause :: dnf

(** Given a condition, this function does some logical simplifications.
    It returns both the simplified condition and a disjunction of
    conjunctions of parametrized call or return.
*)
let simplifyCond condition =
  Aorai_option.debug
    "initial condition: %a" Pretty_automaton.Typed.print_condition condition;
  (* Step 1 : Condition is translate into Disjunctive Normal Form *)
  let res1 = condToDNF condition in
  Aorai_option.debug "initial dnf: %a" pretty_dnf res1;
  (* Step 2 : Positive Call/Ret are used to simplify negative ones *)
  let res =
    List.rev
      (List.fold_left
         (fun lclauses clause ->
            simplClause (positiveCallOrRet clause) lclauses)
         [] res1)
  in
  Aorai_option.debug "after step 2: %a" pretty_dnf res;
  (* Step 3 : simplification between exprs inside a clause *)
  let res =
    List.rev
      (List.fold_left
         (fun lclauses clause -> simplClause (simplify clause) lclauses) [] res)
  in
  Aorai_option.debug "after step 3: %a" pretty_dnf res;

  (* Step 4 : simplification between clauses *)
  let res = simplifyClauses res in
  Aorai_option.debug "after step 4: %a" pretty_dnf res;
  ((dnfToCond res), res)

(** Given a list of transitions, this function returns the same list of
    transition with simplifyCond done on its cross condition *)
let simplifyTrans transl =
  List.fold_left
    (fun (ltr,lpcond) tr ->
       let (crossCond , pcond ) = simplifyCond (tr.cross) in
       (* pcond stands for parametrized condition :
          disjunction of conjunctions of parametrized call/return *)
       let tr'= { tr with cross = crossCond } in
       Aorai_option.debug "condition is %a, dnf is %a"
         Pretty_automaton.Typed.print_condition crossCond pretty_dnf pcond;
       if tr'.cross <> TFalse then (tr'::ltr,pcond::lpcond) else (ltr,lpcond)
    )
    ([],[])
    (List.rev transl)

(** Given a DNF condition, it returns the same condition simplified according
    to the context (function name and status). Hence, the returned condition
    is without any Call/Return stmts.
*)
let simplifyDNFwrtCtx dnf kf1 status =
  Aorai_option.debug "Before simplification: %a" pretty_dnf dnf;
  let rec simplCondition c =
    match c with
    | TCall (kf2, None) ->
      if  Kernel_function.equal kf1 kf2 && status = Automaton_ast.Call then
        TTrue
      else TFalse
    | TCall (kf2, Some _) ->
      if Kernel_function.equal kf1 kf2 && status = Automaton_ast.Call then
        c
      else TFalse
    | TReturn kf2 ->
      if Kernel_function.equal kf1 kf2 && status = Automaton_ast.Return then
        TTrue
      else TFalse
    | TNot c -> tnot (simplCondition c)
    | TAnd(c1,c2) -> tand (simplCondition c1) (simplCondition c2)
    | TOr (c1,c2) -> tor (simplCondition c1) (simplCondition c2)
    | TTrue | TFalse | TRel _ -> c
  in
  let simplCNFwrtCtx cnf =
    tands (List.map simplCondition cnf)
  in
  let res = tors (List.map simplCNFwrtCtx dnf) in
  Aorai_option.debug
    "After simplification: %a" Pretty_automaton.Typed.print_condition res; res

(*
Tests :

Working :
==========
simplifyCond(PAnd(POr(PTrue,PIndexedExp("a")),PNot(PAnd(PFalse,PIndexedExp("b")))));;
- : condition = PTrue

simplifyCond(POr(PAnd(PNot(PIndexedExp("b")),POr(PTrue,PIndexedExp("a"))),PAnd(PIndexedExp("a"),PNot(PFalse))));;
- : condition = POr (PIndexedExp "a", PNot (PIndexedExp "b"))


simplifyCond(PAnd(PAnd(PCall("a"),PIndexedExp "a"),PAnd(PNot(PCall("a")),PNot(PIndexedExp "a"))));;
- : condition = PFalse


simplifyCond(PAnd(PIndexedExp "a",PNot(PIndexedExp "a")));;
- : condition = PFalse


simplifyCond(PAnd(PCall("a"),PCall("a")));;
- : condition = PCall "a"

simplifyCond(PAnd(PIndexedExp("a"),PNot(PIndexedExp("a"))));;
- : condition = PFalse


simplifyCond(POr(PCall("a"),PNot(PCall("a"))));;
- : condition = PTrue

simplifyCond(PAnd(POr(PCall("a"),PCall("b")),POr(PNot(PCall("a")),PCall("b")))) ;;
- : condition = PCall "b"

simplifyCond(POr (PCall "b", PCall "b"));;
- : condition = PCall "b"




Simplifications to be done :
=========================



*)

(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
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