Fix hardware address dereferencing and subaddresses (#651)

virgil-serbanuta · web-flow · commit 3a016071b33f · 2021-01-05T13:36:04.000+02:00
* Fix hardware address dereferencing

* Fix hardware address initialization

* Range map for hardware addresses.

* Refactor range maps

* Fix rangeMapAppendSorted

* Fix mergeRangeMaps

* Some more fixes

Co-authored-by: Virgil Serbanuta &lt;virgil.serbanuta&gt;
diff --git a/semantics/c/language/common/conversion.k b/semantics/c/language/common/conversion.k
@@ -30,6 +30,7 @@ module C-CONVERSION
      imports C-SETTINGS-SYNTAX
      imports C-TYPING-EFFECTIVE-SYNTAX
      imports C-TYPING-SYNTAX
+     imports LIST
      imports SET
 
      rule intArithInterpret(T:UType, N:Int) => intArithInterpret(T, N, true)
@@ -284,14 +285,20 @@ module C-CONVERSION
      rule <k>(.K => IMPL("CCV13", "Conversion from an integer to non-null pointer."))
                ~> cast(ut(... st: pointerType(_)) #as T'::UType, tv(V:CValue, integerUType #as T::UType), _)
           ...</k>
-          <hardware-addresses> HwAddr:Set </hardware-addresses>
-          requires notBool isNullPointerConstant(tv(V, T)) andBool notBool V in HwAddr
+          requires notBool isNullPointerConstant(tv(V, T)) andBool notBool #isHardwareAddress(V)
 
      rule <k>(.K => IMPL("CCV13-H", "Conversion from an integer to non-null hardware-dependent pointer."))
                ~> cast(ut(... st: pointerType(_)) #as T'::UType, tv(V:CValue, integerUType #as T::UType), _)
           ...</k>
-          <hardware-addresses>... SetItem(V) ...</hardware-addresses>
-          requires notBool isNullPointerConstant(tv(V, T))
+          requires notBool isNullPointerConstant(tv(V, T)) andBool #isHardwareAddress(V)
+
+     rule [[ #isHardwareAddress(Addr:Int) => rangeMapContains(M, Addr) ]]
+          <hardware-addresses> M:RangeMap </hardware-addresses>
+     rule #isHardwareAddress(Addr:CValue) => false
+          requires notBool isInt(Addr)
+
+     rule [[findHardwareAddress(Addr:Int) => rangeMapFind(M, Addr)]]
+          <hardware-addresses> M:RangeMap </hardware-addresses>
 
      /*@ \fromStandard{\source[n1570]{\para{6.3.2.3}{6}}}{
      Any pointer type may be converted to an integer type. Except as previously
diff --git a/semantics/c/language/common/expr/reference.k b/semantics/c/language/common/expr/reference.k
@@ -70,10 +70,7 @@ module C-COMMON-EXPR-REFERENCE
                andBool Loc =/=K NullPointer
                andBool ifFromArrayInBounds(Loc,
                     utype(pointerType(type(char))), 1) ==K true
-               andBool
-                    (notBool hasLint
-                    orBool notBool (isNativeLoc(Loc) orBool isHardwareLoc(Loc))
-                    )
+               andBool notBool (hasLint andBool isNativeLoc(Loc))
           [structural]
 
      rule (.K => CV("CER6", "Unary '*' operator applied to non-pointer."))
diff --git a/semantics/common/compat.k b/semantics/common/compat.k
@@ -7,6 +7,7 @@ endmodule
 module COMPAT-SYNTAX
      imports COMPAT-SORTS
      imports COMMON-SYNTAX
+     imports LIST
 
      syntax String ::= firstChar(String) [function]
      syntax String ::= lastChar(String) [function]
@@ -78,6 +79,23 @@ module COMPAT-SYNTAX
      // implements List[Idx <- Val]
      syntax List ::= myListUpdate(List, Int, KItem) [function]
 
+
+     // Range map. It is recommended to use .rangeMap and rangeMapAppendSorted
+     // to construct it.
+     syntax RangeMap
+     // A range item contains all integers between start and end, including both
+     // ends.
+     syntax RangeMapItem ::= rangeMapItem(start:Int, end:Int)
+     syntax MaybeRangeMapItem ::= RangeMapItem | "noRangeMapItem"
+
+     syntax RangeMap ::= ".RangeMap"  [function]
+     syntax RangeMap ::= rangeMapAppendSorted(RangeMap, RangeMapItem)  [function]
+     // Each pair of ranges from the two maps be either identical, or disjoint.
+     syntax RangeMap ::= mergeRangeMaps(RangeMap, RangeMap)  [function]
+
+     syntax Bool ::= rangeMapContains(RangeMap, value:Int)  [function]
+     syntax MaybeRangeMapItem ::= rangeMapFind(RangeMap, value:Int)  [function]
+
 endmodule
 
 module COMPAT-KAST [kast]
@@ -102,6 +120,7 @@ module COMPAT
      imports C-CONFIGURATION
      imports K-REFLECTION
      imports BOOL
+     imports LIST
      imports MAP
      imports STRING
 
@@ -294,4 +313,123 @@ module COMPAT
           )
           requires N >Int 0
 
+
+     // The list must be sorted, must contain only RangeMapItem, and the ranges
+     // must be disjoint.
+     syntax RangeMap ::= rangeMap(List)
+
+     syntax RangeMap ::= #mergeRangeMaps(first:RangeMap, second:RangeMap, merged:RangeMap)  [function]
+
+     // (the address at 'start' is <= 'addr') or (start == 0)
+     // (the address at 'end' is >= 'addr') or (end == last-element).
+     // If only one of them is equal to 'addr', we change the other one.
+     syntax MaybeRangeMapItem ::= #rangeMapFind(RangeMap, value:Int, start:Int, end:Int)  [function]
+     syntax MaybeRangeMapItem ::= #rangeMapFindChoice(RangeMap, addr:Int, start:Int, middle:Int, middleItem:RangeMapItem, end:Int)  [function]
+
+     syntax MaybeRangeMapItem ::= #checkInRangeMapItem(value:Int, RangeMapItem)  [function]
+     syntax MaybeRangeMapItem ::= #firstRangeMapItem(MaybeRangeMapItem, MaybeRangeMapItem)  [function]
+
+     syntax Bool ::= isInRangeMapItem(addr:Int, RangeMapItem) [function]
+     syntax RangeMapItem ::= asRangeMapItem(KItem)  [function]
+
+     rule rangeMapContains(M:RangeMap, Value:Int)
+          => isRangeMapItem(rangeMapFind(M, Value))
+
+     rule rangeMapFind(rangeMap(.List), _:Int) => noRangeMapItem
+     rule rangeMapFind(rangeMap(L:List) #as M:RangeMap, Value:Int)
+          => #rangeMapFind(M, Value, 0, size(L) -Int 1)
+          [owise]
+
+     rule #rangeMapFind(rangeMap(L:List), Value:Int, Start:Int, Start)
+          => #checkInRangeMapItem(Value, asRangeMapItem(L[Start]))
+     rule #rangeMapFind(rangeMap(L:List), Value:Int, Start:Int, End:Int)
+          => #firstRangeMapItem(
+               #checkInRangeMapItem(Value, asRangeMapItem(L[Start])),
+               #checkInRangeMapItem(Value, asRangeMapItem(L[End]))
+          )
+          requires Start ==Int End -Int 1
+     rule #rangeMapFind(rangeMap(L:List) #as M:RangeMap, Value:Int, Start:Int, End:Int)
+          => #rangeMapFindChoice(
+               M, Value, Start,
+               (Start +Int End) /Int 2,
+               asRangeMapItem(L[(Start +Int End) /Int 2]),
+               End
+          )
+          requires Start <Int End -Int 1
+
+     rule #rangeMapFindChoice(M:RangeMap, Value:Int, Start:Int, Middle:Int, rangeMapItem(MiddleStart:Int, _:Int), _End:Int)
+          => #rangeMapFind(M, Value, Start, Middle)
+          requires Value <Int MiddleStart
+     rule #rangeMapFindChoice(M:RangeMap, Value:Int, _Start:Int, Middle:Int, rangeMapItem(MiddleStart:Int, _:Int), End:Int)
+          => #rangeMapFind(M, Value, Middle, End)
+          requires Value >=Int MiddleStart
+
+     rule isInRangeMapItem(Value:Int, rangeMapItem(Start:Int, End:Int))
+          => Start <=Int Value andBool Value <=Int End
+
+     rule #checkInRangeMapItem(Value:Int, Item:RangeMapItem) => Item
+          requires isInRangeMapItem(Value, Item)
+     rule #checkInRangeMapItem(_:Int, _:RangeMapItem) => noRangeMapItem  [owise]
+
+     rule #firstRangeMapItem(noRangeMapItem, Item:MaybeRangeMapItem) => Item
+     rule #firstRangeMapItem(Item:RangeMapItem, _) => Item
+
+     rule asRangeMapItem(Item:RangeMapItem) => Item
+
+     rule .RangeMap => rangeMap(.List)
+     rule rangeMapAppendSorted(
+               rangeMap(.List),
+               rangeMapItem(Start:Int, End:Int) #as Item:RangeMapItem
+          )
+          => rangeMap(ListItem(Item))
+     rule rangeMapAppendSorted(
+               rangeMap(
+                    (_::List ListItem(rangeMapItem(_:Int, LastEnd:Int))) #as L::List),
+               rangeMapItem(Start:Int, End:Int) #as Item:RangeMapItem
+          )
+          => rangeMap(L ListItem(Item))
+          requires LastEnd <Int Start andBool Start <=Int End
+
+     rule mergeRangeMaps(First:RangeMap, Second:RangeMap)
+          => #mergeRangeMaps(First, Second, .RangeMap)
+
+     rule #mergeRangeMaps(rangeMap(.List), rangeMap(.List), Merged:RangeMap)
+          => Merged
+     rule #mergeRangeMaps(rangeMap(.List), rangeMap(L::List), rangeMap(Merged::List))
+          => rangeMap(Merged L)
+          requires size(L) >Int 0
+     rule #mergeRangeMaps(rangeMap(L::List), rangeMap(.List), rangeMap(Merged::List))
+          => rangeMap(Merged L)
+          requires size(L) >Int 0
+     rule #mergeRangeMaps(
+               rangeMap(ListItem(rangeMapItem(Start:Int, End:Int) #as FirstItem) FirstRemainder:List),
+               rangeMap(ListItem(rangeMapItem(Start:Int, End:Int)) SecondRemainder:List),
+               Merged:RangeMap
+          )
+          => #mergeRangeMaps(
+               rangeMap(FirstRemainder),
+               rangeMap(SecondRemainder),
+               rangeMapAppendSorted(Merged, FirstItem)
+          )
+     rule #mergeRangeMaps(
+               rangeMap(ListItem(rangeMapItem(FirstStart:Int, _:Int) #as FirstItem) FirstRemainder:List),
+               rangeMap(ListItem(rangeMapItem(SecondStart:Int, _:Int)) _:List) #as Second:RangeMap,
+               Merged:RangeMap
+          )
+          => #mergeRangeMaps(
+               rangeMap(FirstRemainder), Second,
+               rangeMapAppendSorted(Merged, FirstItem)
+          )
+          requires FirstStart <Int SecondStart
+     rule #mergeRangeMaps(
+               rangeMap(ListItem(rangeMapItem(FirstStart:Int, _:Int)) _:List) #as First:RangeMap,
+               rangeMap(ListItem(rangeMapItem(SecondStart:Int, _:Int) #as SecondItem) SecondRemainder:List),
+               Merged:RangeMap
+          )
+          => #mergeRangeMaps(
+               First, rangeMap(SecondRemainder),
+               rangeMapAppendSorted(Merged, SecondItem)
+          )
+          requires FirstStart >Int SecondStart
+
 endmodule
diff --git a/semantics/common/configuration.k b/semantics/common/configuration.k
@@ -5,6 +5,7 @@ module COMMON-CONFIGURATION
   imports SET
   imports STRING-SYNTAX
   imports COMMON-SYNTAX
+  imports COMPAT-SYNTAX
 
   configuration
   <global>
@@ -143,7 +144,7 @@ module COMMON-CONFIGURATION
           </tu>
      </translation-units>
 
-     <hardware-addresses> .Set </hardware-addresses>
+     <hardware-addresses> .RangeMap </hardware-addresses>
    </global>
 
 endmodule
diff --git a/semantics/common/init.k b/semantics/common/init.k
@@ -75,13 +75,22 @@ module COMMON-INIT
      rule <k> reportSuccess => .K ...</k>
           <result-value> _ => 0 </result-value>
 
-     rule initHardwareAddresses(hardwareAddresses(.K)) => .
-     rule <k> initHardwareAddresses(hardwareAddresses((#hardwareAddress(Address:Int, Size:Int) => .K) ~> _:K)) ...</k>
-          <hardware-addresses>... (.Set => SetItem(Address)) ... </hardware-addresses>
+     syntax KItem ::= #initHardwareAddresses(KItem, previousAddress:Int)
+
+     rule initHardwareAddresses(hardwareAddresses(...) #as HwAddr:KItem) => #initHardwareAddresses(HwAddr, -1)
+     rule #initHardwareAddresses(hardwareAddresses(.K), _) => .
+     rule <k> #initHardwareAddresses(
+               hardwareAddresses((#hardwareAddress(Address:Int, Size:Int) #as HwAddr:KItem => .K) ~> _:K),
+               PreviousAddress:Int)
+          ...</k>
           <mem>...
                (.Map =>
                     obj(Address, cfg:bitsPerByte *Int cfg:alignofPointer, hardwareAddress())
                     |-> object(t(quals(.Set), .Set, arrayType(t(quals(.Set), .Set, char), Size)), Size, makeArray(Size, uninit))
                )
           ...</mem>
+          <hardware-addresses>
+               M:RangeMap => rangeMapAppendSorted(M, rangeMapItem(Address, Address +Int Size -Int 1))
+          </hardware-addresses>
+          requires Address >Int PreviousAddress
 endmodule
diff --git a/semantics/common/syntax.k b/semantics/common/syntax.k
@@ -20,6 +20,7 @@ endmodule
 
 module COMMON-SYNTAX
      imports COMMON-SORTS
+     imports LIST
      imports SET
      imports STRING-SYNTAX
 
@@ -63,6 +64,8 @@ module COMMON-SYNTAX
      syntax KItem ::= hardwareAddresses(K)
      syntax KItem ::= #hardwareAddress(Int, Int)
      syntax KItem ::= initHardwareAddresses(KItem)
+     syntax Bool ::= #isHardwareAddress(CValue)  [function, withConfig]
+     syntax MaybeRangeMapItem ::= findHardwareAddress(Int)  [function, withConfig]
 
      syntax LanguageLinkage ::= "CLinkage" | "CPPLinkage"
 
diff --git a/semantics/linking/init.k b/semantics/linking/init.k
@@ -282,7 +282,7 @@ module LINKING-INIT
 
                <translation-units> TUs1::Bag </translation-units>
 
-               <hardware-addresses> HwA1::Set </hardware-addresses>
+               <hardware-addresses> HwA1:RangeMap </hardware-addresses>
           </global>),
           (<global>
                <mem> M2:Map </mem>
@@ -314,7 +314,7 @@ module LINKING-INIT
 
                <translation-units> TUs2::Bag </translation-units>
 
-               <hardware-addresses> HwA2::Set </hardware-addresses>
+               <hardware-addresses> HwA2:RangeMap </hardware-addresses>
           </global>))
           =>
           <global>
@@ -351,7 +351,7 @@ module LINKING-INIT
 
                <translation-units> TUs1 TUs2 </translation-units>
 
-               <hardware-addresses> HwA1 |Set HwA2 </hardware-addresses>
+               <hardware-addresses> mergeRangeMaps(HwA1, HwA2) </hardware-addresses>
           </global>
 
      // TODO(chathhorn): remove redundancy
