From 12b11cfffe03c6ac543d64b0054ff1fa54b8d378 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 4 Aug 2020 15:00:51 +0200
Subject: [PATCH] [CilBuilder] Add skip and pure expression building
---
.../ast_building/cil_builder.ml | 56 ++++++++++++-------
.../ast_building/cil_builder.mli | 9 ++-
2 files changed, 43 insertions(+), 22 deletions(-)
diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml
index c59609f5aa9..1ef5a124be6 100644
--- a/src/kernel_services/ast_building/cil_builder.ml
+++ b/src/kernel_services/ast_building/cil_builder.ml
@@ -447,6 +447,7 @@ struct
let incr dest = `instr (Assign (harden_lval dest, harden_exp (add dest one)))
let call res callee args =
`instr (Call (harden_lval_opt res, harden_exp callee, harden_exp_list args))
+
let stmtkind sk = `stmt (CilStmtkind sk)
let stmt s = `stmt (CilStmt s)
let stmts l = `stmt (Sequence (List.map (fun s -> CilStmt s) l))
@@ -666,6 +667,9 @@ struct
let append_stmt b s =
b.stmts <- s :: b.stmts
+ let append_instr b i =
+ append_stmt b (CilInstr i)
+
let append_local v =
let fundec = get_owner () and b = top () in
fundec.Cil_types.slocals <- fundec.Cil_types.slocals @ [v];
@@ -783,26 +787,6 @@ struct
let return exp =
stmtkind (Cil_types.Return (cil_exp_opt ~loc exp, loc))
- (* Instructions *)
-
- let instr i =
- let b = top () in
- append_stmt b (CilInstr i)
-
- let assign lval exp =
- let lval' = cil_lval ~loc lval
- and exp' = cil_exp ~loc exp in
- instr (Cil_types.Set (lval', exp', loc))
-
- let incr lval =
- assign lval (add lval (int 1))
-
- let call dest callee args =
- let dest' = cil_lval_opt ~loc dest
- and callee' = cil_exp ~loc callee
- and args' = cil_exp_list ~loc args in
- instr (Cil_types.Call (dest', callee', args', loc))
-
(* Variables *)
let return_type typ =
@@ -817,7 +801,7 @@ struct
| None -> ()
| Some init ->
let local_init = Cil_types.AssignInit (cil_init ~loc init) in
- instr (Cil_types.Local_init (v, local_init, loc));
+ append_instr b (Cil_types.Local_init (v, local_init, loc));
v.vdefined <- true
end;
append_local v;
@@ -843,6 +827,36 @@ struct
v.Cil_types.vattr <- attributes;
`var v
+
+ (* Instructions *)
+
+ let instr i =
+ let b = top () in
+ append_instr b i
+
+ let assign lval exp =
+ let lval' = cil_lval ~loc lval
+ and exp' = cil_exp ~loc exp in
+ instr (Cil_types.Set (lval', exp', loc))
+
+ let incr lval =
+ assign lval (add lval (int 1))
+
+ let call dest callee args =
+ let dest' = cil_lval_opt ~loc dest
+ and callee' = cil_exp ~loc callee
+ and args' = cil_exp_list ~loc args in
+ instr (Cil_types.Call (dest', callee', args', loc))
+
+ let pure exp =
+ let exp' = cil_exp ~loc exp in
+ let `var v = local' (Cil.typeOf exp') "tmp" ~init:(Exp.exp exp') in
+ v.vdescr <- Some (Format.asprintf "%a" !Cil.pp_exp_ref exp')
+
+ let skip () =
+ instr (Cil_types.Skip (loc))
+
+
(* Operators *)
let (:=) = assign
diff --git a/src/kernel_services/ast_building/cil_builder.mli b/src/kernel_services/ast_building/cil_builder.mli
index 11c744096fa..eb72f9f880d 100644
--- a/src/kernel_services/ast_building/cil_builder.mli
+++ b/src/kernel_services/ast_building/cil_builder.mli
@@ -188,11 +188,14 @@ sig
type instr = [ `instr of instr' ]
type stmt = [ instr | `stmt of stmt' ]
+ (* Instructions *)
val instr : Cil_types.instr -> [> instr]
val skip : [> instr]
val assign : [< lval] -> [< exp] -> [> instr]
val incr : [< lval] -> [> instr]
val call : [< lval | `none] -> [< exp] -> [< exp] list -> [> instr]
+
+ (* Statements *)
val stmtkind : Cil_types.stmtkind -> [> stmt]
val stmt : Cil_types.stmt -> [> stmt]
val stmts : Cil_types.stmt list -> [> stmt]
@@ -224,7 +227,6 @@ sig
include module type of Exp
(* Statements *)
- val instr : Cil_types.instr -> unit
val stmtkind : Cil_types.stmtkind -> unit
val stmt : Cil_types.stmt -> unit
val stmts : Cil_types.stmt list -> unit
@@ -242,9 +244,14 @@ sig
val case : [< exp] -> unit
val break : unit -> unit
val return : [< exp | `none] -> unit
+
+ (* Instructions *)
+ val instr : Cil_types.instr -> unit
+ val skip : unit -> unit
val assign : [< lval] -> [< exp] -> unit
val incr : [< lval] -> unit
val call : [< lval | `none] -> [< exp] -> [< exp] list -> unit
+ val pure : [< exp ] -> unit
(* Variables *)
val return_type : Cil_types.typ -> unit
--
GitLab