Minor refactor.

Author: chathhorn

semantics/common/alignment.k

@@ -2,7 +2,7 @@ module ALIGNMENT-SYNTAX
      imports SYMLOC-SORTS
      imports INT-SYNTAX
 
-     syntax Int ::= getAlign(SymLoc) [function]
+     syntax Int ::= getAlign(SymLoc) [function, withConfig]
      syntax Int ::= getNativeAlign(address: Int, max: Int) [function]
 endmodule
 
@@ -14,16 +14,24 @@ module ALIGNMENT
      imports C-SETTINGS-SYNTAX
 
      rule getAlign(NullPointer) => cfg:alignofMalloc
-     rule getAlign(Loc::SymLoc) => getAlign'(base(Loc), offset(Loc)) [owise]
-     syntax Int ::= "getAlign'" "(" SymBase "," Int ")" [function, withConfig]
+     rule getAlign(Loc::SymLoc) => getAlign'(base(Loc), offset(Loc))
+          requires notBool isLinkerLoc(Loc)
+     rule [[ getAlign(Loc::SymLoc => resolveLinking(Loc, Linkings)) ]]
+          <linkings> Linkings::Map </linkings>
+          requires isLinkerLoc(Loc) andBool base(Loc) in_keys(Linkings)
+     rule getAlign(Loc::SymLoc) => getAlign'(base(Loc), offset(Loc))
+          [owise]
+
+     syntax Int ::= "getAlign'" "(" SymBase "," Int ")" [function]
+     rule getAlign'(obj(... align: Align::Int)::DirectBase, I::Int) => getNativeAlign(I, Align)
+     rule getAlign'(obj(... align: Align::Int)::LinkBase, I::Int) => getNativeAlign(I, Align)
+
+     rule getNativeAlign(_, 0) => 0
+     rule getNativeAlign(Address::Int, Max::Int) => #getNativeAlign(Address %Int Max, Max, 1) [owise]
 
-     rule getAlign'(obj(... align: 0)::DirectBase, _) => 0
-     rule [[ getAlign'((obj(... d: link(_)) #as Base::SymBase => Base'), _) ]]
-          <linkings>... Base |-> Base'::SymBase ...</linkings>
-     rule getAlign'(obj(... align: Align::Int)::DirectBase, I::Int) => getNativeAlign(I %Int Align, Align) [owise]
      syntax Int ::= #getNativeAlign(Int, Int, Int) [function]
-     rule getNativeAlign(Address::Int, Max::Int) => #getNativeAlign(Address, Max, 1)
-     rule #getNativeAlign(Address::Int, Max::Int, Accum::Int) => #getNativeAlign(Address, Max, Accum <<Int 1)
+     rule #getNativeAlign(Address::Int, Max::Int, Accum::Int)
+          => #getNativeAlign(Address, Max, Accum <<Int 1)
           requires Address &Int Accum ==Int 0 andBool Accum <Int Max
      rule #getNativeAlign(_, Accum::Int, _) => Accum [owise]