Merge pull request #240 from chathhorn/varargs2

Fixes to native calls with varargs.
kframework · Feb 24, 2016 · 92d9df0 · 92d9df0
2 parents 796e40d + 7a0d0fc
commit 92d9df0
Show file tree

Hide file tree

Showing 2 changed files with 47 additions and 42 deletions.
diff --git a/semantics/library/bootstrap.k b/semantics/library/bootstrap.k
@@ -11,7 +11,7 @@ module LIBC-BOOTSTRAP-SYNTAX
                     | "builtin*" "(" String "," RValue "," List ")" [klabel(builtin1+)]
                     | "builtin*" "(" String "," RValue "," RValue "," List ")" [klabel(builtin2+)]
                     | "builtin*" "(" String "," RValue "," RValue "," RValue "," List ")" [klabel(builtin3+)]
-                    | "builtin*" "(" String "," List ")"
+                    | "builtin*" "(" String "," List "," List ")"
 endmodule
 
 module LIBC-BOOTSTRAP
@@ -91,13 +91,13 @@ module LIBC-BOOTSTRAP
           requires allRValueInHeatList(VarArgs)
           [structural]
 
-     rule prepareBuiltin(Identifier(F:String), false, Args:HeatList, _)
-          => builtin*(F, hListToList(Args))
+     rule prepareBuiltin(Identifier(F:String), false, Args:HeatList, .HeatList)
+          => builtin*(F, hListToList(Args), .List)
           requires allRValueInHeatList(Args)
                andBool size(hListToList(Args)) >Int 6
           [structural]
      rule prepareBuiltin(Identifier(F:String), true, Args:HeatList, VarArgs:HeatList)
-          => builtin*(F, hListToList(Args) hListToList(VarArgs))
+          => builtin*(F, hListToList(Args), hListToList(VarArgs))
           requires allRValueInHeatList(Args)
                andBool allRValueInHeatList(VarArgs)
                andBool size(hListToList(Args)) >Int 3

diff --git a/semantics/library/native.k b/semantics/library/native.k
@@ -5,56 +5,61 @@ module C-NATIVE-BRIDGE
      imports C-BUILTIN-SYNTAX
      imports C-CONFIGURATION
 
-     syntax K ::= #nativeCall(String, Type, List) [function, hook(C_SEMANTICS.nativeCall), impure, canTakeSteps]
-
-     rule <k> builtin(S:String) => #nativeCall(S, T, .List) ...</k>
-          <types>... Identifier(S) |-> T:Type ...</types>
-          requires S in_keys(nativeDefinedBuiltins) [native-call]
-     rule <k> builtin(S:String, A1:RValue)
-               => #nativeCall(S, T, ListItem(A1))
+     syntax K ::= #nativeCall(String, Type, List, List) [function, hook(C_SEMANTICS.nativeCall), impure, canTakeSteps]
+     syntax KItem ::= nativeCall(String, List, List)
+     rule <k> nativeCall(S:String, Args:List, VarArgs:List)
+               => #nativeCall(S, T, Args, VarArgs)
           ...</k>
           <types>... Identifier(S) |-> T:Type ...</types>
+
+     rule builtin(S:String) => nativeCall(S, .List, .List)
           requires S in_keys(nativeDefinedBuiltins) [native-call]
-     rule <k> builtin(S:String, A1:RValue, A2:RValue)
-               => #nativeCall(S, T, ListItem(A1) ListItem(A2))
-          ...</k>
-          <types>... Identifier(S) |-> T:Type ...</types>
+
+     rule builtin(S:String) => nativeCall(S, .List, .List)
           requires S in_keys(nativeDefinedBuiltins) [native-call]
-     rule <k> builtin(S:String, A1:RValue, A2:RValue, A3:RValue)
-               => #nativeCall(S, T, ListItem(A1) ListItem(A2) ListItem(A3))
-          ...</k>
-          <types>... Identifier(S) |-> T:Type ...</types>
+     rule builtin(S:String, A1:RValue)
+          => nativeCall(S, ListItem(A1), .List)
           requires S in_keys(nativeDefinedBuiltins) [native-call]
-     rule <k> builtin(S:String, A1:RValue, A2:RValue, A3:RValue, A4:RValue)
-               => #nativeCall(S, T, ListItem(A1) ListItem(A2) ListItem(A3)
-                    ListItem(A4))
-          ...</k>
-          <types>... Identifier(S) |-> T:Type ...</types>
+     rule builtin(S:String, A1:RValue, A2:RValue)
+          => nativeCall(S, ListItem(A1) ListItem(A2), .List)
           requires S in_keys(nativeDefinedBuiltins) [native-call]
-     rule <k> builtin(S:String, A1:RValue, A2:RValue, A3:RValue, A4:RValue,
-                    A5:RValue)
-               => #nativeCall(S, T, ListItem(A1) ListItem(A2) ListItem(A3)
-                    ListItem(A4) ListItem(A5))
-          ...</k>
-          <types>... Identifier(S) |-> T:Type ...</types>
+     rule builtin(S:String, A1:RValue, A2:RValue, A3:RValue)
+          => nativeCall(S, ListItem(A1) ListItem(A2) ListItem(A3),
+               .List)
           requires S in_keys(nativeDefinedBuiltins) [native-call]
-     rule <k> builtin(S:String, A1:RValue, A2:RValue, A3:RValue, A4:RValue,
-                    A5:RValue, A6:RValue)
-               => #nativeCall(S, T, ListItem(A1) ListItem(A2) ListItem(A3)
-                    ListItem(A4) ListItem(A5) ListItem(A6))
-          ...</k>
-          <types>... Identifier(S) |-> T:Type ...</types>
+     rule builtin(S:String, A1:RValue, A2:RValue, A3:RValue, A4:RValue)
+          => nativeCall(S, ListItem(A1) ListItem(A2) ListItem(A3)
+               ListItem(A4), .List)
           requires S in_keys(nativeDefinedBuiltins) [native-call]
-     rule <k> builtin*(S:String, Args:List) => #nativeCall(S, T, Args) ...</k>
-          <types>... Identifier(S) |-> T:Type ...</types>
+     rule builtin(S:String, A1:RValue, A2:RValue, A3:RValue, A4:RValue,
+               A5:RValue)
+          => nativeCall(S, ListItem(A1) ListItem(A2) ListItem(A3)
+               ListItem(A4) ListItem(A5), .List)
+          requires S in_keys(nativeDefinedBuiltins) [native-call]
+     rule builtin(S:String, A1:RValue, A2:RValue, A3:RValue, A4:RValue,
+               A5:RValue, A6:RValue)
+          => nativeCall(S, ListItem(A1) ListItem(A2) ListItem(A3)
+               ListItem(A4) ListItem(A5) ListItem(A6), .List)
+          requires S in_keys(nativeDefinedBuiltins) [native-call]
+
+     rule builtin*(S:String, A1:RValue, VarArgs:List)
+          => nativeCall(S, ListItem(A1), VarArgs)
+          requires S in_keys(nativeDefinedBuiltins) [native-call]
+     rule builtin*(S:String, A1:RValue, A2:RValue, VarArgs:List)
+          => nativeCall(S, ListItem(A1) ListItem(A2), VarArgs)
+          requires S in_keys(nativeDefinedBuiltins) [native-call]
+     rule builtin*(S:String, A1:RValue, A2:RValue, A3:RValue, VarArgs:List)
+          => nativeCall(S, ListItem(A1) ListItem(A2) ListItem(A3), VarArgs)
+          requires S in_keys(nativeDefinedBuiltins) [native-call]
+
+     rule builtin*(S:String, Args:List, VarArgs:List)
+          => nativeCall(S, Args, VarArgs)
           requires S in_keys(nativeDefinedBuiltins) [native-call]
 
      // Memory allocated by the native heap needs to be freed by a call to
      // native free.
-     rule <k> builtin("free", tv(Loc:SymLoc, T:Type))
-               => #nativeCall("free", FunType, ListItem(tv(Loc, T)))
-          ...</k>
-          <types>... Identifier("free") |-> FunType:Type ...</types>
+     rule builtin("free", tv(Loc:SymLoc, T:Type))
+          => nativeCall("free", ListItem(tv(Loc, T)), .List)
           requires isNativeLoc(Loc)
 
 endmodule