From 530330951980c0cd895f4ca11afe2254b4bcaf57 Mon Sep 17 00:00:00 2001 From: zach Date: Mon, 22 Jan 2024 21:29:02 -0800 Subject: [PATCH] cleanup: Add Current.param/Current.result --- .github/workflows/docs.yml | 2 +- Extism/Bindings.lean | 71 ++++++++++++++++++++++------- Extism/Manifest.lean | 35 +++++++++++---- Extism/Types.lean | 10 +++-- Test.lean | 12 ++--- c/bindings.c | 92 ++++++++++++++++++++++++++------------ 6 files changed, 159 insertions(+), 63 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 49637db..06fc031 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -42,7 +42,7 @@ jobs: - name: Upload artifact uses: actions/upload-pages-artifact@v2 with: - path: '.lake/build/docs' + path: '.lake/build/doc' - name: Deploy to GitHub Pages id: deployment uses: actions/deploy-pages@v2 diff --git a/Extism/Bindings.lean b/Extism/Bindings.lean index 90b1243..c7bc23d 100644 --- a/Extism/Bindings.lean +++ b/Extism/Bindings.lean @@ -7,6 +7,7 @@ import Extism.Types open Extism +/-- Returns the version of the Extism shared object -/ @[extern "l_extism_version"] opaque version : IO String @@ -18,37 +19,75 @@ private def PluginRef : Type := PluginPointed.type instance : Nonempty PluginRef := PluginPointed.property private opaque FunctionPointed : NonemptyType +/-- Host function type -/ def Extism.Function : Type := FunctionPointed.type instance : Nonempty Extism.Function := FunctionPointed.property private opaque CurrentPointed : NonemptyType +/-- The current plugin, from within a host function -/ def Extism.Current : Type := CurrentPointed.type instance : Nonempty Extism.Current := CurrentPointed.property +/-- Set result to i64 from inside a host function -/ @[extern "l_extism_current_set_result_i64"] -opaque Current.setResultI64 : @& Extism.Current -> @& Int64 -> @& Int64 -> IO Unit +opaque Current.setResultI64 : @& Extism.Current -> UInt64 -> UInt64 -> IO Unit +/-- Get i64 param from inside a host function -/ @[extern "l_extism_current_get_param_i64"] -opaque Current.getParamI64 : @& Extism.Current -> @& Int64 -> IO Int64 +opaque Current.getParamI64 : @& Extism.Current -> UInt64 -> IO UInt64 +/-- Set result to i32 from inside a host function -/ @[extern "l_extism_current_set_result_i32"] -opaque Current.setResultI32 : @& Extism.Current -> @& Int64 -> @& Int32 -> IO Unit +opaque Current.setResultI32 : @& Extism.Current -> UInt64 -> UInt32 -> IO Unit +/-- Get i32 param from inside a host function -/ @[extern "l_extism_current_get_param_i32"] -opaque Current.getParamI32 : @& Extism.Current -> @& Int64 -> IO Int32 +opaque Current.getParamI32 : @& Extism.Current -> UInt64 -> IO UInt32 +/-- Set result to f64 from inside a host function -/ @[extern "l_extism_current_set_result_f64"] -opaque Current.setResultF64 : @& Extism.Current -> @& Int64 -> @& Float -> IO Unit +opaque Current.setResultF64 : @& Extism.Current -> UInt64 -> Float -> IO Unit +/-- Get f64 param from inside a host function -/ @[extern "l_extism_current_get_param_f64"] -opaque Current.getParamF64 : @& Extism.Current -> @& Int64 -> IO Float +opaque Current.getParamF64 : @& Extism.Current -> UInt64 -> IO Float +/-- Set result to f32 from inside a host function -/ @[extern "l_extism_current_set_result_f32"] -opaque Current.setResultF32 : @& Extism.Current -> @& Int64 -> @& Float -> IO Unit +opaque Current.setResultF32 : @& Extism.Current -> UInt64 -> Float -> IO Unit +/-- Get f32 param from inside a host function -/ @[extern "l_extism_current_get_param_f32"] -opaque Current.getParamF32 : @& Extism.Current -> @& Int64 -> IO Float +opaque Current.getParamF32 : @& Extism.Current -> UInt64 -> IO Float +@[extern "l_extism_current_alloc"] +private opaque currentAlloc : @& Extism.Current -> UInt64 -> IO UInt64 + +@[extern "l_extism_current_length"] +private opaque currentLength : @& Extism.Current -> UInt64 -> IO UInt64 + +@[extern "l_extism_current_free"] +private opaque currentFree : @& Extism.Current -> UInt64 -> IO Unit + +@[extern "l_extism_current_read"] +private opaque currentRead : @& Extism.Current -> UInt64 -> IO ByteArray + +@[extern "l_extism_current_write"] +private opaque currentWrite : @& Extism.Current -> UInt64 -> @& ByteArray -> IO Unit + +def Current.result [ToBytes a] (current: Extism.Current) (index: USize) (v: a) : IO Unit := do + let data := ToBytes.toBytes v + let len := data.size + let n := <- currentAlloc current len.toUInt64 + currentWrite current n data + Current.setResultI64 current index.toUInt64 n + +def Current.param [FromBytes a] (current: Extism.Current) (index: USize) : IO a := do + let n := <- Current.getParamI64 current index.toUInt64 + let res := <- currentRead current n + let bytes := FromBytes.fromBytes? res + IO.ofExcept bytes + @[extern "l_extism_plugin_new"] private opaque newPluginRef : @& ByteArray -> @& Array Function -> Bool -> IO PluginRef @@ -59,7 +98,7 @@ private opaque pluginRefCall : @& PluginRef -> @& String -> @& ByteArray -> IO B private opaque functionNew : @& String -> @& String -> @& Array UInt8 -> @& Array UInt8 -> (Current -> IO Unit) -> IO Function --- ValType represents the possible types for host function params/results +/-- ValType represents the possible types for host function params/results -/ inductive Extism.ValType where | i32 | i64 @@ -86,7 +125,7 @@ private def newPluginFromFile newPluginRef data functions wasi --- Create a new host function in the specified namespace +/-- Create a new host function in the specified namespace -/ def Extism.Function.newInNamespace (ns : String) (name: String) @@ -98,7 +137,7 @@ def Extism.Function.newInNamespace let results := Array.map ValType.toInt results functionNew ns name params results f --- Create a new host function in the default namespace +/-- Create a new host function in the default namespace -/ def Extism.Function.new (name: String) (params: Array ValType) @@ -107,12 +146,12 @@ def Extism.Function.new := Function.newInNamespace "extism:host/user" name params results f --- Plugin struct +/-- Plugin type -/ structure Extism.Plugin where inner: PluginRef functions: Array Function --- Create a new plugin from a `PluginInput` +/-- Create a new plugin from a `PluginInput` -/ def Extism.Plugin.new [PluginInput a] (data: a) (functions: Array Function) @@ -122,7 +161,7 @@ def Extism.Plugin.new [PluginInput a] let x := <- newPluginRef input functions wasi return (Extism.Plugin.mk x #[]) --- Create a new plugin from a file +/-- Create a new plugin from a file -/ def Extism.Plugin.fromFile (path: System.FilePath) (functions: Array Function) @@ -131,7 +170,7 @@ def Extism.Plugin.fromFile let x := <- newPluginFromFile path functions wasi return (Extism.Plugin.mk x #[]) --- Call a plugin function, performing conversion of input and output +/-- Call a plugin function, performing conversion of input and output -/ def Extism.Plugin.call [ToBytes a] [FromBytes b] (plugin: Extism.Plugin) (funcName: String) @@ -141,7 +180,7 @@ def Extism.Plugin.call [ToBytes a] [FromBytes b] let res := <- pluginRefCall plugin.inner funcName data IO.ofExcept (FromBytes.fromBytes? res) --- Call multiple plugins, piping the output from the last into the next +/-- Call multiple plugins, piping the output from the last into the next -/ def Extism.Plugin.pipe [ToBytes a] [FromBytes b] (plugin: Plugin) (names: List String) diff --git a/Extism/Manifest.lean b/Extism/Manifest.lean index a20a7ee..c6266ac 100644 --- a/Extism/Manifest.lean +++ b/Extism/Manifest.lean @@ -1,4 +1,3 @@ -import Lean.Data.RBMap import Lean.Data.Json.Basic import Lean.Data.Json.FromToJson import Lean.Data.Json.Printer @@ -6,6 +5,7 @@ import Lean.Data.Json.Parser private def Pair := String × Lean.Json +/-- Wasm file -/ structure Extism.WasmFile where path: System.FilePath name: Option String @@ -27,10 +27,7 @@ instance : Lean.ToJson Extism.WasmFile where let m := addIfSome m "hash" x.hash Lean.Json.mkObj m -structure Extism.Memory where - maxPages: Int -deriving Lean.FromJson, Lean.ToJson, Inhabited, Repr - +/-- Wasm URL -/ structure Extism.WasmUrl where url: String headers: Option (List (String × String)) @@ -57,6 +54,7 @@ instance : Lean.ToJson Extism.WasmUrl where let m := addIfSome m "hash" x.hash Lean.Json.mkObj m +/-- Wasm type -/ inductive Extism.Wasm where | wasmFile: Extism.WasmFile -> Extism.Wasm | wasmUrl: Extism.WasmUrl -> Extism.Wasm @@ -75,16 +73,24 @@ instance : Lean.ToJson Extism.Wasm where | Extism.Wasm.wasmFile f => Lean.ToJson.toJson f | Extism.Wasm.wasmUrl u => Lean.ToJson.toJson u +/-- Create a new `Wasm` from a path on disk -/ def Extism.Wasm.file (path: System.FilePath) : Wasm := Extism.Wasm.wasmFile (WasmFile.mk path none none) +/-- Create a new `Wasm` from a URL -/ def Extism.Wasm.url (url: String) : Wasm := Extism.Wasm.wasmUrl (WasmUrl.mk url none none none none) +/-- Memory limits -/ +structure Extism.Memory where + maxPages: Int +deriving Lean.FromJson, Lean.ToJson, Inhabited, Repr + +/-- Extism Manifest, used to link and configure plugins -/ structure Extism.Manifest: Type where wasm: Array Wasm allowedHosts: Option (List String) - allowedPaths: Option (List (String × String)) + allowedPaths: Option (List (System.FilePath × System.FilePath)) memory: Option Memory config: Option (List (String × String)) timeoutMs: Option Int @@ -105,7 +111,7 @@ instance : Lean.ToJson Extism.Manifest where let paths := match x.allowedPaths with | Option.some x => List.map (fun (k, v) => - (k, Lean.toJson v)) x + (k.toString, Lean.toJson v)) x |> Lean.Json.mkObj |> Option.some | Option.none => Option.none @@ -117,37 +123,48 @@ instance : Lean.ToJson Extism.Manifest where Lean.Json.mkObj m +/-- Create a new Manifest from an array of `Wasm` -/ def Extism.Manifest.new (wasm: Array Extism.Wasm) : Extism.Manifest := Extism.Manifest.mk wasm none none none none none -def Extism.Manifest.withMemoryMax (max: Int) (m: Extism.Manifest) : Extism.Manifest := +/-- Set memory max pages -/ +def Extism.Manifest.withMaxPages (max: Int) (m: Extism.Manifest) : Extism.Manifest := {m with memory := some (Extism.Memory.mk max)} +/-- Set configuration key -/ def Extism.Manifest.withConfig (k: String) (v: String) (m: Extism.Manifest) := let c := match m.config with | Option.none => [] | Option.some x => x {m with config := (k, v) :: c} +/-- Set timeout in milliseconds -/ def Extism.Manifest.withTimeout (ms: Int) (m: Extism.Manifest) := {m with timeoutMs := Option.some ms} -def Extism.Manifest.allowPath (k: String) (v: String) (m: Extism.Manifest) := +/-- Allow access to a path on disk -/ +def Extism.Manifest.allowPath (k: System.FilePath) (v: Option System.FilePath) (m: Extism.Manifest) := let c := match m.allowedPaths with | Option.none => [] | Option.some x => x + let v := match v with + | Option.none => k + | Option.some v => v {m with allowedPaths := (k, v) :: c} +/-- Allow host -/ def Extism.Manifest.allowHost (k: String) (m: Extism.Manifest) := let c := match m.allowedHosts with | Option.none => [] | Option.some x => x {m with allowedHosts := k :: c} +/-- Convenience function to convert an `Extism.Manifest` to a JSON string -/ def Extism.Manifest.json (m: Extism.Manifest) : String := let x := Lean.ToJson.toJson m Lean.Json.pretty x +/-- Convenience function to parse an `Extism.Manifest` from a string -/ def Extism.Manifest.parseJson (s: String) : Except String Extism.Manifest := do let x := <- Lean.Json.parse s Lean.FromJson.fromJson? x diff --git a/Extism/Types.lean b/Extism/Types.lean index e8a12cb..a4abc33 100644 --- a/Extism/Types.lean +++ b/Extism/Types.lean @@ -5,12 +5,19 @@ import Lean.Data.Json.Printer import Extism.Manifest +/-- `PluginInput` is implemented by types that can be accepted as the wasm input to + `Plugin.new` --/ class Extism.PluginInput (a: Type) where toPluginInput: a -> ByteArray +/-- `ToBytes` is used to convert input data into bytes -/ class Extism.ToBytes (a: Type) where toBytes: a -> ByteArray +/-- `FromBytes` is used to convert from bytes to output data -/ +class Extism.FromBytes (a: Type) where + fromBytes?: ByteArray -> Except String a + instance : Extism.ToBytes ByteArray where toBytes (x: ByteArray) := x @@ -20,9 +27,6 @@ instance : Extism.ToBytes String where instance [Lean.ToJson a] : Extism.ToBytes a where toBytes x := (Lean.Json.compress (Lean.ToJson.toJson x)).toUTF8 -class Extism.FromBytes (a: Type) where - fromBytes?: ByteArray -> Except String a - instance : Extism.FromBytes ByteArray where fromBytes? (x: ByteArray) := Except.ok x diff --git a/Test.lean b/Test.lean index 6849bf9..2455fc0 100644 --- a/Test.lean +++ b/Test.lean @@ -3,8 +3,9 @@ import Extism open Extism def helloWorld (curr: Current) : IO Unit := do - let a := <- Current.getParamI64 curr 0 - let _ := <- Current.setResultI64 curr 0 a + let s: String := <- Current.param curr 0 + IO.println s!"Input: {s}" + Current.result curr 0 s IO.println "Hello world!!!" IO.println "Hello world!!!" IO.println "Hello world!!!" @@ -16,9 +17,8 @@ def hostFunction: IO Unit := do |> Manifest.withConfig "vowels" "aeiouyAEIOUY" let f := <- Function.new "hello_world" #[ValType.i64] #[ValType.i64] helloWorld let plugin := <- Plugin.new m #[f] True - let input := String.toUTF8 "this is a test" - let res: String := <- plugin.pipe ["count_vowels", "count_vowels"] input - IO.println s!"{res}" + let res: String := <- plugin.pipe ["count_vowels", "count_vowels"] "this is a test" + IO.println s!"Result: {res}" def fromUrl : IO Unit := do let url := "https://github.com/extism/plugins/releases/latest/download/count_vowels.wasm" @@ -28,5 +28,5 @@ def fromUrl : IO Unit := do IO.println s!"{res}" def main : IO Unit := do - fromUrl + -- fromUrl hostFunction diff --git a/c/bindings.c b/c/bindings.c index 2df7b51..4d5d5ff 100644 --- a/c/bindings.c +++ b/c/bindings.c @@ -185,60 +185,96 @@ lean_obj_res l_extism_function_new(b_lean_obj_arg funcNamespace, } lean_obj_res l_extism_current_get_param_i64(b_lean_obj_arg current, - b_lean_obj_arg i) { + uint64_t i) { Current *c = current_plugin_unbox(current); - return lean_io_result_mk_ok(lean_box(c->params[lean_unbox(i)].v.i64)); + assert(extism_current_plugin_memory_length(c->plugin, c->params[i].v.i64)); + return lean_io_result_mk_ok(lean_box_uint64(c->params[i].v.i64)); } -lean_obj_res l_extism_current_set_result_i64(b_lean_obj_arg current, - b_lean_obj_arg i, - b_lean_obj_arg x) { +lean_obj_res l_extism_current_set_result_i64(b_lean_obj_arg current, uint64_t i, + uint64_t x) { Current *c = current_plugin_unbox(current); - c->results[lean_unbox(i)].t = I64; - c->results[lean_unbox(i)].v.i64 = lean_unbox(x); + c->results[i].t = I64; + c->results[i].v.i64 = x; return lean_io_result_mk_ok(lean_box(0)); } lean_obj_res l_extism_current_get_param_i32(b_lean_obj_arg current, - b_lean_obj_arg i) { + uint64_t i) { Current *c = current_plugin_unbox(current); - return lean_io_result_mk_ok(lean_box(c->params[lean_unbox(i)].v.i32)); + return lean_io_result_mk_ok(lean_box_uint32(c->params[i].v.i32)); } -lean_obj_res l_extism_current_set_result_i32(b_lean_obj_arg current, - b_lean_obj_arg i, - b_lean_obj_arg x) { +lean_obj_res l_extism_current_set_result_i32(b_lean_obj_arg current, uint64_t i, + uint32_t x) { Current *c = current_plugin_unbox(current); - c->results[lean_unbox(i)].t = I32; - c->results[lean_unbox(i)].v.i32 = lean_unbox(x); + c->results[i].t = I32; + c->results[i].v.i32 = x; return lean_io_result_mk_ok(lean_box(0)); } lean_obj_res l_extism_current_get_param_f32(b_lean_obj_arg current, - b_lean_obj_arg i) { + uint64_t i) { Current *c = current_plugin_unbox(current); - return lean_io_result_mk_ok(lean_box_float(c->params[lean_unbox(i)].v.f32)); + return lean_io_result_mk_ok(lean_box_float(c->params[i].v.f32)); } -lean_obj_res l_extism_current_set_result_f32(b_lean_obj_arg current, - b_lean_obj_arg i, - b_lean_obj_arg x) { +lean_obj_res l_extism_current_set_result_f32(b_lean_obj_arg current, uint64_t i, + double x) { Current *c = current_plugin_unbox(current); - c->results[lean_unbox(i)].t = F32; - c->results[lean_unbox(i)].v.f32 = lean_unbox_float(x); + c->results[i].t = F32; + c->results[i].v.f32 = x; return lean_io_result_mk_ok(lean_box(0)); } lean_obj_res l_extism_current_get_param_f64(b_lean_obj_arg current, - b_lean_obj_arg i) { + uint64_t i) { Current *c = current_plugin_unbox(current); - return lean_io_result_mk_ok(lean_box_float(c->params[lean_unbox(i)].v.f64)); + return lean_io_result_mk_ok(lean_box_float(c->params[i].v.f64)); } -lean_obj_res l_extism_current_set_result_f64(b_lean_obj_arg current, - b_lean_obj_arg i, - b_lean_obj_arg x) { +lean_obj_res l_extism_current_set_result_f64(b_lean_obj_arg current, uint64_t i, + double x) { Current *c = current_plugin_unbox(current); - c->results[lean_unbox(i)].t = F64; - c->results[lean_unbox(i)].v.f32 = lean_unbox_float(x); + c->results[i].t = F64; + c->results[i].v.f32 = (float)x; + return lean_io_result_mk_ok(lean_box(0)); +} + +lean_obj_res l_extism_current_alloc(b_lean_obj_arg current, uint64_t n) { + Current *c = current_plugin_unbox(current); + ExtismMemoryHandle h = extism_current_plugin_memory_alloc(c->plugin, n); + return lean_io_result_mk_ok(lean_box_uint64(h)); +} + +lean_obj_res l_extism_current_free(b_lean_obj_arg current, uint64_t x) { + Current *c = current_plugin_unbox(current); + extism_current_plugin_memory_free(c->plugin, x); + return lean_io_result_mk_ok(lean_box(0)); +} + +lean_obj_res l_extism_current_length(b_lean_obj_arg current, uint64_t x) { + Current *c = current_plugin_unbox(current); + ExtismSize size = extism_current_plugin_memory_length(c->plugin, x); + return lean_io_result_mk_ok(lean_box_uint64(size)); +} + +lean_obj_res l_extism_current_read(b_lean_obj_arg current, uint64_t x) { + Current *c = current_plugin_unbox(current); + ExtismSize size = extism_current_plugin_memory_length(c->plugin, x); + lean_obj_res res = lean_mk_empty_byte_array(lean_box(size)); + void *dest = lean_sarray_cptr(res); + memcpy(dest, extism_current_plugin_memory(c->plugin) + x, size); + lean_sarray_set_size(res, size); + return lean_io_result_mk_ok(res); +} + +lean_obj_res l_extism_current_write(b_lean_obj_arg current, uint64_t x, + b_lean_obj_arg bytes) { + Current *c = current_plugin_unbox(current); + ExtismSize size = extism_current_plugin_memory_length(c->plugin, x); + size_t arrSize = lean_sarray_size(bytes); + void *dest = lean_sarray_cptr(bytes); + memcpy(extism_current_plugin_memory(c->plugin) + x, dest, + size > arrSize ? arrSize : size); return lean_io_result_mk_ok(lean_box(0)); }