diff --git a/semantics/library/bootstrap.k b/semantics/library/bootstrap.k
index 2f660fd1c..040db4f53 100644
--- 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
index d28edf1f0..bde70a1a6 100644
--- 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 builtin(S:String) => #nativeCall(S, T, .List) ...
- ... Identifier(S) |-> T:Type ...
- requires S in_keys(nativeDefinedBuiltins) [native-call]
- rule 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 nativeCall(S:String, Args:List, VarArgs:List)
+ => #nativeCall(S, T, Args, VarArgs)
...
... Identifier(S) |-> T:Type ...
+
+ rule builtin(S:String) => nativeCall(S, .List, .List)
requires S in_keys(nativeDefinedBuiltins) [native-call]
- rule builtin(S:String, A1:RValue, A2:RValue)
- => #nativeCall(S, T, ListItem(A1) ListItem(A2))
- ...
- ... Identifier(S) |-> T:Type ...
+
+ rule builtin(S:String) => nativeCall(S, .List, .List)
requires S in_keys(nativeDefinedBuiltins) [native-call]
- rule builtin(S:String, A1:RValue, A2:RValue, A3:RValue)
- => #nativeCall(S, T, ListItem(A1) ListItem(A2) ListItem(A3))
- ...
- ... Identifier(S) |-> T:Type ...
+ rule builtin(S:String, A1:RValue)
+ => nativeCall(S, ListItem(A1), .List)
requires S in_keys(nativeDefinedBuiltins) [native-call]
- rule builtin(S:String, A1:RValue, A2:RValue, A3:RValue, A4:RValue)
- => #nativeCall(S, T, ListItem(A1) ListItem(A2) ListItem(A3)
- ListItem(A4))
- ...
- ... Identifier(S) |-> T:Type ...
+ rule builtin(S:String, A1:RValue, A2:RValue)
+ => nativeCall(S, ListItem(A1) ListItem(A2), .List)
requires S in_keys(nativeDefinedBuiltins) [native-call]
- rule 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))
- ...
- ... Identifier(S) |-> T:Type ...
+ 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 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))
- ...
- ... Identifier(S) |-> T:Type ...
+ 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 builtin*(S:String, Args:List) => #nativeCall(S, T, Args) ...
- ... Identifier(S) |-> T:Type ...
+ 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 builtin("free", tv(Loc:SymLoc, T:Type))
- => #nativeCall("free", FunType, ListItem(tv(Loc, T)))
- ...
- ... Identifier("free") |-> FunType:Type ...
+ rule builtin("free", tv(Loc:SymLoc, T:Type))
+ => nativeCall("free", ListItem(tv(Loc, T)), .List)
requires isNativeLoc(Loc)
endmodule