replace stackop instruction with skip instruction

Reviewed By: cristianoc

Differential Revision: D3828544

fbshipit-source-id: 5a1d05f

infer/src/IR/Cfg.re

@@ -733,8 +733,7 @@ let module Node = {
       | Abstract _
       | Sil.Remove_temps _ =>
         /* these are generated instructions that will be replaced by the preanalysis */
-        instrs
-      | instr => [instr, ...instrs];
+        instrs;
     let convert_node_kind =
       fun
       | Start_node _ => Start_node resolved_proc_desc

infer/src/IR/Sil.re

@@ -32,13 +32,6 @@ type if_kind =
   | Ik_switch;
 
 
-/** Stack operation for symbolic execution on propsets */
-type stackop =
-  | Push /* copy the curreny propset to the stack */
-  | Swap /* swap the current propset and the top of the stack */
-  | Pop /* pop the stack and combine with the current propset */;
-
-
 /** An instruction. */
 type instr =
   /** Load a value from the heap into an identifier.
@@ -65,9 +58,10 @@ type instr =
   | Nullify of Pvar.t Location.t
   | Abstract of Location.t /** apply abstraction */
   | Remove_temps of (list Ident.t) Location.t /** remove temporaries */
-  | Stackop of stackop Location.t /** operation on the stack of propsets */
   | Declare_locals of (list (Pvar.t, Typ.t)) Location.t /** declare local variables */;
 
+let skip_instr = Remove_temps [] Location.dummy;
+
 
 /** Check if an instruction is auxiliary, or if it comes from source instructions. */
 let instr_is_auxiliary =
@@ -79,7 +73,6 @@ let instr_is_auxiliary =
   | Nullify _
   | Abstract _
   | Remove_temps _
-  | Stackop _
   | Declare_locals _ => true;
 
 
@@ -658,7 +651,6 @@ let instr_get_loc =
   | Nullify _ loc
   | Abstract loc
   | Remove_temps _ loc
-  | Stackop _ loc
   | Declare_locals _ loc => loc;
 
 
@@ -672,7 +664,6 @@ let instr_get_exps =
   | Nullify pvar _ => [Exp.Lvar pvar]
   | Abstract _ => []
   | Remove_temps temps _ => IList.map (fun id => Exp.Var id) temps
-  | Stackop _ => []
   | Declare_locals _ => [];
 
 
@@ -706,14 +697,6 @@ let pp_instr pe0 f instr => {
   | Abstract loc => F.fprintf f "APPLY_ABSTRACTION; %a" Location.pp loc
   | Remove_temps temps loc =>
     F.fprintf f "REMOVE_TEMPS(%a); %a" (Ident.pp_list pe) temps Location.pp loc
-  | Stackop stackop loc =>
-    let s =
-      switch stackop {
-      | Push => "Push"
-      | Swap => "Swap"
-      | Pop => "Pop"
-      };
-    F.fprintf f "STACKOP.%s; %a" s Location.pp loc
   | Declare_locals ptl loc =>
     let pp_typ fmt (pvar, _) => F.fprintf fmt "%a" (Pvar.pp pe) pvar;
     F.fprintf f "DECLARE_LOCALS(%a); %a" (pp_comma_seq pp_typ) ptl Location.pp loc
@@ -2191,8 +2174,7 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr =>
     }
   | Nullify _
   | Abstract _
-  | Declare_locals _
-  | Stackop _ => instr
+  | Declare_locals _ => instr
   }
 };
 
@@ -2313,15 +2295,6 @@ let instr_compare instr1 instr2 =>
     }
   | (Remove_temps _, _) => (-1)
   | (_, Remove_temps _) => 1
-  | (Stackop stackop1 loc1, Stackop stackop2 loc2) =>
-    let n = Pervasives.compare stackop1 stackop2;
-    if (n != 0) {
-      n
-    } else {
-      Location.compare loc1 loc2
-    }
-  | (Stackop _, _) => (-1)
-  | (_, Stackop _) => 1
   | (Declare_locals ptl1 loc1, Declare_locals ptl2 loc2) =>
     let pt_compare (pv1, t1) (pv2, t2) => {
       let n = Pvar.compare pv1 pv2;
@@ -2541,7 +2514,6 @@ let instr_compare_structural instr1 instr2 exp_map => {
   | (Abstract _, Abstract _) => (0, exp_map)
   | (Remove_temps temps1 _, Remove_temps temps2 _) =>
     id_list_compare_structural temps1 temps2 exp_map
-  | (Stackop stackop1 _, Stackop stackop2 _) => (Pervasives.compare stackop1 stackop2, exp_map)
   | (Declare_locals ptl1 _, Declare_locals ptl2 _) =>
     let n = Pervasives.compare (IList.length ptl1) (IList.length ptl2);
     if (n != 0) {

infer/src/IR/Sil.rei

@@ -34,13 +34,6 @@ type if_kind =
   | Ik_switch;
 
 
-/** Stack operation for symbolic execution on propsets */
-type stackop =
-  | Push /* copy the curreny propset to the stack */
-  | Swap /* swap the current propset and the top of the stack */
-  | Pop /* pop the stack and combine with the current propset */;
-
-
 /** An instruction. */
 type instr =
   /** Load a value from the heap into an identifier.
@@ -67,9 +60,10 @@ type instr =
   | Nullify of Pvar.t Location.t
   | Abstract of Location.t /** apply abstraction */
   | Remove_temps of (list Ident.t) Location.t /** remove temporaries */
-  | Stackop of stackop Location.t /** operation on the stack of propsets */
   | Declare_locals of (list (Pvar.t, Typ.t)) Location.t /** declare local variables */;
 
+let skip_instr: instr;
+
 
 /** Check if an instruction is auxiliary, or if it comes from source instructions. */
 let instr_is_auxiliary: instr => bool;

infer/src/backend/preanal.ml

@@ -145,8 +145,7 @@ module NullifyTransferFunctions = struct
           active_defs', to_nullify
       | Sil.Store (Exp.Lvar lhs_pvar, _, _, _) ->
           VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify
-      | Sil.Store _ | Prune _ | Declare_locals _ | Stackop _ | Remove_temps _
-      | Abstract _ ->
+      | Sil.Store _ | Prune _ | Declare_locals _ | Remove_temps _ | Abstract _ ->
           astate
       | Sil.Nullify _ ->
           failwith "Should not add nullify instructions before running nullify analysis!" in

infer/src/backend/state.ml

@@ -132,8 +132,7 @@ let node_simple_key node =
       | Sil.Nullify _ -> add_key 5
       | Sil.Abstract _ -> add_key 6
       | Sil.Remove_temps _ -> add_key 7
-      | Sil.Stackop _ -> add_key 8
-      | Sil.Declare_locals _ -> add_key 9 in
+      | Sil.Declare_locals _ -> add_key 8 in
   IList.iter do_instr (Cfg.Node.get_instrs node);
   Hashtbl.hash !key
 

infer/src/backend/symExec.ml

@@ -1254,8 +1254,6 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       let sigma' = prop_.Prop.sigma @ sigma_locals in
       let prop' = Prop.normalize tenv (Prop.set prop_ ~sigma:sigma') in
       ret_old_path [prop']
-  | Sil.Stackop _ -> (* this should be handled at the propset level *)
-      assert false
 and diverge prop path =
   State.add_diverging_states (Paths.PathSet.from_renamed_list [(prop, path)]); (* diverge *)
   []
@@ -1717,29 +1715,6 @@ let node handle_exn tenv node (pset : Paths.PathSet.t) : Paths.PathSet.t =
         end
       else sym_exec_wrapper handle_exn tenv pdesc instr (p, tr) in
     Paths.PathSet.union pset2 pset1 in
-  let exe_instr_pset (pset, stack) instr = (* handle a single instruction at the set level *)
-    let pp_stack_instr pset' =
-      L.d_str "Stack Instruction "; Sil.d_instr instr; L.d_ln ();
-      L.d_strln "Stack Instruction Returns";
-      Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv pset'); L.d_ln () in
-    match instr, stack with
-    | Sil.Stackop (Sil.Push, _), _ ->
-        pp_stack_instr pset;
-        (pset, pset :: stack)
-    | Sil.Stackop (Sil.Swap, _), (pset':: stack') ->
-        pp_stack_instr pset';
-        (pset', pset:: stack')
-    | Sil.Stackop (Sil.Pop, _), (pset':: stack') ->
-        let pset'' = Paths.PathSet.union pset pset' in
-        pp_stack_instr pset'';
-        (pset'', stack')
-    | Sil.Stackop _, _ -> (* should not happen *)
-        assert false
-    | _ ->
-        let pset' = Paths.PathSet.fold (exe_instr_prop instr) pset Paths.PathSet.empty in
-        (pset', stack) in
-  let stack = [] in
-  let instrs = Cfg.Node.get_instrs node in
-  let pset', stack' = IList.fold_left exe_instr_pset (pset, stack) instrs in
-  if stack' != [] then assert false; (* final stack must be empty *)
-  pset'
+  let exe_instr_pset pset instr =
+    Paths.PathSet.fold (exe_instr_prop instr) pset Paths.PathSet.empty in
+  IList.fold_left exe_instr_pset pset (Cfg.Node.get_instrs node)

infer/src/checkers/BoundedCallTree.ml

@@ -147,8 +147,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
            other potential special kinds of procedure calls to be added later,
            e.g. Java reflection. *)
         astate
-    | Sil.Load _ | Store _ | Prune _ | Declare_locals _
-    | Stackop _ | Remove_temps _ | Abstract _ | Nullify _ ->
+    | Sil.Load _ | Store _ | Prune _ | Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ ->
         astate
 end
 

infer/src/checkers/abstractInterpreter.ml

@@ -63,11 +63,8 @@ module MakeNoCFG
         | None -> post, inv_map in
       (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
       let instr_ids = match CFG.instr_ids node with
-        | [] ->
-            (* TODO: get rid of Stackop and replace it with Skip *)
-            [Sil.Stackop (Push, Location.dummy), None]
-        | l ->
-            l in
+        | [] -> [Sil.skip_instr, None]
+        | l -> l in
       let astate_post, inv_map_post = IList.fold_left compute_post (pre, inv_map) instr_ids in
       L.out "Post for node %a is %a@." CFG.pp_id node_id A.pp astate_post;
       let inv_map'' = M.add node_id { pre; post=astate_post; visit_count; } inv_map_post in

infer/src/checkers/addressTaken.ml

@@ -44,7 +44,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           | actual_exp, Typ.Tptr _ -> add_address_taken_pvars actual_exp astate_acc
           | _ -> astate_acc in
         IList.fold_left add_actual_by_ref astate actuals
-    | Sil.Store _ | Load _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Stackop _
+    | Sil.Store _ | Load _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _
     | Declare_locals _ ->
         astate
 end

infer/src/checkers/checkers.ml

@@ -541,7 +541,6 @@ let callback_check_field_access { Callbacks.proc_desc } =
     | Sil.Nullify _
     | Sil.Abstract _
     | Sil.Remove_temps _
-    | Sil.Stackop _
     | Sil.Declare_locals _ ->
         () in
   Cfg.Procdesc.iter_instrs do_instr proc_desc

infer/src/checkers/copyPropagation.ml

@@ -107,8 +107,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         if !Config.curr_language = Config.Java
         then astate' (* Java doesn't have pass-by-reference *)
         else IList.fold_left kill_actuals_by_ref astate' actuals
-    | Sil.Store _ | Sil.Prune _ | Sil.Nullify _ | Sil.Abstract _ | Sil.Remove_temps _
-    | Sil.Declare_locals _ | Sil.Stackop _ ->
+    | Sil.Store _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Declare_locals _ ->
         (* none of these can assign to program vars or logical vars *)
         astate
 end

infer/src/checkers/liveness.ml

@@ -52,7 +52,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           astate
         |> exp_add_live call_exp
         |> IList.fold_right exp_add_live (IList.map fst params)
-    | Sil.Declare_locals _ | Stackop _ | Remove_temps _ | Abstract _ | Nullify _ ->
+    | Sil.Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ ->
         astate
 end
 

infer/src/eradicate/typeCheck.ml

@@ -1068,8 +1068,6 @@ let typecheck_instr
 
       let node', ncond = normalize_cond node cond in
       check_condition node' ncond
-  | Sil.Stackop _ ->
-      typestate
 
 (** Typecheck the instructions in a cfg node. *)
 let typecheck_node

infer/src/quandary/TaintAnalysis.ml

@@ -234,7 +234,7 @@ module Make (TraceDomain : Trace.S) = struct
           astate_with_source
       | Sil.Call _ ->
           failwith "Unimp: non-pname call expressions"
-      | Sil.Prune _ | Remove_temps _ | Nullify _ | Abstract _ | Stackop _ | Declare_locals _ ->
+      | Sil.Prune _ | Remove_temps _ | Nullify _ | Abstract _ | Declare_locals _ ->
           astate
   end
 

infer/src/unit/procCfgTests.ml

@@ -21,7 +21,7 @@ let tests =
     Cfg.Procdesc.create cfg (ProcAttributes.default Procname.empty_block !Config.curr_language) in
   let dummy_instr1 = Sil.Remove_temps ([], Location.dummy) in
   let dummy_instr2 = Sil.Abstract Location.dummy in
-  let dummy_instr3 = Sil.Stackop (Pop, Location.dummy) in
+  let dummy_instr3 = Sil.Remove_temps ([Ident.create_fresh Ident.knormal], Location.dummy) in
   let dummy_instr4 = Sil.Remove_temps ([], Location.dummy) in
   let instrs1 = [dummy_instr1; dummy_instr2;] in
   let instrs2 = [dummy_instr3] in