From 834a7bb00000294e0a3dfe3b52bdc78721b65ade Mon Sep 17 00:00:00 2001 From: N1ark Date: Wed, 22 Apr 2026 15:52:15 +0100 Subject: [PATCH 01/30] Bump Charon and Obol --- .github/workflows/build.yml | 8 ++++---- .github/workflows/test-packages.yml | 4 ++-- README.md | 8 ++++---- scripts/versions.json | 4 ++-- soteria-rust.opam | 8 ++++---- soteria-rust.opam.template | 8 ++++---- 6 files changed, 20 insertions(+), 20 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 7caa7c82e..3ea9921bb 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -8,12 +8,12 @@ env: OCAML_VERSION: 5.4.0 # [versionsync: OBOL_REPO=soteria-tools/obol] OBOL_REPO: soteria-tools/obol - # [versionsync: OBOL_COMMIT_HASH=3d2266de79f1e2e601b7a82f6803b649cbe6953c] - OBOL_COMMIT_HASH: 3d2266de79f1e2e601b7a82f6803b649cbe6953c + # [versionsync: OBOL_COMMIT_HASH=ddea5ca5da4c07301584f47f05ea8615fc365b41] + OBOL_COMMIT_HASH: ddea5ca5da4c07301584f47f05ea8615fc365b41 # [versionsync: CHARON_REPO=soteria-tools/charon] CHARON_REPO: soteria-tools/charon - # [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb] - CHARON_COMMIT_HASH: fbd54169205bf97e3c42cbfef95ca5807d697bfb + # [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba] + CHARON_COMMIT_HASH: fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba jobs: build: diff --git a/.github/workflows/test-packages.yml b/.github/workflows/test-packages.yml index 0e11c4f35..68ed6066a 100644 --- a/.github/workflows/test-packages.yml +++ b/.github/workflows/test-packages.yml @@ -6,8 +6,8 @@ on: env: # [versionsync: OBOL_REPO=soteria-tools/obol] OBOL_REPO: soteria-tools/obol - # [versionsync: OBOL_COMMIT_HASH=3d2266de79f1e2e601b7a82f6803b649cbe6953c] - OBOL_COMMIT_HASH: 3d2266de79f1e2e601b7a82f6803b649cbe6953c + # [versionsync: OBOL_COMMIT_HASH=ddea5ca5da4c07301584f47f05ea8615fc365b41] + OBOL_COMMIT_HASH: ddea5ca5da4c07301584f47f05ea8615fc365b41 jobs: test-soteria-c-package: diff --git a/README.md b/README.md index 6d3367b61..a8369399b 100644 --- a/README.md +++ b/README.md @@ -137,12 +137,12 @@ We support two frontends: [Obol](https://github.com/soteria-tools/obol) and [Cha **Manual installation:** 1. **Clone Obol at the correct commit:** - + ```sh cd .. git clone https://github.com/soteria-tools/obol.git cd obol - git checkout 3d2266de79f1e2e601b7a82f6803b649cbe6953c + git checkout ddea5ca5da4c07301584f47f05ea8615fc365b41 ``` > **Note:** The required commit hash can always be found in [`scripts/versions.json`](scripts/versions.json) under `OBOL_COMMIT_HASH`. @@ -168,12 +168,12 @@ We support two frontends: [Obol](https://github.com/soteria-tools/obol) and [Cha **Manual installation:** 1. **Clone Charon at the correct commit:** - + ```sh cd .. git clone https://github.com/soteria-tools/charon.git cd charon - git checkout fbd54169205bf97e3c42cbfef95ca5807d697bfb + git checkout fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba ``` > **Note:** The required commit hash can always be found in [`scripts/versions.json`](scripts/versions.json) under `CHARON_COMMIT_HASH`. diff --git a/scripts/versions.json b/scripts/versions.json index 0820a7f6d..a36e9d540 100644 --- a/scripts/versions.json +++ b/scripts/versions.json @@ -1,9 +1,9 @@ { "_comment": "Central version configuration for Soteria. Run `scripts/versionsync.py check` to verify versions are in sync, or `scripts/versionsync.py update` to update versions everywhere.", "CHARON_REPO": "soteria-tools/charon", - "CHARON_COMMIT_HASH": "fbd54169205bf97e3c42cbfef95ca5807d697bfb", + "CHARON_COMMIT_HASH": "fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba", "OBOL_REPO": "soteria-tools/obol", - "OBOL_COMMIT_HASH": "3d2266de79f1e2e601b7a82f6803b649cbe6953c", + "OBOL_COMMIT_HASH": "ddea5ca5da4c07301584f47f05ea8615fc365b41", "OCAMLFORMAT_VERSION": "0.28.1", "OCAML_VERSION": "5.4.0" } diff --git a/soteria-rust.opam b/soteria-rust.opam index d2301486f..186a9021a 100644 --- a/soteria-rust.opam +++ b/soteria-rust.opam @@ -54,8 +54,8 @@ build: [ dev-repo: "git+https://github.com/soteria-tools/soteria.git" # Versions managed by scripts/versionsync.py - edit scripts/versions.json to change pin-depends: [ - # [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb] - ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"] - # [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb] - ["charon.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"] + # [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba] + ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"] + # [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba] + ["charon.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"] ] diff --git a/soteria-rust.opam.template b/soteria-rust.opam.template index 81464400d..6613d5d1a 100644 --- a/soteria-rust.opam.template +++ b/soteria-rust.opam.template @@ -1,7 +1,7 @@ # Versions managed by scripts/versionsync.py - edit scripts/versions.json to change pin-depends: [ - # [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb] - ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"] - # [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb] - ["charon.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"] + # [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba] + ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"] + # [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba] + ["charon.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"] ] From 3725362f6900d87c5fbb149a50daf92ec87da7fa Mon Sep 17 00:00:00 2001 From: N1ark Date: Wed, 22 Apr 2026 15:54:50 +0100 Subject: [PATCH 02/30] Separate externs/intrinsics handling + fix poly --- soteria-rust/lib/builtins/eval.ml | 148 ++++++++++++------------- soteria-rust/lib/builtins/std.ml | 2 +- soteria-rust/lib/interp.ml | 87 +++++++++------ soteria-rust/lib/rustsymex.ml | 29 +++-- soteria-rust/lib/state/rust_state_m.ml | 13 ++- soteria-rust/test/cram/poly.t/run.t | 10 +- soteria-rust/test/cram/simple.t/run.t | 4 +- 7 files changed, 160 insertions(+), 133 deletions(-) diff --git a/soteria-rust/lib/builtins/eval.ml b/soteria-rust/lib/builtins/eval.ml index f97dd8213..eeecde4f1 100644 --- a/soteria-rust/lib/builtins/eval.ml +++ b/soteria-rust/lib/builtins/eval.ml @@ -1,11 +1,12 @@ open Charon module NameMatcherMap = Charon.NameMatcher.NameMatcherMap +module SMap = Map.Make (String) let match_config = NameMatcher.{ map_vars_to_vars = false; match_with_trait_decl_refs = false } (* Functions we stub to avoid problems in the interpreter *) -type fixme_fn = PanicCleanup | CatchUnwindCleanup +type fixme_fn = CatchUnwindCleanup | PromiseAlignment | DropInPlace (* Functions we could not stub, but we do for performance *) type optim_fn = @@ -21,7 +22,10 @@ type optim_fn = type soteria_fn = Assert | Assume | NondetBytes | Panic (* Miri builtin functions *) -type miri_fn = Alloc | AllocId | Dealloc | PromiseAlignement | Nop +type miri_fn = Alloc | AllocId | Dealloc | Nop + +(* Functions related to panics *) +type panic_fn = PanicCleanup (* Functions related to the allocator, see https://doc.rust-lang.org/src/alloc/alloc.rs.html#11-36 *) @@ -34,13 +38,33 @@ type alloc_fn = type system_fn = HashmapRandomKeys | TlvAtexit type fn = - | Alloc of alloc_fn | Fixme of fixme_fn - | Miri of miri_fn | Optim of optim_fn | Soteria of soteria_fn | System of system_fn - | DropInPlace + +type extern_fn = Alloc of alloc_fn | Miri of miri_fn | Panic of panic_fn + +let extern_functions = + [ + (* Allocator *) + ("__rust_alloc", Alloc (Alloc { zeroed = false })); + ("__rust_alloc_zeroed", Alloc (Alloc { zeroed = true })); + ("__rust_dealloc", Alloc Dealloc); + ("__rust_no_alloc_shim_is_unstable_v2", Alloc NoAllocShimIsUnstable); + ("__rust_realloc", Alloc Realloc); + (* Miri builtins *) + ("miri_get_alloc_id", Miri AllocId); + ("miri_pointer_name", Miri Nop); + ("miri_print_borrow_state", Miri Nop); + ("miri_run_provenance_gc", Miri Nop); + ("miri_write_to_stdout", Miri Nop); + ("miri_alloc", Miri Alloc); + ("miri_dealloc", Miri Dealloc); + (* Panics *) + ("__rust_panic_cleanup", Panic PanicCleanup); + ] + |> SMap.of_list let std_fun_pair_list = [ @@ -54,33 +78,8 @@ let std_fun_pair_list = ("kani::assume", Soteria Assume); ("kani::panic", Soteria Panic); (* Miri builtins *) - ("std::intrinsics::miri_promise_symbolic_alignment", Miri PromiseAlignement); - (* TODO: once https://github.com/AeneasVerif/charon/pull/1088 is merged, - this should be handled through extern bodies. *) - ("miristd::miri_get_alloc_id", Miri AllocId); - ("miristd::miri_pointer_name", Miri Nop); - ("miristd::miri_print_borrow_state", Miri Nop); - ("miristd::miri_run_provenance_gc", Miri Nop); - ("miristd::miri_write_to_stdout", Miri Nop); - ("miristd::miri_alloc", Miri Alloc); - ("miristd::miri_dealloc", Miri Dealloc); - (* Obol is quite bad at parsing names so this is how they're called - there... *) - ("utils::miri_extern::miri_get_alloc_id", Miri AllocId); - ("utils::miri_extern::miri_pointer_name", Miri Nop); - ("utils::miri_extern::miri_print_borrow_state", Miri Nop); - ("utils::miri_extern::miri_run_provenance_gc", Miri Nop); - ("utils::miri_extern::miri_write_to_stdout", Miri Nop); - ("utils::miri_extern::miri_alloc", Miri Alloc); - ("utils::miri_extern::miri_dealloc", Miri Dealloc); - (* Allocator *) - (* TODO: once https://github.com/AeneasVerif/charon/pull/1088 is merged, - this should be handled through extern bodies. *) - ("__rust_alloc", Alloc (Alloc { zeroed = false })); - ("__rust_alloc_zeroed", Alloc (Alloc { zeroed = true })); - ("__rust_dealloc", Alloc Dealloc); - ("__rust_no_alloc_shim_is_unstable_v2", Alloc NoAllocShimIsUnstable); - ("__rust_realloc", Alloc Realloc); + (* HACK: this should be handled with intrinsics. *) + ("std::intrinsics::miri_promise_symbolic_alignment", Fixme PromiseAlignment); (* System stuff *) (* TODO: the name of the function is *just* _tlv_atexit, because it's an external function, but we don't yet have a way to detect that. This @@ -89,10 +88,8 @@ let std_fun_pair_list = ( "std::sys::thread_local::guard::apple::enable::_tlv_atexit", System TlvAtexit ); ("std::sys::random::hashmap_random_keys", System HashmapRandomKeys); - (* Panic Builtins *) - ("__rust_panic_cleanup", Fixme PanicCleanup); (* Dropping, in particular for the generic case, does nothing. *) - ("core::ptr::drop_in_place", DropInPlace); + ("core::ptr::drop_in_place", Fixme DropInPlace); (* Core *) ("std::alloc::Global::alloc_impl", Optim AllocImpl); (* FIXME(OCaml): all float operations could be removed, but we lack bit @@ -174,11 +171,6 @@ module M (StateM : State.StateM.S) = struct | Soteria Assume -> Soteria_lib.assume | Soteria NondetBytes -> Soteria_lib.nondet_bytes fn_sig | Soteria Panic -> Soteria_lib.panic ?msg:None - | Miri Alloc -> Miri.alloc - | Miri AllocId -> Miri.alloc_id - | Miri Dealloc -> Miri.dealloc - | Miri PromiseAlignement -> Miri.promise_alignement - | Miri Nop -> Std.nop | Optim AllocImpl -> Std.alloc_impl | Optim Panic -> Soteria_lib.panic ~msg:(Fmt.to_to_string Crate.pp_name fn_name) @@ -187,45 +179,47 @@ module M (StateM : State.StateM.S) = struct | Optim (FloatIsSign { positive }) -> Std.float_is_sign positive | Optim Nop -> Std.nop | Optim PrintToBufferIfCaptureUsed -> Std.to_buffer_if_capture_used + | Fixme CatchUnwindCleanup -> Std.fixme_catch_unwind_cleanup + | Fixme DropInPlace -> Std.nop + | Fixme PromiseAlignment -> Miri.promise_alignement + | System HashmapRandomKeys -> System.hashmap_random_keys + | System TlvAtexit -> System.tlv_atexit fun_exec + + let extern_fn_to_stub = function | Alloc (Alloc { zeroed }) -> Alloc.alloc ~zeroed | Alloc Dealloc -> Alloc.dealloc | Alloc NoAllocShimIsUnstable -> Alloc.no_alloc_shim_is_unstable | Alloc Realloc -> Alloc.realloc - | Fixme PanicCleanup -> Std.fixme_panic_cleanup - | Fixme CatchUnwindCleanup -> Std.fixme_catch_unwind_cleanup - | System HashmapRandomKeys -> System.hashmap_random_keys - | System TlvAtexit -> System.tlv_atexit fun_exec - | DropInPlace -> Std.nop - - let std_fun_eval (f : UllbcAst.fun_decl) generics fun_exec = - (* Rust allows defining functions and marking them as intrinsics within a - module, and the compiler will treat them as the intrinsic of the same - name. This means their path doesn't match the one we expect for the - patterns; so instead of matching on a path, we only consider intrinsics - from their name. *) - if Common.Charon_util.decl_has_attr f "rustc_intrinsic" then - let name, generics = - match List.rev f.item_meta.name with - | PeIdent (name, _) :: _ -> (name, generics) - | PeInstantiated mono :: PeIdent (name, _) :: _ -> - (name, mono.binder_value) - | _ -> failwith "Unexpected intrinsic shape" - in - Intrinsics.eval_fun name fun_exec generics - else - let name = - match List.last f.item_meta.name with - | PeIdent (name, _) as ident - when String.starts_with ~prefix:"__rust" name -> - [ ident ] - | _ -> f.item_meta.name - in - let ctx = Crate.as_namematcher_ctx () in - let stub = NameMatcherMap.find_opt ctx match_config name std_fun_map in - match stub with - | Some stub -> - fun args -> - StateM.Poly.push_generics ~params:f.generics ~args:generics - @@ fn_to_stub f.signature name fun_exec stub args - | None -> fun_exec (Real { id = f.def_id; generics }) + | Miri Alloc -> Miri.alloc + | Miri AllocId -> Miri.alloc_id + | Miri Dealloc -> Miri.dealloc + | Miri Nop -> Std.nop + | Panic PanicCleanup -> Std.panic_cleanup + + let eval_stub (f : UllbcAst.fun_decl) fun_exec = + let name = f.item_meta.name in + let ctx = Crate.as_namematcher_ctx () in + let stub = NameMatcherMap.find_opt ctx match_config name std_fun_map in + match stub with + | Some stub -> + let stub args = fn_to_stub f.signature name fun_exec stub args in + Some stub + | None -> None + + let eval_intrinsic (f : UllbcAst.fun_decl) name generics fun_exec = + (* In the case of monomorphised code, the generics will be empty but present + in the name; we need to get them there. *) + let generics = + match List.last_opt f.item_meta.name with + | Some (PeInstantiated mono) -> mono.binder_value + | _ -> generics + in + Intrinsics.eval_fun name fun_exec generics + + let eval_extern name = + match SMap.find_opt name extern_functions with + | Some extern_fn -> extern_fn_to_stub extern_fn + | None -> + fun _args -> + Fmt.kstr StateM.not_impl "Extern function %s is not handled" name end diff --git a/soteria-rust/lib/builtins/std.ml b/soteria-rust/lib/builtins/std.ml index 7fd747d98..7bf3ef431 100644 --- a/soteria-rust/lib/builtins/std.ml +++ b/soteria-rust/lib/builtins/std.ml @@ -93,7 +93,7 @@ module M (StateM : State.StateM.S) = struct in mk_res ptr size - let fixme_panic_cleanup _ = + let panic_cleanup _ = (* TODO: whas is __rust_panic_cleanup meant to do and return? *) ok (Ptr (Sptr.null_ptr (), VTable (Sptr.null_ptr ()))) diff --git a/soteria-rust/lib/interp.ml b/soteria-rust/lib/interp.ml index 103ba8e5c..05777bb75 100644 --- a/soteria-rust/lib/interp.ml +++ b/soteria-rust/lib/interp.ml @@ -465,14 +465,12 @@ module Make (StateImpl : State.S) = struct let fundef = Crate.get_fun fn.id in let+ inputs = Poly.push_generics ~params:fundef.generics ~args:fn.generics - @@ Poly.subst_tys fundef.signature.inputs + @@ fun _ -> Poly.subst_tys fundef.signature.inputs in [%l.info "Resolved function call to %a" Crate.pp_name fundef.item_meta.name]; - let fun_maybe_stubbed = - Std_funs.std_fun_eval fundef fn.generics exec_fun - in - (fun_maybe_stubbed, inputs) + let exec = exec_real_fun fundef fn.generics in + (exec, inputs) in function (* Handle builtins separately *) @@ -506,7 +504,7 @@ module Make (StateImpl : State.S) = struct let fundef = Crate.get_fun decl.init in [%l.info "Resolved global init call to %a" Crate.pp_name fundef.item_meta.name]; - let global_fn = Std_funs.std_fun_eval fundef glob.generics exec_fun in + let global_fn = exec_real_fun fundef glob.generics in (* First we allocate the global and store it in the State *) let* ptr = State.alloc_ty ~kind:(Static glob) ~span:decl.item_meta.span.data @@ -1076,15 +1074,15 @@ module Make (StateImpl : State.S) = struct contains polymorphic types. *) let drop_fn : Fun_kind.t option = match trait_ref.kind with - | TraitImpl impl_ref -> + | TraitImpl impl_ref -> ( let impl = Crate.get_trait_impl impl_ref in (* The Drop trait will only have the drop function *) let _, drop_ref = List.hd impl.methods in let drop = Crate.get_fun drop_ref.binder_value.id in - if Option.is_some drop.body then - (* TODO: i don't think we should read [binder_value] here *) - Some (Real drop_ref.binder_value) - else None + match drop.body with + (* TODO: i don't think we should read [binder_value] here *) + | Body _ -> Some (Real drop_ref.binder_value) + | _ -> None) | _ -> None in match drop_fn with @@ -1121,30 +1119,44 @@ module Make (StateImpl : State.S) = struct and exec_real_fun (fundef : UllbcAst.fun_decl) (generics : Types.generic_args) args = let name = fundef.item_meta.name in - let* body = - match fundef.body with - | None -> Fmt.kstr not_impl "Function %a is opaque" Crate.pp_name name - | Some body -> ok body - in - Soteria.Stats.As_ctx.incr StatKeys.function_calls; - let@@ () = Poly.push_generics ~params:fundef.generics ~args:generics in - let@@ () = with_env ~env:Store.empty in - let@ () = with_loc ~loc:fundef.item_meta.span.data in - let* protected = alloc_stack body.locals args in - let starting_block = List.hd body.body in - let exec_block = exec_block ~body starting_block in - unwind_with exec_block - ~f:(fun value -> - let protected_address = - match (fundef.signature.output, value) with - | (TRef (RStatic, _, _) | TRawPtr _), Ptr (addr, _) -> Some addr - | _ -> None - in - let+ () = dealloc_stack ?protected_address protected in - value) - ~fe:(fun err -> - let* () = dealloc_stack protected in - error_raw err) + let@ generics = Poly.push_generics ~params:fundef.generics ~args:generics in + let () = Soteria.Stats.As_ctx.incr StatKeys.function_calls in + match fundef.body with + | Intrinsic { name; arg_names = _ } -> + Std_funs.eval_intrinsic fundef name generics exec_fun args + | Extern name -> Std_funs.eval_extern name args + | Body body -> ( + match Std_funs.eval_stub fundef exec_fun with + | Some stub -> stub args + | None -> + let@ () = with_loc ~loc:fundef.item_meta.span.data in + let@@ () = with_env ~env:Store.empty in + let* protected = alloc_stack body.locals args in + let starting_block = List.hd body.body in + let exec_block = exec_block ~body starting_block in + unwind_with exec_block + ~f:(fun value -> + (* HACK: this is.. really bad. We need proper deallocation of + locals, and figure out why we need this in the first + place. *) + let protected_address = + match (fundef.signature.output, value) with + | (TRef (RStatic, _, _) | TRawPtr _), Ptr (addr, _) -> + Some addr + | _ -> None + in + let+ () = dealloc_stack ?protected_address protected in + value) + ~fe:(fun err -> + let* () = dealloc_stack protected in + error_raw err)) + | Opaque | TraitMethodWithoutDefault | Missing | Error _ -> ( + match Std_funs.eval_stub fundef exec_fun with + | Some stub -> stub args + | None -> + Fmt.kstr not_impl "Can't execute function %a: %a" Crate.pp_name name + (GAst.pp_body Fmt.nop) fundef.body) + | TargetDispatch _ -> failwith "Target dispatch not supported" and exec_fun (fn : Fun_kind.t) = match fn with @@ -1156,6 +1168,11 @@ module Make (StateImpl : State.S) = struct (* re-define this for the export, nowhere else: *) let exec_fun ~args ~state (fundef : UllbcAst.fun_decl) = let@ () = run ~env:() ~state in + (* HACK: we protect this function with a bind to make sure no effects are + raised before the handlers are correctly setup. For a way of fixing this, + see + https://github.com/soteria-tools/soteria/commit/23bdf7aecf6e80752f98129865ce6d5892d41a2f *) + let* () = ok () in let@@ () = with_extra_call_trace ~loc:fundef.item_meta.span.data ~msg:"Entry point" in diff --git a/soteria-rust/lib/rustsymex.ml b/soteria-rust/lib/rustsymex.ml index fbaed868f..b37482f17 100644 --- a/soteria-rust/lib/rustsymex.ml +++ b/soteria-rust/lib/rustsymex.ml @@ -90,27 +90,38 @@ module Poly = struct open Substitute open Syntax - let push_generics ~params ~args (x : 'a t) : 'a t = + (** Executes the given computation with an updated polymorphic environment, + with some generic arguments for some parameters; the arguments must match + the parameters. The callback receives the substituted generic arguments + given the current substitution. *) + let push_generics ~params ~args (x : Types.generic_args -> 'a t) : 'a t = + fun st -> (* We only push generics in polymorphic mode, as otherwise we may get some wrong generics in monomorphic code we want to ignore. *) - if (Config.get ()).polymorphic then ( - let* ({ subst; _ } as st) = get_state () in - let args' = generic_args_substitute subst args in - [%l.debug "Pushing generics %a" Crate.pp_generic_args args']; + let open MonoSymex.Syntax in + if not (Config.get ()).polymorphic then x args st + else + let prev_subst = st.subst in + let args' = generic_args_substitute prev_subst args in + [%l.debug + "Pushing generics@.\t- Para: %a@.\t- Args: %a" Crate.pp_generic_params + params Crate.pp_generic_args args']; let subst = subst_at_binder_zero (make_sb_subst_from_generics params args' Self) in - with_state ~state:{ st with subst } x) - else x + let+ res, st = x args' { st with subst } in + (res, { st with subst = prev_subst }) let subst f x = - let+ { subst; _ } = get_state () in - f subst x + let* { subst; _ } = get_state () in + try return (f subst x) + with Not_found -> give_up "Substitution failed -- wrong poly environment" let subst_ty = subst ty_substitute let subst_tys = subst (fun subst -> List.map (ty_substitute subst)) let subst_tref = subst trait_ref_substitute let subst_constant_expr = subst st_substitute_visitor#visit_constant_expr + let subst_generic_args = subst generic_args_substitute let fill_params params = subst generic_args_substitute @@ bound_identity_args params diff --git a/soteria-rust/lib/state/rust_state_m.ml b/soteria-rust/lib/state/rust_state_m.ml index 546eef0f2..276aead2f 100644 --- a/soteria-rust/lib/state/rust_state_m.ml +++ b/soteria-rust/lib/state/rust_state_m.ml @@ -103,13 +103,14 @@ module type S = sig val push_generics : params:Types.generic_params -> args:Types.generic_args -> - ('a, 'env) t -> + (Types.generic_args -> ('a, 'env) t) -> ('a, 'env) t val fill_params : Types.generic_params -> (Types.generic_args, 'a) monad val subst_ty : Types.ty -> (Types.ty, 'env) t val subst_tys : Types.ty list -> (Types.ty list, 'env) t val subst_tref : Types.trait_ref -> (Types.trait_ref, 'env) t + val subst_generic_args : Types.generic_args -> (Types.generic_args, 'env) t val subst_constant_expr : Types.constant_expr -> (Types.constant_expr, 'env) t @@ -409,13 +410,19 @@ module Make (State : State_intf.S) : | Missing f -> Missing f module Poly = struct - let[@inline] push_generics ~params ~args (x : ('a, 'env) t) : ('a, 'env) t = - fun env state -> Poly.push_generics ~params ~args (x env state) + let[@inline] push_generics ~params ~args + (x : Types.generic_args -> ('a, 'env) t) : ('a, 'env) t = + fun env state -> + Poly.push_generics ~params ~args (fun args -> x args env state) let[@inline] fill_params params = lift_symex (Poly.fill_params params) let[@inline] subst_ty ty = lift_symex (Poly.subst_ty ty) let[@inline] subst_tys tys = lift_symex (Poly.subst_tys tys) let[@inline] subst_tref tref = lift_symex (Poly.subst_tref tref) + + let[@inline] subst_generic_args generic_args = + lift_symex (Poly.subst_generic_args generic_args) + let[@inline] subst_constant_expr c = lift_symex (Poly.subst_constant_expr c) end diff --git a/soteria-rust/test/cram/poly.t/run.t b/soteria-rust/test/cram/poly.t/run.t index ff8af4d87..823384c94 100644 --- a/soteria-rust/test/cram/poly.t/run.t +++ b/soteria-rust/test/cram/poly.t/run.t @@ -42,16 +42,14 @@ Try creating a generic vec │ │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Triggering operation │ ╰───────────────────────────────────────' 1: Entry point 7 │ } - PC 1: (0x0000000000000000 == V|1|) /\ (V|2| <=u 0x00000000000003ff) /\ - (0x0000000000000000 == V|1|) + PC 1: (0x0000000000000000 == V|1|) /\ (0x0000000000000000 == V|1|) => Running vec::with_capacity... note: vec::with_capacity: done in