|
@@ -367,9 +367,26 @@ let rec process_condition mode condition (is_nullable_expr:texpr->bool) callback
|
|
if to_nulls then nulls := expr :: !nulls
|
|
if to_nulls then nulls := expr :: !nulls
|
|
else not_nulls := expr :: !not_nulls
|
|
else not_nulls := expr :: !not_nulls
|
|
in
|
|
in
|
|
|
|
+ let remove expr =
|
|
|
|
+ let expr = reveal_expr expr in
|
|
|
|
+ let subj = get_subject mode expr in
|
|
|
|
+ nulls := List.filter (fun e ->
|
|
|
|
+ let e_subj = get_subject mode (reveal_expr e) in
|
|
|
|
+ e_subj <> subj
|
|
|
|
+ ) !nulls;
|
|
|
|
+ not_nulls := List.filter (fun e ->
|
|
|
|
+ let e_subj = get_subject mode (reveal_expr e) in
|
|
|
|
+ e_subj <> subj
|
|
|
|
+ ) !not_nulls;
|
|
|
|
+ in
|
|
let rec traverse positive e =
|
|
let rec traverse positive e =
|
|
match e.eexpr with
|
|
match e.eexpr with
|
|
| TUnop (Not, Prefix, e) -> traverse (not positive) e
|
|
| TUnop (Not, Prefix, e) -> traverse (not positive) e
|
|
|
|
+ | TBinop (OpAssign, checked_expr, e) when is_suitable mode checked_expr && (is_nullable_expr e) ->
|
|
|
|
+ (* remove expr from both list if there is `e = nullable` in condition *)
|
|
|
|
+ remove checked_expr
|
|
|
|
+ | TBlock exprs ->
|
|
|
|
+ List.iter (fun e -> traverse positive e) exprs
|
|
| TBinop (OpEq, { eexpr = TConst TNull }, checked_expr) when is_suitable mode checked_expr ->
|
|
| TBinop (OpEq, { eexpr = TConst TNull }, checked_expr) when is_suitable mode checked_expr ->
|
|
add positive checked_expr
|
|
add positive checked_expr
|
|
| TBinop (OpEq, checked_expr, { eexpr = TConst TNull }) when is_suitable mode checked_expr ->
|
|
| TBinop (OpEq, checked_expr, { eexpr = TConst TNull }) when is_suitable mode checked_expr ->
|
|
@@ -834,12 +851,13 @@ class local_safety (mode:safety_mode) =
|
|
| TWhile (condition, body, NormalWhile) ->
|
|
| TWhile (condition, body, NormalWhile) ->
|
|
condition_callback condition;
|
|
condition_callback condition;
|
|
let (nulls, not_nulls) = process_condition mode condition is_nullable_expr (fun _ -> ()) in
|
|
let (nulls, not_nulls) = process_condition mode condition is_nullable_expr (fun _ -> ()) in
|
|
|
|
+ let original_safe = self#get_safe_locals_copy in
|
|
(** execute `body` with known not-null variables *)
|
|
(** execute `body` with known not-null variables *)
|
|
List.iter self#get_current_scope#add_to_safety not_nulls;
|
|
List.iter self#get_current_scope#add_to_safety not_nulls;
|
|
body_callback
|
|
body_callback
|
|
(fun () -> List.iter self#get_current_scope#add_to_safety not_nulls)
|
|
(fun () -> List.iter self#get_current_scope#add_to_safety not_nulls)
|
|
body;
|
|
body;
|
|
- List.iter self#get_current_scope#remove_from_safety not_nulls;
|
|
|
|
|
|
+ self#get_current_scope#filter_safety original_safe;
|
|
| _ -> fail ~msg:"Expected TWhile" expr.epos __POS__
|
|
| _ -> fail ~msg:"Expected TWhile" expr.epos __POS__
|
|
(**
|
|
(**
|
|
Should be called for bodies of loops (for, while)
|
|
Should be called for bodies of loops (for, while)
|
|
@@ -955,18 +973,46 @@ class local_safety (mode:safety_mode) =
|
|
*)
|
|
*)
|
|
method process_and left_expr right_expr is_nullable_expr (callback:texpr->unit) =
|
|
method process_and left_expr right_expr is_nullable_expr (callback:texpr->unit) =
|
|
callback left_expr;
|
|
callback left_expr;
|
|
- let (_, not_nulls) = process_condition mode left_expr is_nullable_expr (fun e -> ()) in
|
|
|
|
- List.iter self#get_current_scope#add_to_safety not_nulls;
|
|
|
|
|
|
+ let original_safe = self#get_safe_locals_copy in
|
|
|
|
+ (* save not_nulls for `a != null && a > 0` *)
|
|
|
|
+ let (_, not_nulls) = process_condition mode left_expr is_nullable_expr (fun _ -> ()) in
|
|
|
|
+ (* create temp scope for right_expr *)
|
|
|
|
+ let temp_scope = new safety_scope mode STNormal (Hashtbl.copy original_safe) (Hashtbl.create 10) in
|
|
|
|
+ List.iter temp_scope#add_to_safety not_nulls;
|
|
|
|
+ scopes <- temp_scope :: scopes;
|
|
callback right_expr;
|
|
callback right_expr;
|
|
- List.iter self#get_current_scope#remove_from_safety not_nulls
|
|
|
|
|
|
+ self#scope_closed;
|
|
|
|
+
|
|
|
|
+ let safe_after_rhs = temp_scope#get_safe_locals in
|
|
|
|
+ let final_safe = Hashtbl.create (Hashtbl.length original_safe) in
|
|
|
|
+ Hashtbl.iter (fun subj e ->
|
|
|
|
+ if Hashtbl.mem original_safe subj && Hashtbl.mem safe_after_rhs subj then
|
|
|
|
+ Hashtbl.replace final_safe subj e
|
|
|
|
+ ) original_safe;
|
|
|
|
+
|
|
|
|
+ self#get_current_scope#reset_to final_safe;
|
|
(**
|
|
(**
|
|
Handle boolean OR outside of `if` condition.
|
|
Handle boolean OR outside of `if` condition.
|
|
*)
|
|
*)
|
|
method process_or left_expr right_expr is_nullable_expr (callback:texpr->unit) =
|
|
method process_or left_expr right_expr is_nullable_expr (callback:texpr->unit) =
|
|
|
|
+ let original_safe = self#get_safe_locals_copy in
|
|
|
|
+ (* save nulls for `a == null || a > 0` *)
|
|
let (nulls, _) = process_condition mode left_expr is_nullable_expr callback in
|
|
let (nulls, _) = process_condition mode left_expr is_nullable_expr callback in
|
|
- List.iter self#get_current_scope#add_to_safety nulls;
|
|
|
|
|
|
+ (* create temp scope for right_expr *)
|
|
|
|
+ let temp_scope = new safety_scope mode STNormal (Hashtbl.copy original_safe) (Hashtbl.create 10) in
|
|
|
|
+ List.iter temp_scope#add_to_safety nulls;
|
|
|
|
+ scopes <- temp_scope :: scopes;
|
|
callback right_expr;
|
|
callback right_expr;
|
|
- List.iter self#get_current_scope#remove_from_safety nulls
|
|
|
|
|
|
+ self#scope_closed;
|
|
|
|
+
|
|
|
|
+ let safe_after_rhs = temp_scope#get_safe_locals in
|
|
|
|
+ let final_safe = Hashtbl.create (Hashtbl.length original_safe) in
|
|
|
|
+ Hashtbl.iter (fun subj e ->
|
|
|
|
+ if Hashtbl.mem original_safe subj && Hashtbl.mem safe_after_rhs subj then
|
|
|
|
+ Hashtbl.replace final_safe subj e
|
|
|
|
+ ) original_safe;
|
|
|
|
+
|
|
|
|
+ self#get_current_scope#reset_to final_safe;
|
|
(**
|
|
(**
|
|
Remove subject from the safety list if a nullable value is assigned or if an object with safe field is reassigned.
|
|
Remove subject from the safety list if a nullable value is assigned or if an object with safe field is reassigned.
|
|
*)
|
|
*)
|