package mopsa

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

Source file numeric_eval.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
(****************************************************************************)
(*                                                                          *)
(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)
(*                                                                          *)
(* Copyright (C) 2017-2019 The MOPSA Project.                               *)
(*                                                                          *)
(* This program is free software: 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, either version 3 of the License, or     *)
(* (at your option) any later version.                                      *)
(*                                                                          *)
(* This program 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.                      *)
(*                                                                          *)
(* You should have received a copy of the GNU Lesser General Public License *)
(* along with this program.  If not, see <http://www.gnu.org/licenses/>.    *)
(*                                                                          *)
(****************************************************************************)

(** Reduction rule for numeric evaluations *)

open Mopsa
open Ast
open Sig.Reduction.Eval



module Reduction =
struct
  let name = "universal.numeric.reductions.numeric_eval"

  let reduce exp man rman pre results flow =
    (* No reduction if no numeric expression found *)
    if not @@ List.exists
        (fun e ->
           let n = get_expr_translation "Universal" e in
           is_numeric_type n.etyp
        ) results
    then None
    else
    (* Simplify constant expressions *)
    let results' =
      results
      |> List.map (fun e ->
          let n = get_expr_translation "Universal" e in
          match expr_to_const n with
          | Some c -> add_expr_translation "Universal" { n with ekind = E_constant c } e
          | None -> e
        )
      (* Convert boolean values to numeric values to simplify reduction *)
      |> List.map (fun e ->
          let n = get_expr_translation "Universal" e in
          match ekind n with
          | E_constant (C_bool true) -> add_expr_translation "Universal" { n with ekind = E_constant (C_int Z.one); etyp = T_int } e
          | E_constant (C_bool false) -> add_expr_translation "Universal" { n with ekind = E_constant (C_int Z.zero); etyp = T_int } e
          | _ -> e
        )
    in
    match results' with
      | [] -> Some (Eval.empty flow)
      | [e] -> Some (Eval.singleton e flow)
      | hd::tl ->
        (* Iterate over the list of result expressions and accumulate the most precise one *)
        let rec iter acc flow = function
          | [] -> Eval.singleton acc flow
          | hd::tl ->
            let nacc = get_expr_translation "Universal" acc in
            let nhd = get_expr_translation "Universal" hd in
            match ekind nacc, ekind nhd with
            (* Top rules *)
            | _, E_constant (C_top _) ->
              iter acc flow tl

            | E_constant (C_top _), _ ->
              iter hd flow tl

            (* Integer expressions *)
            | E_constant (C_int a), E_constant (C_int b) ->
              if Z.(a = b) then iter acc flow tl else Eval.empty flow

            | E_constant (C_int_interval(a,b)), E_constant(C_int c) ->
              let c = ItvUtils.IntBound.Finite c in
              if ItvUtils.IntBound.leq a c && ItvUtils.IntBound.leq c b then iter hd flow tl else Eval.empty flow

            | E_constant(C_int c), E_constant (C_int_interval(a,b)) ->
              let c = ItvUtils.IntBound.Finite c in
              if ItvUtils.IntBound.leq a c && ItvUtils.IntBound.leq c b then iter acc flow tl else Eval.empty flow

            | E_constant(C_int_interval (a,b)), E_constant (C_int_interval(c,d)) ->
              let lo = ItvUtils.IntBound.max a c and hi = ItvUtils.IntBound.min b d in
              if ItvUtils.IntBound.leq lo hi then
                let acc = add_expr_translation "Universal" (mk_int_general_interval lo hi exp.erange) acc in
                iter acc flow tl
              else
                Eval.empty flow

            (* Variables *)
            | E_var (v1,mode1), E_var (v2,mode2) ->
              (* Ensure that both variables are equal *)
              man.exec (mk_assume (eq acc hd exp.erange) exp.erange) flow >>% fun flow' ->
              (* Keep the strong variable as the most precise expression *)
              let precise = if var_mode v1 mode1 = STRONG then acc else hd in
              iter precise flow' tl

            | E_var _, _
            | _, E_var _ ->
              (* Ensure that variable is equal the other expression *)
              man.exec (mk_assume (eq acc hd exp.erange) exp.erange) flow >>% fun flow' ->
              (* Keep the variable as the most precise expression *)
              let precise =
                match ekind nhd with
                | E_var (v,_) -> hd
                | _ -> acc
              in
              iter precise flow' tl

            (* Logic expressions *)
            | E_binop(op1,_,_), E_binop(op2,_,_) when (is_comparison_op op1 || is_logic_op op1)
                                                   && (is_comparison_op op2 || is_logic_op op2) ->
              (* Transform as a conjunction *)
              let acc' = add_expr_translation "Universal" (mk_log_and acc hd exp.erange) acc in
              iter acc' flow tl

            (* constant AND compare : keep compare *)
            | E_constant (C_int n), E_binop(op,_,_)
            | E_binop(op,_,_), E_constant (C_int n) when (is_comparison_op op || is_logic_op op) ->
              let precise =
                match ekind nhd with E_binop _ -> hd | _ -> acc
              in
              iter precise flow tl

            (* Keep other constants *)
            | E_constant _, _ ->
              iter hd flow tl

            | _, E_constant _ ->
              iter acc flow tl


            | _ -> iter acc flow tl
        in
        Some (iter hd flow tl)

end

let () = register_eval_reduction (module Reduction)
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