From 9339c414770044cd477815f1cdadd40d0da5a9ba Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 19 May 2017 13:38:02 +0200
Subject: [PATCH] Aligning small blocks during temporal analysis
---
src/plugins/e-acsl/prepare_ast.ml | 55 +++++++++++++++++++++++++++++++
1 file changed, 55 insertions(+)
diff --git a/src/plugins/e-acsl/prepare_ast.ml b/src/plugins/e-acsl/prepare_ast.ml
index cece0929519..980326a32fb 100644
--- a/src/plugins/e-acsl/prepare_ast.ml
+++ b/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
--
GitLab