Aligning small blocks during temporal analysis

src/plugins/e-acsl/prepare_ast.ml

@@ -22,9 +22,64 @@
 
 open Cil_types
 
+exception Alignment_error of string
+let align_error s = raise (Alignment_error s)
+
+(* Returns true if the list of attributes [attrs] contains an [align]
+ * attribute of [algn] or greater. Returns false otherwise.
+ * Throws an exception if
+ *  - [attrs] contains several [align] attributes specifying different
+ *    alignment
+ *  - [attrs] has a single align attribute with a value which is less than [algn] *)
+let sufficiently_aligned attrs algn =
+  let alignment = List.fold_left (fun acc attr ->
+    match attr with
+    | Attr("align", [AInt i]) ->
+      let alignment = Integer.to_int i in
+      if acc <> 0 && acc <> alignment then
+        (* Multiple align attributes with different values *)
+        align_error "Multiple alignment attributes"
+      else if alignment < algn then
+        (* If there is an alignment attribute it should be greater
+          * or equal to [algn] *)
+        align_error "Insufficient alignment"
+      else
+        alignment
+    | Attr("align", _) ->
+      (* Align attribute with an argument other than a single number,
+      should not happen really *)
+      assert false
+    | _ -> acc
+  ) 0 attrs in
+  if alignment > 0 then true else false
+
+(* Given the type and the list of attributes of [varinfo] ([fieldinfo]) return
+ * true if that [varinfo] ([fieldinfo]) requires to be aligned at the boundary
+ * of [algn] (i.e., less than [algn] bytes and has no alignment attribute *)
+let require_alignment typ attrs algn =
+  if (Cil.bitsSizeOf typ) < algn*8 && not (sufficiently_aligned attrs algn) then
+    true
+  else
+    false
+
 class prepare_visitor prj = object (_)
   inherit Visitor.frama_c_copy prj
 
+  (* Add align attributes to local variables (required by temporal analysis) *)
+  method !vblock _ =
+    if (Temporal.is_enabled ()) then
+      Cil.DoChildrenPost (fun blk ->
+        List.iter (fun vi ->
+          if require_alignment vi.vtype vi.vattr 4; then begin
+            vi.vattr <- Attr("aligned",[AInt(Integer.four)]) :: vi.vattr
+          end)
+        blk.blocals;
+      blk)
+    else
+      Cil.DoChildren
+
+  (* Move variable declared in the body of a switch statement to the outer
+     scope *)
   method !vstmt_aux _ =
     Cil.DoChildrenPost (fun stmt ->
       match stmt.skind with