Add Pure instr

src/check.ml

@@ -821,6 +821,11 @@ and checkInstr (i: instr) =
   if !ignoreInstr i then ()
   else
   match i with
+  | Pure (e, l) ->
+      currentLoc := l;
+      currentExpLoc := l;
+      ignore (checkExp false e)
+
   | Set (dest, e, l, el) ->
       currentLoc := l;
       currentExpLoc := el;

src/cil.ml

@@ -827,7 +827,8 @@ and stmtkind =
 (** Instructions. They may cause effects directly but may not have control
     flow.*)
 and instr =
-    Set        of lval * exp * location * location  (** An assignment. A cast is present
+  | Pure of exp * location (** Side-effect-less expression evaluation. *)
+  | Set        of lval * exp * location * location  (** An assignment. A cast is present
                                              if the exp has different type
                                              from lval.
                                              Second location is just for expression when inside condition. *)
@@ -1134,7 +1135,8 @@ let stripUnderscores (s: string) : string =
 
 let get_instrLoc (inst : instr) =
   match inst with
-      Set(_, _, loc, _) -> loc
+    | Pure (_, loc) -> loc
+    | Set(_, _, loc, _) -> loc
     | Call(_, _, _, loc, _) -> loc
     | Asm(_, _, _, _, _, loc) -> loc
     | VarDecl(_,loc) -> loc
@@ -3590,6 +3592,11 @@ class defaultCilPrinterClass : cilPrinter = object (self)
   (*** INSTRUCTIONS ****)
   method pInstr () (i:instr) =       (* imperative instruction *)
     match i with
+    | Pure (e, l) ->
+      self#pLineDirective l
+        ++ self#pExp () e
+        ++ text printInstrTerminator
+
     | Set(lv,e,l,el) -> begin
         (* Be nice to some special cases *)
         match e with
@@ -5363,6 +5370,9 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr =
   let fLval lv = visitCilLval vis lv in
   match i with
   | VarDecl(v,l) -> i
+  | Pure (e, l) ->
+      let e' = fExp e in
+      if e' != e then Pure (e', l) else i
   | Set(lv,e,l,el) ->
       let lv' = fLval lv in let e' = fExp e in
       if lv' != lv || e' != e then Set(lv',e',l,el) else i

src/cil.mli

@@ -1023,12 +1023,13 @@ and stmtkind =
 
 (** {b Instructions}.
  An instruction {!instr} is a statement that has no local
-(intraprocedural) control flow. It can be either an assignment,
+(intraprocedural) control flow. It can be either pure evaluation, an assignment,
 function call, or an inline assembly instruction. *)
 
 (** Instructions. *)
 and instr =
-  Set        of lval * exp * location * location
+  | Pure of exp * location (** Side-effect-less expression evaluation. *)
+  | Set        of lval * exp * location * location
    (** An assignment. The type of the expression is guaranteed to be the same
       with that of the lvalue.
       Second location is just for expression when inside condition. *)

src/ext/pta/ptranal.ml

@@ -269,7 +269,8 @@ let rec analyze_init (i : init ) : A.tau =
 
 let analyze_instr (i : instr ) : unit =
   match i with
-      Set (lval, rhs, l, el) ->
+    | Pure _ -> ()
+    | Set (lval, rhs, l, el) ->
         A.assign (analyze_lval lval) (analyze_expr rhs)
     | Call (res, fexpr, actuals, l, el) ->
         if not (isFunctionType (typeOf fexpr)) then

src/ext/zrapp/availexps.ml

@@ -205,11 +205,16 @@ let eh_kill_addrof_or_global eh =
 let eh_handle_inst i eh =
   if (!ignore_inst) i then eh else
   match i with
+  | Pure _ -> 
+    eh_kill_mem eh;
+    eh_kill_addrof_or_global eh;
+    eh
+
     (* if a pointer write, kill things with read in them.
        also kill mappings from vars that have had their address taken,
        and globals.
        otherwise kill things with lv in them and add e *)
-    Set(lv,e,_,_) -> (match lv with
+  | Set(lv,e,_,_) -> (match lv with
       (Mem _, _) ->
 	(eh_kill_mem eh;
 	 eh_kill_addrof_or_global eh;

src/ext/zrapp/availexpslv.ml

@@ -263,7 +263,12 @@ let lvh_kill_addrof_or_global lvh =
 let lvh_handle_inst i lvh =
   if (!ignore_inst) i then lvh else
   match i with
-    Set(lv,e,_,_) -> begin
+  | Pure _ ->
+    lvh_kill_mem lvh;
+    lvh_kill_addrof_or_global lvh;
+    lvh
+
+  | Set(lv,e,_,_) -> begin
       match lv with
       | (Mem _, _) -> begin
 	  LvExpHash.replace lvh lv e;

src/ext/zrapp/reachingdefs.ml

@@ -275,7 +275,8 @@ let getDefRhs didstmh stmdat defId =
 	      | _ -> false)
 	  | None -> false) iihl in
 	(match i with
-	  Set((lh,_),e,_,_) ->
+  | Pure _ -> assert false (* Pure cannot define *)
+	| Set((lh,_),e,_,_) ->
 	    (match lh with
 	      Var(vi') ->
 		(IH.add rhsHtbl defId (Some(RDExp(e),stm.sid,iosh_in));

src/frontc/cabs2cil.ml

@@ -842,6 +842,7 @@ module BlockChunk =
         {l with synthetic = true}
 
       let doInstr: instr -> instr = function
+        | Pure (e, loc) -> Pure (e, doLoc loc)
         | Set (l, e, loc, eloc) -> Set (l, e, doLoc loc, doLoc eloc)
         | VarDecl (v, loc) -> VarDecl (v, doLoc loc)
         | Call (l, f, a, loc, eloc) -> Call (l, f, a, doLoc loc, doLoc eloc)
@@ -936,6 +937,7 @@ module BlockChunk =
           c
 
       let eDoInstr: instr -> instr = function
+        | Pure (e, loc) -> Pure (e, doLoc loc)
         | Set (l, e, loc, eloc) -> Set (l, e, loc, doLoc eloc)
         | VarDecl (v, loc) -> VarDecl (v, loc)
         | Call (l, f, a, loc, eloc) -> Call (l, f, a, loc, doLoc eloc)
@@ -3504,7 +3506,7 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
   let finishExp ?(newWhat=what)
                 (se: chunk) (e: exp) (t: typ) : chunk * exp * typ =
     match newWhat with
-      ADrop
+    | ADrop -> (SynthetizeLoc.doChunkTail (se +++ (Pure (e, !currentLoc))), e, t) (* TODO: also add eloc if comma expression inside if condition, etc. *)
     | AType -> (SynthetizeLoc.doChunkTail se, e, t)
     | AExpLeaveArrayFun ->
         (SynthetizeLoc.doChunkTail se, e, t) (* It is important that we do not do "processArrayFun" in
@@ -4250,7 +4252,11 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
                  lv, empty
              in
              let (se2, e'', t'') = doExp false e2 (ASet(tmplv, lvt)) in
-             finishExp (se1 @@ se2 @@ se3) (Lval tmplv) lvt
+             let newWhat = match what with
+               | ADrop -> AExpLeaveArrayFun
+               | what -> what
+             in
+             finishExp ~newWhat (se1 @@ se2 @@ se3) (Lval tmplv) lvt
            end
         | _ -> E.s (error "Invalid left operand for ASSIGN")
     end
@@ -4788,6 +4794,7 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
 
 
         (* Now we must finish the call *)
+        let pwhat' = ref what in
         if !piscall then begin
           let addCall (calldest: lval option) (res: exp) (t: typ) =
 	          let prev = !prechunk () in
@@ -4806,7 +4813,9 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
             prestype := t
           in
           match !pwhat with
-          | ADrop -> addCall None zero intType
+          | ADrop ->
+            pwhat' := AExpLeaveArrayFun;
+            addCall None zero intType
           | AType -> prestype := !resType'
           | ASet(lv, vtype) when !doCollapseCallCast || (Util.equals (typeSig vtype) (typeSig !resType')) ->
               (* We can assign the result directly to lv *)
@@ -4828,7 +4837,7 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
           end
         end;
 
-        finishExp (!prechunk ()) !pres !prestype)
+        finishExp ~newWhat:!pwhat' (!prechunk ()) !pres !prestype)
 
 
     | A.COMMA el ->
@@ -6503,7 +6512,8 @@ and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function
                unnecessary warning than to break CIL's invariant that
                return statements are inserted properly.  *)
             let instrFallsThrough (i : instr) = match i with
-              Set _ -> true
+            | Pure _
+            | Set _ -> true
             | Call (None, Lval (Var e, NoOffset), _, _, _) ->
                 (* See if this is exit, or if it has the noreturn attribute *)
                 if e.vname = "exit" then false