Skip to content

Commit 21896b2

Browse files
brunoborgesCopilot
andcommitted
proof: add FFM proof for call-c-from-java pattern (#129)
Uses strlen from the system C library via the Foreign Function & Memory API to prove the FFM code compiles and runs correctly. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent dc4738e commit 21896b2

File tree

1 file changed

+25
-0
lines changed

1 file changed

+25
-0
lines changed

proof/language/CallCFromJava.java

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
///usr/bin/env jbang "$0" "$@" ; exit $?
2+
//JAVA 25+
3+
//JAVA_OPTIONS --enable-native-access=ALL-UNNAMED
4+
5+
import java.lang.foreign.*;
6+
import java.lang.invoke.MethodHandle;
7+
import java.util.Optional;
8+
9+
/// Proof: call-c-from-java
10+
/// Source: content/language/call-c-from-java.yaml
11+
void main() throws Throwable {
12+
13+
try (Arena arena = Arena.ofConfined()) {
14+
// Use a system library to prove FFM compiles and links
15+
SymbolLookup stdlib = Linker.nativeLinker().defaultLookup();
16+
Optional<MemorySegment> segment = stdlib.find("strlen");
17+
MemorySegment foreignFuncAddr = segment.get();
18+
FunctionDescriptor strlen_sig =
19+
FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.ADDRESS);
20+
MethodHandle strlenMethod =
21+
Linker.nativeLinker().downcallHandle(foreignFuncAddr, strlen_sig);
22+
var ret = (long) strlenMethod.invokeExact(arena.allocateFrom("Bambi"));
23+
System.out.println("Return value " + ret);
24+
}
25+
}

0 commit comments

Comments
 (0)