Skip to content

Commit

Permalink
Remove warnings
Browse files Browse the repository at this point in the history
  • Loading branch information
@naim-mr
naim-mr committed Feb 27, 2024
1 parent 5c2229f commit 2bc3199
Show file tree
Hide file tree
Showing 6 changed files with 58 additions and 118 deletions.
12 changes: 6 additions & 6 deletions banal/banal_float.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -182,13 +182,13 @@ module Single = struct

include Generic

external round_flt: float -> float = "ml_round_flt" "ml_round_flt_f" "float"
external of_int_flt: int -> float = "ml_of_int_flt" "ml_of_int_flt_f" "float"
external round_flt: float -> float = "ml_round_flt" "ml_round_flt_f" [@@unboxed] [@@noalloc]
external of_int_flt: int -> float = "ml_of_int_flt" "ml_of_int_flt_f" [@@noalloc]

external add_flt: float -> float -> float = "ml_add_flt" "ml_add_flt_f" "float"
external sub_flt: float -> float -> float = "ml_sub_flt" "ml_sub_flt_f" "float"
external mul_flt: float -> float -> float = "ml_mul_flt" "ml_mul_flt_f" "float"
external div_flt: float -> float -> float = "ml_div_flt" "ml_div_flt_f" "float"
external add_flt: float -> float -> float = "ml_add_flt" "ml_add_flt_f" [@@unboxed] [@@noalloc]
external sub_flt: float -> float -> float = "ml_sub_flt" "ml_sub_flt_f" [@@unboxed] [@@noalloc]
external mul_flt: float -> float -> float = "ml_mul_flt" "ml_mul_flt_f" [@@unboxed] [@@noalloc]
external div_flt: float -> float -> float = "ml_div_flt" "ml_div_flt_f" [@@unboxed] [@@noalloc]

let round a = round_flt a

Expand Down
2 changes: 1 addition & 1 deletion banal/banal_linearization.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -196,7 +196,7 @@ module Make(I : INTERVAL) = struct
(* constraint linearization
returns both the true and false conditions
*)
let rec lin_cons (env:env) ((e,t,x):expr typed) : lincons =
let lin_cons (env:env) ((e,t,x):expr typed) : lincons =
match e with
| T_binary (op,e1,e2) ->
let l1, l2 = lin_expr env e1, lin_expr env e2 in
Expand Down
105 changes: 27 additions & 78 deletions domains/DecisionTree.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1356,59 +1356,22 @@ struct
let r = aux (r1,r2) (nc1::cs) in
Node ((c1,nc1),l,r)
| Node ((c1,nc1),l1,r1),Node((c2,_),_,_) when (C.isLeq c1 c2) (* c1 < c2 *) ->
let bcs = B.inner env vars cs in
let bc1 = B.inner env vars [c1] in
if (B.isLeq bcs bc1)
then (* c1 is redundant *) aux (l1,t2) cs
else (* c1 is not redundant *)
let bnc1 = B.inner env vars [nc1] in
if (B.isLeq bcs bnc1)
then (* nc1 is redundant *) aux (r1,t2) cs
else (* nc1 is not redundant *)
let l = aux (l1,t2) (c1::cs) in
let r = aux (r1,t2) (nc1::cs) in
Node ((c1,nc1),l,r)
let l = aux (l1,t2) (c1::cs) in
let r = aux (r1,t2) (nc1::cs) in
Node ((c1,nc1),l,r)
| Node ((c1,_),_,_),Node((c2,nc2),l2,r2) when (C.isLeq c2 c1) (* c1 > c2 *) ->
let bcs = B.inner env vars cs in
let bc2 = B.inner env vars [c2] in
if (B.isLeq bcs bc2)
then (* c2 is redundant *) aux (t1,l2) cs
else (* c2 is not redundant *)
let bnc2 = B.inner env vars [nc2] in
if (B.isLeq bcs bnc2)
then (* nc2 is redundant *) aux (t1,r2) cs
else (* nc2 is not redundant *)
let l = aux (t1,l2) (c2::cs) in
let r = aux (t1,r2) (nc2::cs) in
Node ((c2,nc2),l,r)
let l = aux (t1,l2) (c2::cs) in
let r = aux (t1,r2) (nc2::cs) in
Node ((c2,nc2),l,r)
| Node ((c1,nc1),l1,r1),_ ->
let bcs = B.inner env vars cs in
let bc1 = B.inner env vars [c1] in
if (B.isLeq bcs bc1)
then (* c1 is redundant *) aux (l1,t2) cs
else (* c1 is not redundant *)
let bnc1 = B.inner env vars [nc1] in
if (B.isLeq bcs bnc1)
then (* nc1 is redundant *) aux (r1,t2) cs
else (* nc1 is not redundant *)
let l = aux (l1,t2) (c1::cs) in
let r = aux (r1,t2) (nc1::cs) in
Node ((c1,nc1),l,r)
let l = aux (l1,t2) (c1::cs) in
let r = aux (r1,t2) (nc1::cs) in
Node ((c1,nc1),l,r)
| _,Node((c2,nc2),l2,r2) ->
let bcs = B.inner env vars cs in
let bc2 = B.inner env vars [c2] in
if (B.isLeq bcs bc2)
then (* c2 is redundant *) aux (t1,l2) cs
else (* c2 is not redundant *)
let bnc2 = B.inner env vars [nc2] in
if (B.isLeq bcs bnc2)
then (* nc2 is redundant *) aux (t1,r2) cs
else (* nc2 is not redundant *)
let l = aux (t1,l2) (c2::cs) in
let r = aux (t1,r2) (nc2::cs) in
Node ((c2,nc2),l,r)
let l = aux (t1,l2) (c2::cs) in
let r = aux (t1,r2) (nc2::cs) in
Node ((c2,nc2),l,r)
in
let (t1,t2) = (tree_unification t1.tree t2.tree t1.env t1.vars) |> fun (tree1,tree2) -> {t1 with tree = tree1 } , {t2 with tree = tree2} in
(* handling the case when t2.domain is defined by constraints not present in the tree(s) *)
let ls1 = match domain1 with | None -> LSet.empty | Some domain1 ->
List.fold_left (fun s c ->
Expand Down Expand Up @@ -1453,10 +1416,7 @@ struct
if B.isLeq b bx
then (* x is wanted *)
let bcs = B.inner env vars cs in
if B.isLeq bcs bx
then (* x is redundant *) aux t xs cs
else (* x is not redundant *)
if B.isBot (B.meet bx bcs)
if B.isBot (B.meet bx bcs)
then (* x is conflicting *) Bot
else (* x is neither redundant nor conflicting *)
(match t with
Expand All @@ -1467,10 +1427,7 @@ struct
| _ -> Node((c,nc),l,Bot))
| Node((c,nc),l,r) when (C.isLeq c x) (* c < x *) ->
let bc = B.inner env vars [c] in
if B.isLeq bcs bc
then (* c is redundant *) aux l bs cs
else (* c is not redundant *)
if B.isBot (B.meet bc bcs)
if B.isBot (B.meet bc bcs)
then (* c is conflicting *) aux r bs cs
else (* c is neither redundant nor conflicting *)
let l = aux l bs (c::cs) in
Expand All @@ -1486,10 +1443,7 @@ struct
| _ -> Node((x,nx),l,Bot)))
else (* nx is wanted *)
let bcs = B.inner env vars cs in
if B.isLeq bcs bx
then (* x is redundant *) Bot
else (* x is not redundant *)
if B.isBot (B.meet bx bcs)
if B.isBot (B.meet bx bcs)
then (* x is conflicting *) aux t xs cs
else (* x is neither redundant nor conflicting *)
(match t with
Expand All @@ -1500,10 +1454,7 @@ struct
| _ -> Node((c,nc),Bot,r))
| Node((c,nc),l,r) when (C.isLeq c x) (* c < x *) ->
let bc = B.inner env vars [c] in
if B.isLeq bcs bc
then (* c is redundant *) aux l bs cs
else (* c is not redundant *)
if B.isBot (B.meet bc bcs)
if B.isBot (B.meet bc bcs)
then (* c is conflicting *) aux r bs cs
else (* c is neither redundant nor conflicting *)
let l = aux l bs (c::cs) in
Expand Down Expand Up @@ -1547,15 +1498,15 @@ struct
in
aux t.tree []

let rec print fmt t =
let print fmt t =
let domain = t.domain in
let env = t.env in
let vars = t.vars in
let print_domain fmt domain =
(* let print_domain fmt domain =
match domain with
| None -> ()
| Some domain -> B.print fmt domain
in
in *)
let rec aux t cs =
match t with
| Bot ->
Expand Down Expand Up @@ -1662,9 +1613,8 @@ struct
let manager = Polka.manager_alloc_strict ()
(* Compute the vulnerability analysis, right now the algorithm is naif doesnot implement the dynamic programming *)
let vulnerable t =
(*
print_tree t.vars Format.std_formatter (compress t).tree ;
Format.print_newline () ; *)
Format.print_newline () ;
let forget x = (AbstractSyntax.A_var x, A_RANDOM ) in
let rec unconstraint t cns = match t with
| Bot -> false,[cns]
Expand All @@ -1686,18 +1636,18 @@ struct
[]
| x::[] ->
let t' = (bwdAssign t (forget x)) in
(*

Format.printf "\n Remove last %s \n" x.varName;
print_tree t.vars Format.std_formatter t'.tree ; *)
print_tree t.vars Format.std_formatter t'.tree ;
let b,cons = unconstraint t'.tree [] in
let left_sub = if b then
[(x::acc),cons]
else
[]
in
(*

Format.printf "\n Reste last %s \n" x.varName;
print_tree t.vars Format.std_formatter t.tree ; *)
print_tree t.vars Format.std_formatter t.tree ;
let b,cons = unconstraint t.tree [] in
let right_sub =
if b then
Expand All @@ -1708,13 +1658,12 @@ struct
left_sub@right_sub
| x::q ->
let t' = (bwdAssign t (forget x)) in
(*

Format.printf "\nRemove %s \n" x.varName;
print_tree t.vars Format.std_formatter t'.tree ; *)
print_tree t.vars Format.std_formatter t'.tree ;
let l1 = (aux q (x::acc) t') in
(*
Format.printf "\n Reste %s \n" x.varName;
print_tree t.vars Format.std_formatter t.tree ;*)
print_tree t.vars Format.std_formatter t.tree ;
let l2 = (aux q acc t)
in l1 @ l2
in
Expand Down
4 changes: 2 additions & 2 deletions main/CFGInterpreter.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,13 +104,13 @@ let execute
| FORWARD -> getIncomingStates
| BACKWARD -> getOutgoingStates
in
(**
(*
array that counts the number of times a node as heen processed
NOTE: this assumes that nodes have ids numbered from 1...n and that the
array is accessed through this id e.g. processed.(i) where 'i' is the node id
*)
let processed = Array.make (nodeCount + 1) 0 in
(**
(*
auxiliary function that implements the worklist algorithm expressed in tail-recursive form.
Takes an inital 'nodeMap' as argument that assigns an abstract state to each node and returns a final 'nodeMap'
containing the result of the analysis.
Expand Down
4 changes: 2 additions & 2 deletions main/Cda.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ struct
let i =
List.fold_left
(fun (ai:D.t) (ab:B.t) ->
(**
(*
[ai] is a tree,
[ab] is a contraint toward an undefined leaf the tree
*)
Expand All @@ -147,7 +147,7 @@ struct
Needed to divide the domain if after one iteration we cannot infer the property
*)
then (
(**
(*
[b1] \cup [b2] == ab
*)

Expand Down
49 changes: 20 additions & 29 deletions main/Semantics.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,50 +23,41 @@ let get_bexp prop = match prop with

module type SEMANTIC =
sig
(**
[D]: Underlying instanciantion of the DecisionTree Abstract Domain
*)
(*
[D]: Underlying instanciantion of the DecisionTree Abstract Domain *)
module D : RANKING_FUNCTION

(**
[B]: Underlying instanciantion of the Numerical Abstract Domain used in D
*)
(*
[B]: Underlying instanciantion of the Numerical Abstract Domain used in D *)
module B = D.B
(**
[r]: Ghost type to to handle the different types returned by bwdBlk in different iterators
*)
(*
[r]: Ghost type to to handle the different types returned by bwdBlk in different iterators *)
type r
(**
(*
[p]: Ghost type to to handle the different types for the properties
two case:
(bExp*'a) StringMap.t
or
ctl_property
*)
ctl_property *)

val dummy_prop: 'a p
(**
[fwdInvMap]: a map from the label of the program to an associated the over-approximating numerical abstraction computed in a forward analysis
*)
(*
[fwdInvMap]: a map from the label of the program to an associated the over-approximating numerical abstraction computed in a forward analysis *)
val fwdInvMap: B.t InvMap.t ref
(**
[bwdInvMap]: a map from the label of the program to an associated a decision tree that abstract a ranking function of the program.
*)
(*
[bwdInvMap]: a map from the label of the program to an associated a decision tree that abstract a ranking function of the program. *)
val bwdInvMap: D.t InvMap.t ref
(**
[bwdStm]: abstract backward transfer function of statement for the decision tree abstract domain
*)
(* val bwdStm: ?property:'a p -> ?domain:B.t -> func StringMap.t -> Environment.t -> var list -> r -> stmt -> r
(**
[bwdBlk]: abstract backward transfer function of blocks for the decision tree abstract domain
*)
val bwdBlk: ?property:'a p -> func StringMap.t -> Environment.t -> var list -> r -> block -> r *)
(*
[bwdStm]: abstract backward transfer function of statement for the decision tree abstract domain *)
(* val bwdStm: ?property:'a p -> ?domain:B.t -> func StringMap.t -> Environment.t -> var list -> r -> stmt -> r *)
(*
[bwdBlk]: abstract backward transfer function of blocks for the decision tree abstract domain *)
(* val bwdBlk: ?property:'a p -> func StringMap.t -> Environment.t -> var list -> r -> block -> r *)

val bwdRec: ?property:'a p -> func StringMap.t -> Environment.t -> var list -> D.t -> block -> D.t
val initBlk: Environment.t -> var list -> block -> unit
(**
[analyze]: iterating function that run the analysis for the given semantic
*)
(*
[analyze]: iterating function that run the analysis for the given semantic *)
val analyze: ?precondition:bExp -> ?property:'a p -> AbstractSyntax.prog -> string -> bool

end

0 comments on commit 2bc3199

Please sign in to comment.