package mopsa

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

Source file intervals_rel.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
(****************************************************************************)
(*                                                                          *)
(* 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 operator for computing the most precise interval in a
    post-condition and inform the intervals domain about it.
*)

open Mopsa
open Sig.Reduction.Simplified
open Ast

module Reduction =
struct

  let name = "universal.numeric.reductions.intervals_rel"
  let debug fmt = Debug.debug ~channel:name fmt

  module I = Values.Intervals.Integer.Value
  module R = Relational.Domain

  (** Get a list of variables related numerically to [v] *)
  let get_related_vars v man ctx a = man.ask (R.Q_related_vars v) ctx a

  (** Get the list of modified variables *)
  let get_modified_vars stmt man ctx a =
    match skind stmt with
    | S_assign({ekind = E_var (v, _)}, _) -> [v]

    | S_assume e ->
      (* In case of a filter, we search for the relations of the
         variables present in the expression *)
      let vars = Visitor.expr_vars e in
      List.fold_left (fun acc v -> get_related_vars v man ctx a @ acc) vars vars |>
      List.sort_uniq compare_var

    | _ -> []

  (** Reduction operator *)
  (* TODO: 
     - factor with universal.numeric.packing.intervals_static_scope.ml
     - float reduction
  *)
  let reduce stmt man ctx (pre:'a) (post:'a) : 'a =
    let (module CR : Relational.Instances.RELATIONAL) = !Relational.Instances_choices.numeric_domain in

    (* Get the modified variables *)
    let vars = get_modified_vars stmt man ctx pre |>
               List.filter (fun v -> is_int_type (vtyp v)) in

    (* Refine the interval of each variable *)
    List.fold_left (fun post var ->
        (* Get the interval of var in the box domain *)
        let itv = man.get_value I.id var post in

        (* Get the interval in the relational domain *)
        let itv' = CR.bound_var var (man.get_env CR.id post) in

        (* Combine data *)
        let itv'' = I.meet itv itv' in

        let () = debug "%a %a %a %a %a" pp_var var pp_typ (vtyp var) (format I.print) itv (format I.print) itv' (format I.print) itv'' in

        (* Check if box is less precise *)
        let post = if not (I.subset itv itv')
          then man.set_value I.id var itv'' post
          else
            post
        in

        (* Check if rel is less precise *)
        if not (I.subset itv' itv)
        then
          let range = stmt.srange in
          let ev = mk_var var range in
          match itv'' with
          | Bot.BOT -> man.set_env CR.id CR.bottom post
          | Bot.Nb _ ->
            let ol, oh = I.bounds_opt itv'' in
            let assume s post =
              let oenv = CR.assume s (fun q -> man.ask q ctx post) (man.get_env CR.id post) in
              OptionExt.apply (fun env -> man.set_env CR.id env post) post oenv in
            let post =
              OptionExt.apply (fun l ->
                  assume (mk_assume (mk_binop ~etyp:T_bool (mk_constant ~etyp:T_int (C_int l) range) O_le ev range) range) post) post ol in
            let post =
              OptionExt.apply (fun h -> assume (mk_assume (mk_binop ~etyp:T_bool ev O_le (mk_constant ~etyp:T_int (C_int h) range) range) range) post) post oh in
            post
        else post

      ) post vars

end


let () =
  register_simplified_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