C parser fixes needed for the LLVM backend

semantics/c/language/common/conversion.k

@@ -81,6 +81,11 @@ module C-CONVERSION
           requires notBool isBoolUType(T')
                andBool M -Int N <=Int bitSizeofType(T')
 
+     rule cast(integerUType #as T'::UType, tv(encodedValue(V::EncodableValue, N::Int, M::Int), integerUType))
+          => tv(encodedValue(V, N, M), T')
+          requires notBool isBoolUType(T')
+               andBool M -Int N <=Int bitSizeofType(T')
+
      /*@ \fromStandard{\source[n1570]{\para{6.3.1.3}{2}}}{
      Otherwise, if the new type is unsigned, the value is converted by
      repeatedly adding or subtracting one more than the maximum value that can

semantics/c/language/common/dynamic.k

@@ -41,13 +41,13 @@ module C-DYNAMIC-SYNTAX
 
      // These hold typed frozen computations -- one each for lvalues, rvalues,
      // and non-converted lvalues.
-     syntax LHold ::= le(K, Type)
-     syntax RHold ::= te(K, UType)
-     syntax NCLHold ::= ncle(K, Type)
+     syntax LHold ::= le(KItem, Type)
+     syntax RHold ::= te(KItem, UType)
+     syntax NCLHold ::= ncle(KItem, Type)
      syntax CompoundExpression ::= compoundExp(K)
      syntax Hold ::= HoldLValue | HoldResult | CompoundExpression
 
-     syntax K ::= stripHold(K) [function]
+     syntax KItem ::= stripHold(KItem) [function]
 
      syntax RValue ::= "voidVal" [klabel(voidVal)]
      syntax RValue ::= "emptyValue"
@@ -93,8 +93,7 @@ module C-DYNAMIC-SYNTAX
      syntax KItem ::= "comma"
      // these are semantic
 
-     syntax KResult ::= initValue(CId, Type, K)
-     syntax NoInit
+     syntax NoInit ::= initValue(CId, Type, K)
      syntax KResult ::= NoInit
 
      syntax CompoundLiteralId ::= compoundLiteral(Int)
@@ -168,18 +167,18 @@ module C-DYNAMIC
 
      context toRVal(HOLE:KItem => reval(HOLE)) [result(RValue)]
 
-     rule stripHold(te(K:K, _)) => K
-     rule stripHold(le(K:K, _)) => K
-     rule stripHold(ncle(K:K, _)) => K
+     rule stripHold(te(K:KItem, _)) => K
+     rule stripHold(le(K:KItem, _)) => K
+     rule stripHold(ncle(K:KItem, _)) => K
      rule stripHold(tv(_, _) #as V::RValue) => checkUse(V)
      rule stripHold(nclv(Loc::SymLoc, T::Type)) => lv(Loc, T)
-     rule stripHold(K:K) => K [owise]
+     rule stripHold(K:KItem) => K [owise]
 
      rule value(tv(V:CValue, _)) => V
      rule value(nclv(Loc:SymLoc, _)) => Loc
-     rule value(te(K:K, _)) => K
-     rule value(le(K:K, _)) => K
-     rule value(ncle(K:K, _)) => K
+     rule value(te(K:KItem, _)) => K
+     rule value(le(K:KItem, _)) => K
+     rule value(ncle(K:KItem, _)) => K
      rule value(compoundExp(K:K)) => K
 
      rule type(tv(_, T::UType)) => type(T)
@@ -209,8 +208,6 @@ module C-DYNAMIC
      rule N:Int => tv(N, utype(cfg:largestUnsigned))
           [structural] // for internal computations
 
-     rule isNoInit(initValue(_, _, .K)) => true
-
      rule fillRHoles(V:RValue, te(L:K := E:K, T::UType)) => te(L := fillRHoles(V, E), T)
      rule fillRHoles(V:RValue, Cast(T::Type, E:K)) => Cast(T, fillRHoles(V, E))
      rule fillRHoles(V:RValue, RHOLE) => V

semantics/c/language/common/expr/relational.k

@@ -444,27 +444,16 @@ module C-COMMON-EXPR-RELATIONAL
           requires Loc  =/=K NullPointer
                andBool Loc' =/=K NullPointer
                andBool notBool sameBase(Loc, Loc')
-               andBool notBool isAdjacent(stripProv(Loc), stripProv(Loc'))
                andBool isCompatibleEqualityTypes(T, T', Loc, Loc')
           [structural]
      rule tv(Loc:SymLoc, T::UType) != tv(Loc':SymLoc, T'::UType)
           => makeTruth(true, T, T')
           requires Loc  =/=K NullPointer
                andBool Loc' =/=K NullPointer
                andBool notBool sameBase(Loc, Loc')
-               andBool notBool isAdjacent(stripProv(Loc), stripProv(Loc'))
                andBool isCompatibleEqualityTypes(T, T', Loc, Loc')
           [structural]
 
-     rule tv(Loc:SymLoc, T::UType) == tv(Loc':SymLoc, T'::UType)
-          => tv(unknown(1), makeTruthType(T, T'))
-          requires isAdjacent(stripProv(Loc), stripProv(Loc'))
-               andBool isCompatibleEqualityTypes(T, T', Loc, Loc')
-     rule tv(Loc:SymLoc, T::UType) != tv(Loc':SymLoc, T'::UType)
-          => tv(unknown(0), makeTruthType(T, T'))
-          requires isAdjacent(stripProv(Loc), stripProv(Loc'))
-               andBool isCompatibleEqualityTypes(T, T', Loc, Loc')
-
      // arithmetic types
      rule isCompatibleEqualityTypes(T1::UType, T2::UType, _, _) => true
           requires (isPromoted(T1) orBool isFloatUType(T1))
@@ -498,11 +487,4 @@ module C-COMMON-EXPR-RELATIONAL
                andBool notBool (isPointerType(type(L)) andBool isNullPointerConstant(R))
                andBool notBool (isPointerType(type(R)) andBool isNullPointerConstant(L))
 
-     syntax Bool ::= isAdjacent(SymLoc, SymLoc) [function, withConfig]
-     rule [[ isAdjacent(loc(S::SymBase, Size:Int), loc(_, 0)) => true ]]
-          <mem>... S |-> object(_, Size, _) ...</mem>
-
-     rule [[ isAdjacent(loc(_, 0), loc(S::SymBase, Size:Int)) => true ]]
-          <mem>... S |-> object(_, Size, _) ...</mem>
-     rule isAdjacent(_, _) => false [owise]
 endmodule

semantics/c/language/common/memory/reading.k

@@ -171,11 +171,11 @@ module C-MEMORY-READING
           requires NumBits >Int 0
      rule extractBitsFromList-aux(_, 0, 0, Done::List) => dataList(Done)
 
-     syntax KItem ::= interpret(UType, BitValue)
+     syntax RValue ::= interpret(UType, BitValue) [function]
      rule interpret(integerUType #as T::UType, I:Int)
           => #if max(T) >=Int I #then tv(I, T) #else interpret(T, I -Int (1 <<Int absInt(bitSizeofType(T)))) #fi
      rule interpret(integerUType #as T::UType, encodedPtr(NullPointer, _, _)) => tv(unknown(0), T)
-     rule <k> interpret(T::UType, I:Int) => interpretPointer(T, I, Mem) ...</k>
+     rule [[ interpret(T::UType, I:Int) => interpretPointer(T, I, Mem) ]]
           <mem> Mem::Map </mem>
           requires isPointerUType(T)
      rule interpret(ut(... st: _:SimpleFloatType) #as T::UType, 0) => tv(zeroCFloat(T), T)

semantics/c/language/common/syntax.k

@@ -6,14 +6,15 @@ endmodule
 
 module C-SYNTAX
      imports C-SORTS
+     imports COMPAT-SORTS
      imports C-REVAL-SYNTAX
      imports INT-SYNTAX
      imports STRING-SYNTAX
      imports COMMON-SYNTAX
 
      syntax KResult ::= SpecifierElem
 
-     syntax KItem ::= Block(Int, KItem) [avoid]
+     syntax KItem ::= Block(Int, StrictList) [avoid]
 
      /*
      type cabsloc = {
@@ -263,7 +264,7 @@ module C-SYNTAX
         should be printed as just T *)
      | CALL of expression * expression list
      */
-     syntax KItem ::= Call(K, K) [symbol]
+     syntax KItem ::= Call(KItem, KItem) [symbol]
      context Call((HOLE:KItem => reval(HOLE)), _) [ndheat, result(RValue)]
      /*
      | MEMBEROF of expression * string
@@ -276,6 +277,6 @@ module C-SYNTAX
      and attribute = String * expression list
      */
      // String, List
-     syntax KItem ::= Attribute(String, KItem) [symbol]
+     syntax KItem ::= Attribute(String, StrictList) [symbol]
 
 endmodule

semantics/c/language/common/type-builder.k

@@ -67,8 +67,8 @@ module C-TYPE-BUILDER
      rule restrict(T:FlexType) => addQualifier(Restrict(), expand(T))
 
      rule typeref(S:String) => #typeref(Identifier(S))
-     syntax Type ::= #typeref(CId) [function, withConfig]
 
+     syntax Type ::= #typeref(CId) [function, withConfig]
      rule [[ #typeref(X:CId) => T ]]
           <external-defs>... X |-> Base:SymBase ...</external-defs>
           <mem>... Base |-> object(T:Type, _, _) ...</mem> 

semantics/c/language/common/typing/common.k

@@ -121,7 +121,7 @@ module C-TYPING-COMMON
      rule hasNoName(_) => false [owise]
 
      rule [[ getTagInfo(tag(X::CId, Tu::String, B::BlockRef))
-          => extractTagInfo({M[Tu] orDefault .Map}:>Map[tag(X, Tu, B)]) ]]
+          => extractTagInfo({M[Tu] orDefault .Map}:>Map[tag(X, Tu, B)] orDefault #incomplete) ]]
           <global>... <tags> M::Map </tags> ...</global>
 
      syntax TagInfo ::= extractTagInfo(K) [function]

semantics/c/language/common/typing/effective.k

@@ -64,7 +64,7 @@ module C-TYPING-EFFECTIVE
           requires Loc =/=K NullPointer
      rule updateLastAccessVariant(Loc::SymLoc, _, _) => Loc [owise]
 
-     rule <k> getLastAccessType(loc(Base::SymBase, _, _:Set SetItem(objectType(T::Type))))
+     rule <k> getLastAccessType(loc(Base::SymBase, _, SetItem(objectType(T::EffectiveType)) _::Set))
                => fixFlexibleType(T, Len)
           ...</k>
           <mem>... Base |-> object(_, Len::Int, _) ...</mem>

semantics/c/language/execution/init.k

@@ -5,7 +5,7 @@ module C-EXECUTION-INIT-SYNTAX
      imports COMMON-SORTS
      syntax KItem ::= pgmArgs(List) [function]
      syntax KItem ::= incomingArguments(List)
-     syntax KItem ::= callEntryPoint(String, Int, K)
+     syntax KItem ::= callEntryPoint(String, Int, KItem)
      syntax KItem ::= initMainThread(String)
      syntax KItem ::= "initMainThread'" "(" String ")"
      syntax KItem ::= "callAtExit" | "callAtQuickExit"
@@ -85,23 +85,21 @@ module C-EXECUTION-INIT
           => tv(NullPointer, utype(pointerType(type(void))))
 
      syntax Type ::= strType(String) [function]
-     rule strType(S:String)
+     rule strType(S::String)
           => type(arrayType(type(char), lengthString(S) +Int 1))
 
-     syntax KItem ::= "incomingArguments-aux" "(" List "," Int ")"
-
-     rule incomingArguments(L:List) => incomingArguments-aux(L, 0)
+     rule incomingArguments(L::List) => #incomingArguments(L, 0)
           [structural]
-     rule incomingArguments-aux(ListItem(S:String) L:List, N:Int)
+
+     syntax KItem ::= #incomingArguments(List, Int)
+     rule #incomingArguments(ListItem(S:String) L::List, N::Int)
           => allocObject(bnew(N +Int 1, strType(S), argv), strType(S))
           ~> writeString(lnew(bnew(N +Int 1, strType(S), argv)), S)
-          ~> Initializer(*(mainArguments + tv(N, utype(int)))
-               := lv(lnew(bnew(N +Int 1, strType(S), argv)), strType(S)))
-          ~> incomingArguments-aux(L:List, N:Int +Int 1)
+          ~> Initializer(*(mainArguments + tv(N, utype(int))) := lv(lnew(bnew(N +Int 1, strType(S), argv)), strType(S)))
+          ~> #incomingArguments(L, N +Int 1)
           [structural]
-     rule incomingArguments-aux(.List, N:Int)
-          => Initializer(*(mainArguments + tv(N, utype(int)))
-               := NullPointerConstant)
+     rule #incomingArguments(.List, N::Int)
+          => Initializer(*(mainArguments + tv(N, utype(int))) := NullPointerConstant)
           [structural]
 
      rule pgmArgs(L:List)
@@ -193,9 +191,9 @@ module C-EXECUTION-INIT
 
      /*@ this bit of indirection is used to check that the main prototype is
       correct, and to call it with the appropriate arguments */
-     rule <k> callEntryPoint(EP::String, N::Int, Args:K)
+     rule <k> callEntryPoint(EP::String, N::Int, Args::KItem)
                => enterRestrictTU
-               ~> reval(#callEntryPoint(EP, N, mainArguments, Args, T))
+               ~> reval(#callEntryPoint(EP, N, Args, T))
                ~> callAtExit
           ...</k>
           <types>... Identifier(EP) |-> T::Type ...</types>
@@ -206,14 +204,14 @@ module C-EXECUTION-INIT
      rule getEntryPoint(_) => "main" [owise]
 
      // int main(void) -- also, int main() gets normalized to main(void)
-     syntax K ::= #callEntryPoint(String, Int, CId, K, Type) [function]
-     rule #callEntryPoint(Entry::String, _, _, _,
+     syntax K ::= #callEntryPoint(String, Int, KItem, Type) [function]
+     rule #callEntryPoint(Entry::String, _, _,
                t(quals(.Set), _, functionType(ut(.Set, int),
                     ListItem(typedDeclaration(t(quals(.Set), .Set, void), _)))))
           => Call(Identifier(Entry), list(.List))
      // int main(int argc, char* argv[]), int main(int argc, char** argv), and old style (no prototype).
-     rule #callEntryPoint(Entry::String, N::Int, X::CId, Args:K, _)
-          => Args ~> Call(Identifier(Entry), list(ListItem(tv(N, utype(int))) ListItem(X)))
+     rule #callEntryPoint(Entry::String, N::Int, Args::KItem, _)
+          => Args ~> Call(Identifier(Entry), list(ListItem(tv(N, utype(int))) ListItem(mainArguments)))
           [owise]
 
      rule <k> reval(V:RValue) ~> callAtExit => AtExit ~> reval(V) ~> callAtExit ...</k>
@@ -231,8 +229,7 @@ module C-EXECUTION-INIT
           <status> _ => mainExited </status>
 
      // fixme I'm not sure threads clean up their memory
-     rule [terminate]:
-          <exec>...
+     rule <exec>...
                (<thread>...
                     // main's thread, not the global "thread"
                     <thread-id> 0 </thread-id>

semantics/c/language/translation/decl/initializer.k

@@ -41,9 +41,9 @@ module C-DECL-INITIALIZER
           [structural]
 
      // aggregates
-     rule figureInit(X:CId, aggregateOrUnionType #as T::Type, CompoundInit(L:KItem))
+     rule figureInit(X:CId, aggregateOrUnionType #as T::Type, CompoundInit(list(L::List)))
           => giveType(X, T)
-          ~> figureInit-aux(X, T, startInit(T, X, CompoundInit(L)))
+          ~> figureInit-aux(X, T, startInit(T, X, L))
           requires notBool (isIncompleteStringType(T) andBool isCompoundStringInit(L))
           [structural]
 
@@ -126,8 +126,8 @@ module C-DECL-INITIALIZER
      rule isIncompleteStringType(t(_, _, incompleteArrayType(charType))) => true
      rule isIncompleteStringType(_) => false [owise]
 
-     syntax Bool ::= isCompoundStringInit(KItem) [function]
-     rule isCompoundStringInit(list(ListItem(InitFragment(NextInit(), SingleInit(StringLiteral(_)))))) => true
+     syntax Bool ::= isCompoundStringInit(List) [function]
+     rule isCompoundStringInit(ListItem(InitFragment(NextInit(), SingleInit(StringLiteral(_))))) => true
      rule isCompoundStringInit(_) => false [owise]
 
      // id, type, initializer
@@ -163,8 +163,8 @@ module C-DECL-INITIALIZER
           <curr-object> _:List => .List </curr-object>
           <saved-init> K:K => .K </saved-init>
 
-     syntax KItem ::= startInit(Type, CId, K)
-     rule <k> startInit(aggregateOrUnionType #as T::Type, X:CId, CompoundInit(list(L:List)))
+     syntax KItem ::= startInit(Type, CId, List)
+     rule <k> startInit(aggregateOrUnionType #as T::Type, X:CId, L:List)
                => fillInits(L) ~> getInit
           ...</k>
           <incomplete-length> _ => 0 </incomplete-length>
@@ -225,7 +225,7 @@ module C-DECL-INITIALIZER
      rule <k> subobjectKCell #as Init:KItem ...</k>
           <curr-subobject>
                (ListItem(down) => ListItem(firstField(K, findFieldNames(T), T)))
-               ListItem(ncle(K:K, structOrUnionType #as T::Type))
+               ListItem(ncle(K:KItem, structOrUnionType #as T::Type))
           ...</curr-subobject>
           <curr-object> Obj::List </curr-object>
           requires notBool (isInFieldInit(Init) andBool structOrUnionAtTop(Obj))
@@ -341,7 +341,7 @@ module C-DECL-INITIALIZER
           ...</k>
           <curr-subobject>
                (.List => ListItem(down))
-               ListItem(ncle(K:K, aggregateOrUnionType #as T::Type))
+               ListItem(ncle(K:KItem, aggregateOrUnionType #as T::Type))
                Remainder::List
           </curr-subobject>
           <curr-object>
@@ -377,7 +377,7 @@ module C-DECL-INITIALIZER
           <curr-subobject>
                _:List => ListItem(block) ListItem(ncle(K, T))
           </curr-subobject>
-          <curr-object> ListItem(ncle(K:K, structOrUnionType #as T::Type)) ...</curr-object>
+          <curr-object> ListItem(ncle(K:KItem, structOrUnionType #as T::Type)) ...</curr-object>
           [structural]
      // fixme does this need to worry about incompleteLength_
      rule <k> fillInit(InitFragment(AtIndexInit(Index:KItem, K':KItem), Exp:KItem))
@@ -387,7 +387,7 @@ module C-DECL-INITIALIZER
           <curr-subobject>
                _:List => ListItem(block) ListItem(ncle(K, T))
           </curr-subobject>
-          <curr-object> ListItem(ncle(K:K, t(... st: _:SimpleArrayType) #as T::Type)) ...</curr-object>
+          <curr-object> ListItem(ncle(K:KItem, t(... st: _:SimpleArrayType) #as T::Type)) ...</curr-object>
           [structural]
 
      syntax KItem ::= buildDesignator(K)
@@ -396,7 +396,7 @@ module C-DECL-INITIALIZER
           ...</k>
           <curr-subobject>
                ListItem(block) (.List => ListItem(thisField(K, F, findFieldNames(T), T)))
-                    ListItem(ncle(K:K, structOrUnionType #as T::Type))
+                    ListItem(ncle(K:KItem, structOrUnionType #as T::Type))
           ...</curr-subobject>
           [structural]
 
@@ -451,7 +451,7 @@ module C-DECL-INITIALIZER
           [structural]
      rule <k> initializeSingleInit2(T'::Type, _) ...</k>
           <curr-subobject>
-               (.List => ListItem(down)) ListItem(ncle(K:K, T::Type))
+               (.List => ListItem(down)) ListItem(ncle(K:KItem, T::Type))
           ...</curr-subobject>
           requires isAggregateOrUnionType(T)
                andBool notBool isAggregateOrUnionType(T')

semantics/c/language/translation/expr/assignment.k

@@ -91,11 +91,11 @@ module C-EXPR-ASSIGNMENT
           => te(lv(Loc, T) := checkUse(tv(V, T')), stripConstants(utype(T')))
           requires notBool isConstType(T)
                andBool (utype(T) ==Type T')
-     rule nclv(Loc:SymLoc, T::Type) := te(K:K, T'::UType)
+     rule nclv(Loc:SymLoc, T::Type) := te(K:KItem, T'::UType)
           => te(lv(Loc, T) := K, stripConstants(utype(T')))
           requires notBool isConstType(T)
                andBool (utype(T) ==Type T')
-     rule ncle(L:K, T::Type) := R:RValue
+     rule ncle(L:KItem, T::Type) := R:RValue
           => te(L := stripHold(R), stripConstants(utype(R)))
           requires notBool isConstType(T)
                andBool (utype(T) ==Type utype(R))