From b094c4afa5093382720eaa659ecd1d3339fcdfd9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Recoules?= <frederic.recoules@cea.fr>
Date: Wed, 24 Apr 2019 15:58:02 +0200
Subject: [PATCH] [Kernel] Normalize asm templates by merging adjacent strings
and splitting on newline character
---
src/kernel_internals/parsing/cparser.mly | 4 +--
src/kernel_services/parsetree/cabshelper.ml | 34 ++++++++++++++++++++
src/kernel_services/parsetree/cabshelper.mli | 2 ++
3 files changed, 38 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 29da754e5d2..ed1934a750d 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -969,11 +969,11 @@ statement:
}
| ASM GOTO asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc (Parsing.symbol_start_pos (), Parsing.symbol_end_pos ()) in
- no_ghost [ASM ($3, $5, $6, loc)]
+ no_ghost [ASM ($3, mk_asm_templates $5, $6, loc)]
}
| ASM asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc (Parsing.symbol_start_pos (), Parsing.symbol_end_pos ()) in
- no_ghost [ASM ($2, $4, $5, loc)]
+ no_ghost [ASM ($2, mk_asm_templates $4, $5, loc)]
}
| MSASM { no_ghost [ASM ([], [fst $1], None, snd $1)]}
| TRY block EXCEPT paren_comma_expression block {
diff --git a/src/kernel_services/parsetree/cabshelper.ml b/src/kernel_services/parsetree/cabshelper.ml
index 50d016622a4..73412c8d111 100644
--- a/src/kernel_services/parsetree/cabshelper.ml
+++ b/src/kernel_services/parsetree/cabshelper.ml
@@ -232,6 +232,40 @@ let mk_behavior ?(name=Cil.default_behavior_name) ?(assumes=[]) ?(requires=[])
b_extended = extended;
}
+let mk_asm_templates =
+ let buf = Buffer.create 100 in
+ let rec outer res = function
+ | [] when Buffer.length buf = 0 -> List.rev res
+ | [] ->
+ let res = List.rev @@ Buffer.contents buf :: res in
+ Buffer.clear buf;
+ res
+ | str :: tail -> tail |> outer @@ inner res str 0
+ and inner res template i =
+ if i < String.length template then
+ let c = String.get template i in
+ Buffer.add_char buf c;
+ if c = '\n' then
+ if i < String.length template - 1 then
+ match String.get template @@ i + 1 with
+ | '\t' ->
+ Buffer.add_char buf '\t';
+ let res = Buffer.contents buf :: res in
+ Buffer.clear buf;
+ inner res template @@ i + 2
+ | c ->
+ let res = Buffer.contents buf :: res in
+ Buffer.clear buf;
+ Buffer.add_char buf c;
+ inner res template @@ i + 2
+ else
+ let res = Buffer.contents buf :: res in
+ Buffer.clear buf;
+ res
+ else inner res template @@ i + 1
+ else res in
+ outer []
+
(*
Local Variables:
diff --git a/src/kernel_services/parsetree/cabshelper.mli b/src/kernel_services/parsetree/cabshelper.mli
index 13a295600e7..a4b0498146e 100644
--- a/src/kernel_services/parsetree/cabshelper.mli
+++ b/src/kernel_services/parsetree/cabshelper.mli
@@ -87,3 +87,5 @@ val mk_behavior :
?extended:Logic_ptree.extension list ->
unit ->
Logic_ptree.behavior
+
+val mk_asm_templates : string list -> string list
--
GitLab