current

Author: naim-mr

OAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOAOA

@@ -682,7 +682,15 @@ module Affine (B : PARTITION) : FUNCTION = struct
     | T_var x -> (
         match f with
         | Fun f ->
-            let env = Linexpr1.get_env f in
+            let env0 = Linexpr1.get_env f in
+            let env =
+              if Environment.mem_var env0 v then env0
+              else Environment.add env0 [| v |] [||]
+            in
+            let f =
+              if Environment.mem_var env0 v then f
+              else Linexpr1.extend_environment f env
+            in
             let e = Texpr1.of_expr env (exp_to_apron e) in
             let f = Linexpr1.copy f in
             let a = Lincons1.array_make env 1 in
@@ -708,6 +716,20 @@ module Affine (B : PARTITION) : FUNCTION = struct
   let bwdAssign f (x, e) =
     { ranking = bwdAssign_ranking f.ranking (x, e); env = f.env; vars = f.vars }
 
+  let of_linexpr env vars linexpr =
+    let le =
+      let le_env = Linexpr1.get_env linexpr in
+      if Environment.mem_var le_env v then linexpr
+      else
+        let ext_env = Environment.add le_env [| v |] [||] in
+        Linexpr1.extend_environment linexpr ext_env
+    in
+    { ranking = Fun le; env; vars }
+
+  let of_ordinal_components env vars = function
+    | [] -> zero env vars
+    | l :: _ -> of_linexpr env vars l
+
   let filter f _ = successor f
 
   (**)

domains/Affines.ml

@@ -23,12 +23,26 @@ module type RANKING_FUNCTION = sig
   val bot : ?domain:B.t -> Environment.t -> var list -> t
   val zero : ?domain:B.t -> Environment.t -> var list -> t
   val top : ?domain:B.t -> Environment.t -> var list -> t
+  val init_with_proton_hint :
+    ?domain:B.t -> source_code:string -> loop_code:string ->
+    Environment.t -> var list -> t
   val domain_zero : t -> t
   val isLeq : kind -> t -> t -> bool
   val join : kind -> t -> t -> t
   val plus : t -> t -> t
   val meet : kind -> t -> t -> t
-  val widen : ?jokers:int -> t -> t -> t
+
+  val widen :
+    ?jokers:int ->
+    ?program_source:string ->
+    ?loop_condition:string ->
+    ?loop_description:string ->
+    ?iteration_number:string ->
+    ?history:t list ->
+    t ->
+    t ->
+    t
+
   val dual_widen : t -> t -> t
   val defined : ?condition:expr typed -> t -> bool
   val partially_defined : ?condition:expr typed -> t -> bool

domains/DecisionTree.ml

@@ -38,6 +38,10 @@ module type FUNCTION = sig
   val reset : f -> f
   val predecessor : f -> f
   val successor : f -> f
+  val of_linexpr : Environment.t -> var list -> Linexpr1.t -> f
+  (** Build from ordinal components: [finite; ω^1 coeff; ω^2 coeff; ...].
+      For non-ordinal domains, only the first element is used. *)
+  val of_ordinal_components : Environment.t -> var list -> Linexpr1.t list -> f
   val bwdAssign : f -> expr typed * expr typed -> f
   val filter : f -> expr typed -> f
   val print : Format.formatter -> f -> unit