[eacsl] Add constructor functions to manipulate expressions and statements

src/plugins/e-acsl/src/code_generator/constructor.ml

@@ -26,7 +26,31 @@ open Cil_types
 (* Expressions *)
 (* ********************************************************************** *)
 
-let mk_deref ~loc lv = Cil.new_exp ~loc (Lval(Mem(lv), NoOffset))
+let extract_uncoerced_lval e =
+  let rec aux e =
+    match e.enode with
+    | Lval _ -> Some e
+    | CastE (_, e) -> aux e
+    | _ -> None
+  in
+  aux e
+
+let mk_lval ~loc lval =
+  Cil.new_exp ~loc (Lval lval)
+
+let mk_deref ~loc lv = mk_lval ~loc (Mem lv, NoOffset)
+
+let mk_subscript ~loc array idx =
+  match extract_uncoerced_lval array with
+  | Some { enode = Lval lval } ->
+    let subscript_lval = Cil.addOffsetLval (Index(idx, NoOffset)) lval in
+    mk_lval ~loc subscript_lval
+  | Some _ | None ->
+    Options.fatal
+      ~current:true
+      "Trying to create a subscript on an array that is not an Lval: %a"
+      Cil_types_debug.pp_exp
+      array
 
 (* ********************************************************************** *)
 (* Statements *)
@@ -34,8 +58,16 @@ let mk_deref ~loc lv = Cil.new_exp ~loc (Lval(Mem(lv), NoOffset))
 
 let mk_stmt sk = Cil.mkStmt ~valid_sid:true sk
 let mk_instr i = mk_stmt (Instr i)
+let mk_block_stmt blk = mk_stmt (Block blk)
 let mk_call ~loc ?result e args = mk_instr (Call(result, e, args, loc))
 
+let mk_assigns ~loc ~result e = mk_instr (Set(result, e, loc))
+
+let mk_if ~loc ~cond ?(else_blk=Cil.mkBlock []) then_blk =
+  mk_stmt (If (cond, then_blk, else_blk, loc))
+
+let mk_break ~loc = mk_stmt (Break loc)
+
 type annotation_kind =
   | Assertion
   | Precondition
@@ -59,7 +91,7 @@ let mk_block stmt b = match b.bstmts with
      | Instr(Skip _) -> stmt
      | _ -> assert false)
   | [ s ] -> s
-  |  _ :: _ -> mk_stmt (Block b)
+  |  _ :: _ -> mk_block_stmt b
 
 (* ********************************************************************** *)
 (* E-ACSL specific code *)

src/plugins/e-acsl/src/code_generator/constructor.mli

@@ -25,13 +25,54 @@
 open Cil_types
 open Cil_datatype
 
+(* ********************************************************************** *)
+(* Expressions *)
+(* ********************************************************************** *)
+
+val extract_uncoerced_lval: exp -> exp option
+(** Unroll the [CastE] part of the expression until an [Lval] is found, and
+    return it.
+
+    If at some point the expression is neither a [CastE] nor an [Lval], then
+    return [None]. *)
+
+val mk_lval: loc:location -> lval -> exp
+(** Construct an lval expression from an lval. *)
+
 val mk_deref: loc:Location.t -> exp -> exp
 (** Construct a dereference of an expression. *)
 
+val mk_subscript: loc:location -> exp -> exp -> exp
+(** [mk_subscript ~loc array idx] Create an expression to access the [idx]'th
+    element of the [array]. *)
+
+(* ********************************************************************** *)
+(* Statements *)
+(* ********************************************************************** *)
+
+val mk_stmt: stmtkind -> stmt
+(** Create a statement from a statement kind. *)
+
 val mk_block: stmt -> block -> stmt
 (** Create a block statement from a block to replace a given statement.
     Requires that (1) the block is not empty, or (2) the statement is a skip. *)
 
+val mk_block_stmt: block -> stmt
+(** Create a block statement from a block *)
+
+val mk_assigns: loc:location -> result:lval -> exp -> stmt
+(** [mk_assigns ~loc ~result value] create a statement to assign the [value]
+    expression to the [result] lval. *)
+
+val mk_if:
+  loc:location -> cond:exp -> ?else_blk:block -> block -> stmt
+(** [mk_if ~loc ~cond ~then_blk ~else_blk] create an if statement with [cond]
+    as condition and [then_blk] and [else_blk] as respectively "then" block and
+    "else" block. *)
+
+val mk_break: loc:location -> stmt
+(** Create a break statement *)
+
 (* ********************************************************************** *)
 (* E-ACSL specific code: build calls to its RTL API *)
 (* ********************************************************************** *)