Pragma pack (#652)

* parser: emit #pragma pack

* ignore unknown pragmas again

* Docker: build with any user id

* stdlib depends on the hardware-addresses file

* WIP pack

* move stuff to translation semantics

* fix missing import

* pragma pack

* try fix Jenkinsfile

* try fix Jenkinsfile

* try fix Jenkinsfile

* try fix Jenkinsfile

* try fix jenkinsfile

* try fix Jenkinsfile

* try fix Jenkinsfile

* Try fix Jenkinsfile

* Try fix Jenkinsfile

* see what happens

* It looks like something strips the command

* There is probably a newline comming from sh

* cache MaxAlign in fieldInfo

* Remove commented code

Author: h0nzZik

Diff for: Dockerfile

@@ -20,7 +20,11 @@ RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.7 \
     && cd ../..                                                     \
     && rm -rf z3
 
+ARG USER_ID=1000
+ARG GROUP_ID=1000
+
 # This user is set up in the runtimeverificationinc/kframework:* images.
+RUN usermod -u $USER_ID user
 USER user:user
 
 ##################
@@ -58,3 +62,5 @@ RUN cd ${DEPS_DIR}/k \
       -Dcheckstyle.skip
 
 ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin"
+
+ENTRYPOINT ["./scripts/docker-entrypoint.sh"]

Diff for: Jenkinsfile

@@ -21,7 +21,9 @@ pipeline {
         } }
         stage ( 'Build docker image' ) { steps {
           script {
-            img = docker.build "c-semantics:${env.CHANGE_ID}"
+            def uid = sh([returnStdout: true, script: 'id -u']).trim()
+            def gid = sh([returnStdout: true, script: 'id -g']).trim()
+            img = docker.build("c-semantics:${env.CHANGE_ID}", "--build-arg=USER_ID=${uid} --build-arg=GROUP_ID=${gid} .")
           }
         } }
         stage ( 'Compile' ) {

Diff for: Makefile

@@ -207,6 +207,7 @@ $(LIBSTDCXX_SO): $(call timestamp_of,c-cpp-linking) \
                  $(call timestamp_of,cpp-translation) \
                  $(wildcard $(PROFILE_DIR)/compiler-src/*.C) \
                  $(foreach d,$(SUBPROFILE_DIRS),$(wildcard $(d)/compiler-src/*)) \
+                 $(OUTPUT_DIR)/hardware-addresses.timestamp \
                  PROFILE_DEPS
 	@$(LOGGER) "$(PROFILE): Translating the C++ standard library..."
 	@cd $(PROFILE_DIR)/compiler-src && \
@@ -230,6 +231,7 @@ $(LIBC_SO): $(call timestamp_of,c-cpp-linking) \
             $(call timestamp_of,c-translation) \
             $(wildcard $(PROFILE_DIR)/src/*.c) \
             $(foreach d,$(SUBPROFILE_DIRS),$(wildcard $(d)/src/*.c)) \
+            $(OUTPUT_DIR)/hardware-addresses.timestamp \
             PROFILE_DEPS
 	@$(LOGGER) "$(PROFILE): Translating the C standard library..."
 	@cd $(PROFILE_DIR)/src && \

Diff for: parser/cabs.ml

@@ -315,6 +315,7 @@ and expression =
   | LTL_O of string * expression
 (*   | LTL_UNTIL of expression * expression
   | LTL_RELEASE of expression * expression *)
+  | PACK of expression
 
 and generic_association =
 	| GENERIC_PAIR of type_name * expression

Diff for: parser/clexer.mll

@@ -612,10 +612,11 @@ and hash = parse
                   (* A file name may follow *)
 		  file lexbuf }
 | "line"        { addWhite lexbuf; hash lexbuf } (* MSVC line number info *)
+| "pragma" blank "pack" { PRAGMA_PACK }
                 (* For pragmas with irregular syntax, like #pragma warning, 
                  * we parse them as a whole line. *)
 | "pragma" blank
-                { addWhite lexbuf; hash lexbuf }
+                { (*pragmaLine := true;*) PRAGMA (currentLoc ()) ; addWhite lexbuf; hash lexbuf }
 | _	        { addWhite lexbuf; endline lexbuf}
 
 and file =  parse 

Diff for: parser/cparser.mly

@@ -289,6 +289,7 @@ let trd3 (_, _, result) = result
 %token<Cabs.cabsloc> BEGINANNOTATION ENDANNOTATION
 %token<Cabs.cabsloc> PROPERTY
 %token LTL ATOM LTL_BUILTIN_TOK
+%token PRAGMA_PACK
 %token BACKTICK BACKSLASH
 
 /* sm: cabs tree transformation specification keywords */
@@ -1315,10 +1316,16 @@ pragma:
 | PRAGMA attr SEMICOLON PRAGMA_EOL	{ PRAGMA ($2, $1) }
 | PRAGMA_LINE                           { PRAGMA (VARIABLE (fst $1), 
                                                   snd $1) }
+| PRAGMA_PACK pragma_pack { $2 }
 | PRAGMA LTL ltl_pragma PRAGMA_EOL { $3 }
 | PRAGMA PRAGMA_EOL { PRAGMA (VARIABLE "", $1) }
 ;
 
+pragma_pack:
+| LPAREN RPAREN { PRAGMA (PACK NOTHING, $1) }
+| LPAREN constant RPAREN { PRAGMA (PACK (CONSTANT (fst $2)), $1) }
+
+
 ltl_pragma:
 | IDENT COLON ltl_expression	{ LTL_ANNOTATION ((fst $1), (fst $3), (snd $1)) }
 

Diff for: parser/kPrinter.ml

@@ -488,6 +488,7 @@ and expression =
     | GNU_BODY blk                                               -> kapply KItem "GnuBody" [lazy_block blk KItem]
     | BITMEMBEROF (exp, fld)                                     -> kapply KItem "DotBit" [lazy_expression exp KItem; identifier fld CId]
     | EXPR_PATTERN s                                             -> kapply KItem "ExpressionPattern" [ktoken_string s String]
+    | PACK exp                                                   -> kapply KItem "PragmaPack" [lazy_expression exp KItem]
 and lazy_expression = fun a sort -> LazyPrinter ((fun aa -> expression aa sort), a)
 
 and type_spec =

Diff for: profiles/x86-gcc-limited-libc/semantics/c-settings.k

@@ -65,7 +65,8 @@ module C-SETTINGS
      rule cfg:alignofOversizedFloat => 16
      rule cfg:alignofPointer => 8
      // Max of the above.
-     rule cfg:alignofMalloc => 16
+     rule cfg:defaultMaxAlign => 16
+     rule cfg:alignofMalloc => cfg:defaultMaxAlign
 
      rule cfg:intToPointer(0, _) => NullPointer
      rule cfg:intToPointer(_, _) => trap [owise]

Diff for: scripts/docker-build

@@ -0,0 +1,3 @@
+#!/bin/bash
+docker build --build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g) -t old-c-semantics .
+docker run --rm --mount src=$(pwd),target=/home/user/c-semantics,type=bind --workdir=/home/user/c-semantics old-c-semantics make

Diff for: scripts/docker-entrypoint.sh

@@ -0,0 +1,5 @@
+#!/bin/bash
+
+eval $(opam config env)
+eval $(perl -I "~/perl5/lib/perl5" -Mlocal::lib)
+exec "$@"

Diff for: scripts/rid

@@ -0,0 +1,3 @@
+#!/bin/bash
+# run-in-docker (rid)
+docker run --rm --mount src=$(pwd),target=/home/user/c-semantics,type=bind --workdir=/home/user/c-semantics old-c-semantics "$@"

Diff for: semantics/c/language/common/alignment.k

@@ -68,16 +68,9 @@ module C-ALIGNMENT
      // TODO(dwightguth): make sure we correctly handle all the corner cases
      rule byteAlignofType'(_) => 1 [owise]
 
-     rule maxByteAlignofDecls(L:List) => maxByteAlignofDecls'(1, L)
-
-     syntax Int ::= "maxByteAlignofDecls'" "(" Int "," List ")" [function]
-     rule maxByteAlignofDecls'(Sz::Int, ListItem(typedDeclaration(T::Type, _)) LL:List)
-          => maxByteAlignofDecls'(maxInt(Sz, byteAlignofType(T)), LL)
-     rule maxByteAlignofDecls'(Sz::Int, .List) => Sz
-
      syntax Int ::= byteAlignofTagged(TagInfo) [function]
-     rule byteAlignofTagged(fieldInfo(Decls:List, _, _, _, _))
-          => maxByteAlignofDecls(Decls)
+     rule byteAlignofTagged(fieldInfo(_, _, _, _, _, MaxAlign:Int))
+          => MaxAlign
      rule byteAlignofTagged(enumInfo(... enumAlias: T::SimpleIntegerType))
           => byteAlignofType'(type(T))
      rule byteAlignofTagged(_) => 1 [owise]

Diff for: semantics/c/language/common/bitsize.k

@@ -62,7 +62,7 @@ module C-BITSIZE
      rule maxByteSizeofList'(Sz:Int, .List) => Sz
 
      syntax Int ::= bitSizeofFields(FieldInfo) [function]
-     rule bitSizeofFields(fieldInfo(_, NBits:Int, _, _, _)) => NBits
+     rule bitSizeofFields(fieldInfo(_, NBits:Int, _, _, _, _)) => NBits
      rule bitSizeofFields(_) => 0 [owise]
 
 endmodule

Diff for: semantics/c/language/common/memory/writing.k

@@ -195,8 +195,8 @@ module C-MEMORY-WRITING
 
      syntax KItem ::= initStructPadding(SymLoc, FieldInfo, Bool)
      rule (.K => initPaddingByte(Loc +bits I, Trap))
-          ~> initStructPadding(Loc::SymLoc, fieldInfo(_, Sz::Int, _, _, (SetItem(I::Int) => .Set) _), Trap::Bool)
-     rule initStructPadding(_, fieldInfo(_, _, _, _, .Set), _) => .K
+          ~> initStructPadding(Loc::SymLoc, fieldInfo(_, Sz::Int, _, _, (SetItem(I::Int) => .Set) _, _), Trap::Bool)
+     rule initStructPadding(_, fieldInfo(_, _, _, _, .Set, _), _) => .K
 
      syntax K ::= initFieldPadding(SymLoc, Type, CId, Bool) [function]
      rule initFieldPadding(Loc::SymLoc, T::Type, F::CId, Trap::Bool)
@@ -347,7 +347,7 @@ module C-MEMORY-WRITING
      rule splitStructPartialBytes(_, _, 0) => .List
 
      syntax Bool ::= isPaddingOffset(Int, K) [function]
-     rule isPaddingOffset(Offset::Int, fieldInfo(_, _, _, _, PaddingOffs::Set))
+     rule isPaddingOffset(Offset::Int, fieldInfo(_, _, _, _, PaddingOffs::Set, _))
           => Offset *Int cfg:bitsPerByte in PaddingOffs
 
      rule writeChars(Loc::SymLoc, S::String)

Diff for: semantics/c/language/common/settings.k

@@ -44,6 +44,7 @@ module C-SETTINGS-SYNTAX
      syntax Int ::= "cfg:alignofLongDouble" [function]
      syntax Int ::= "cfg:alignofOversizedFloat" [function]
      syntax Int ::= "cfg:alignofPointer" [function]
+     syntax Int ::= "cfg:defaultMaxAlign" [function]
      syntax Int ::= "cfg:alignofMalloc" [function]
 
      syntax UType

Diff for: semantics/c/language/common/typing.k

@@ -62,7 +62,7 @@ module C-TYPING-SYNTAX
 
      // TODO(chathhorn): move?
      // Offsets and field names for structs and unions.
-     syntax FieldInfo ::= fieldInfo(List, Int, Map, Map, Set)
+     syntax FieldInfo ::= fieldInfo(List, Int, Map, Map, Set, Int)
      syntax EnumInfo ::= enumInfo(enumAlias: SimpleIntegerType, ctMap: Map)
      syntax TagInfo ::= FieldInfo | EnumInfo
      syntax SimpleIntegerType ::= getEnumAlias(TagId) [function]

Diff for: semantics/c/language/common/typing/common.k

@@ -115,7 +115,7 @@ module C-TYPING-COMMON
 
      syntax FieldInfo ::= toFieldInfo(TagInfo) [function]
      rule toFieldInfo(Fields:FieldInfo) => Fields
-     rule toFieldInfo(_) => fieldInfo(.List, 0, .Map, .Map, .Set) [owise]
+     rule toFieldInfo(_) => fieldInfo(.List, 0, .Map, .Map, .Set, 0) [owise]
 
      syntax Bool ::= hasNoName(Map) [function]
      rule hasNoName((_:NoName |-> structOrUnionType) _::Map) => true
@@ -126,7 +126,7 @@ module C-TYPING-COMMON
           <global>... <tags> M::Map </tags> ...</global>
 
      syntax TagInfo ::= extractTagInfo(K) [function]
-     rule extractTagInfo(fieldInfo(L::List, I::Int, M1::Map, M2::Map, S::Set)) => fieldInfo(L, I, M1, M2, S)
+     rule extractTagInfo(fieldInfo(L::List, I::Int, M1::Map, M2::Map, S::Set, MaxAlign::Int)) => fieldInfo(L, I, M1, M2, S, MaxAlign)
      rule extractTagInfo(enumInfo(...) #as EI::EnumInfo) => EI
      rule extractTagInfo(_) => #incomplete [owise]
 

Diff for: semantics/c/language/common/typing/compatibility.k

@@ -113,7 +113,8 @@ module C-TYPING-COMPATIBILITY
                     Cache SetItem(kpair(S, S'))))
 
      syntax Bool ::= #areStructsCompat(FieldInfo, FieldInfo, Set) [function, memo]
-     rule #areStructsCompat(fieldInfo(Fs::List, _, _, _, _), fieldInfo(Fs'::List, _, _, _, _), Cache::Set)
+     // TODO: are they compatible even if one was packed using attribute or pragma?
+     rule #areStructsCompat(fieldInfo(Fs::List, _, _, _, _, _), fieldInfo(Fs'::List, _, _, _, _, _), Cache::Set)
           => #areCompatFields(Fs, Fs', Cache)
           requires Fs =/=K .List andBool Fs' =/=K .List
      rule #areStructsCompat(_, _, _) => true [owise]