diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index 4152906bd..1b125f359 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/charon-ml/src/CharonVersion.ml @@ -1,3 +1,3 @@ (* This is an automatically generated file, generated from `charon/Cargo.toml`. *) (* To re-generate this file, rune `make` in the root directory *) -let supported_charon_version = "0.1.150" +let supported_charon_version = "0.1.151" diff --git a/charon-ml/src/PrintGAst.ml b/charon-ml/src/PrintGAst.ml index 41edf8d89..647a09770 100644 --- a/charon-ml/src/PrintGAst.ml +++ b/charon-ml/src/PrintGAst.ml @@ -18,7 +18,7 @@ let item_id_to_string (id : item_id) : string = let fn_operand_to_string (env : 'a fmt_env) (op : fn_operand) : string = match op with | FnOpRegular func -> fn_ptr_to_string env func - | FnOpMove p -> "move " ^ place_to_string env p + | FnOpDynamic op -> "(" ^ operand_to_string env op ^ ")" let call_to_string (env : 'a fmt_env) (indent : string) (call : call) : string = let func = fn_operand_to_string env call.func in diff --git a/charon-ml/src/generated/Generated_GAst.ml b/charon-ml/src/generated/Generated_GAst.ml index 42bb1fe7b..3e435bc19 100644 --- a/charon-ml/src/generated/Generated_GAst.ml +++ b/charon-ml/src/generated/Generated_GAst.ml @@ -93,8 +93,7 @@ and error = { span : span; msg : string } and fn_operand = | FnOpRegular of fn_ptr (** Regular case: call to a top-level function, trait method, etc. *) - | FnOpMove of place - (** Use of a function pointer stored in a local variable *) + | FnOpDynamic of operand (** Use of a function pointer. *) (** A function signature. *) and fun_sig = { diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index 82ab3cb4e..46c643237 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -821,9 +821,9 @@ and fn_operand_of_json (ctx : of_json_ctx) (js : json) : | `Assoc [ ("Regular", regular) ] -> let* regular = fn_ptr_of_json ctx regular in Ok (FnOpRegular regular) - | `Assoc [ ("Move", move) ] -> - let* move = place_of_json ctx move in - Ok (FnOpMove move) + | `Assoc [ ("Dynamic", dynamic) ] -> + let* dynamic = operand_of_json ctx dynamic in + Ok (FnOpDynamic dynamic) | _ -> Error "") and fn_ptr_of_json (ctx : of_json_ctx) (js : json) : (fn_ptr, string) result = diff --git a/charon-ml/tests/Test_NameMatcher.ml b/charon-ml/tests/Test_NameMatcher.ml index ca6f9c2c9..f2e34493d 100644 --- a/charon-ml/tests/Test_NameMatcher.ml +++ b/charon-ml/tests/Test_NameMatcher.ml @@ -147,7 +147,7 @@ module PatternTest = struct (fun call -> match call.func with | FnOpRegular fn_ptr -> fn_ptr - | FnOpMove _ -> + | FnOpDynamic _ -> failwith "Indirect calls are unsupported un name matcher tests") calls diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 51a197522..df883e085 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -219,7 +219,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.150" +version = "0.1.151" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 5ee04e60b..99cb67242 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.150" +version = "0.1.151" authors = [ "Son Ho ", "Guillaume Boisseau ", diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index 8bb2616ac..2c09bf44c 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -386,8 +386,8 @@ pub struct TraitAssocTyImpl { pub enum FnOperand { /// Regular case: call to a top-level function, trait method, etc. Regular(FnPtr), - /// Use of a function pointer stored in a local variable - Move(Place), + /// Use of a function pointer. + Dynamic(Operand), } #[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 2ff649a64..8c324c023 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -1093,14 +1093,7 @@ impl BodyTransCtx<'_, '_, '_> { hax::FunOperand::Dynamic(op) => { // Call to a local function pointer let op = self.translate_operand(span, op)?; - let (Operand::Move(p) | Operand::Copy(p)) = op else { - raise_error!( - self, - span, - "unsupported dynamic call to constant expression" - ) - }; - FnOperand::Move(p) + FnOperand::Dynamic(op) } }; let args = self.translate_arguments(span, args)?; diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 20cd3ad4c..d7b3c2866 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -428,7 +428,7 @@ impl FmtWithCtx for FnOperand { fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { FnOperand::Regular(func) => write!(f, "{}", func.with_ctx(ctx)), - FnOperand::Move(p) => write!(f, "(move {})", p.with_ctx(ctx)), + FnOperand::Dynamic(op) => write!(f, "({})", op.with_ctx(ctx)), } } } diff --git a/charon/src/transform/normalize/transform_dyn_trait_calls.rs b/charon/src/transform/normalize/transform_dyn_trait_calls.rs index 356ee996a..2e9b95ccd 100644 --- a/charon/src/transform/normalize/transform_dyn_trait_calls.rs +++ b/charon/src/transform/normalize/transform_dyn_trait_calls.rs @@ -116,7 +116,7 @@ fn transform_dyn_trait_call( ); // Transform the original call to use the function pointer - call.func = FnOperand::Move(method_field_place); + call.func = FnOperand::Dynamic(Operand::Copy(method_field_place)); Ok(()) } diff --git a/charon/src/transform/simplify_output/index_to_function_calls.rs b/charon/src/transform/simplify_output/index_to_function_calls.rs index dd956a56f..6d70a8a96 100644 --- a/charon/src/transform/simplify_output/index_to_function_calls.rs +++ b/charon/src/transform/simplify_output/index_to_function_calls.rs @@ -156,7 +156,7 @@ impl VisitBodyMut for IndexVisitor<'_, '_> { fn visit_fn_operand(&mut self, x: &mut FnOperand) -> ControlFlow { match x { FnOperand::Regular(_) => self.visit_inner(x), - FnOperand::Move(_) => self.visit_inner_with_mutability(x, true), + FnOperand::Dynamic(_) => self.visit_inner_with_mutability(x, true), } } diff --git a/charon/tests/ui/closure-as-fn.out b/charon/tests/ui/closure-as-fn.out index f2e1b3850..021f93496 100644 --- a/charon/tests/ui/closure-as-fn.out +++ b/charon/tests/ui/closure-as-fn.out @@ -187,7 +187,7 @@ fn main() storage_live(@3) storage_live(@4) @4 := copy (f@1) - @3 := (move @4)() + @3 := (move (@4))() storage_dead(@4) storage_dead(@3) @0 := () diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out index 773ea48be..e8e6d030c 100644 --- a/charon/tests/ui/closures.out +++ b/charon/tests/ui/closures.out @@ -261,7 +261,7 @@ where @5 := copy (f@2) storage_live(@6) @6 := &*(x@3) - @4 := (move @5)(move (@6)) + @4 := (move (@5))(move (@6)) storage_dead(@6) storage_dead(@5) @0 := Option::Some { 0: move (@4) } @@ -378,7 +378,7 @@ pub fn test_closure_u32(@1: u32) -> u32 @4 := copy (f@2) storage_live(@5) @5 := copy (x@1) - @0 := (move @4)(move (@5)) + @0 := (move (@4))(move (@5)) storage_dead(@5) storage_dead(@4) storage_dead(f@2) @@ -522,7 +522,7 @@ pub fn test_closure_u32s(@1: u32) -> u32 @5 := copy (x@1) storage_live(@6) @6 := copy (x@1) - @0 := (move @4)(move (@5), move (@6)) + @0 := (move (@4))(move (@5), move (@6)) storage_dead(@6) storage_dead(@5) storage_dead(@4) @@ -651,7 +651,7 @@ pub fn test_closure_ref_u32<'a>(@1: &'a (u32)) -> &'a (u32) @5 := copy (f@2) storage_live(@6) @6 := &*(x@1) - @4 := (move @5)(move (@6)) + @4 := (move (@5))(move (@6)) @0 := &*(@4) storage_dead(@6) storage_dead(@5) @@ -799,7 +799,7 @@ where @5 := copy (f@2) storage_live(@6) @6 := &*(x@1) - @4 := (move @5)(move (@6)) + @4 := (move (@5))(move (@6)) @0 := &*(@4) storage_dead(@6) storage_dead(@5) @@ -971,7 +971,7 @@ where @5 := copy (f@2) storage_live(@6) @6 := &*(x@1) - @4 := (move @5)(move (@6)) + @4 := (move (@5))(move (@6)) @0 := &*(@4) storage_dead(@6) storage_dead(@5) @@ -1237,7 +1237,7 @@ pub fn test_id_clone(@1: u32) -> u32 @3 := copy (f@2) storage_live(@4) @4 := copy (x@1) - @0 := (move @3)(move (@4)) + @0 := (move (@3))(move (@4)) storage_dead(@4) storage_dead(@3) storage_dead(f@2) @@ -1262,7 +1262,7 @@ where @3 := copy (f@2) storage_live(@4) @4 := move (x@1) - @0 := (move @3)(move (@4)) + @0 := (move (@3))(move (@4)) storage_dead(@4) storage_dead(@3) storage_dead(f@2) @@ -1601,7 +1601,7 @@ pub fn test_regions_casted<'a>(@1: &'a (u32)) -> u32 storage_live(@6) @6 := &x@1 @5 := &*(@6) - @0 := (move @4)(move (@5)) + @0 := (move (@4))(move (@5)) storage_dead(@5) storage_dead(@4) storage_dead(f@2) diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index ee94cbe48..31e9f2904 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -634,7 +634,7 @@ fn main() storage_live(@4) storage_live(@5) @5 := &*(v@1) with_metadata(copy (v@1.metadata)) - @4 := (move (*(@5.metadata)).method_join_method)(move (@5)) + @4 := (copy ((*(@5.metadata)).method_join_method))(move (@5)) storage_dead(@5) storage_dead(@4) @0 := () diff --git a/charon/tests/ui/issue-378-ctor-as-fn.out b/charon/tests/ui/issue-378-ctor-as-fn.out index 8d5d30fe1..ab2ab6320 100644 --- a/charon/tests/ui/issue-378-ctor-as-fn.out +++ b/charon/tests/ui/issue-378-ctor-as-fn.out @@ -181,7 +181,7 @@ fn main() storage_live(@6) storage_live(@7) @7 := copy (f@4) - @6 := (move @7)(const (42 : u8)) + @6 := (move (@7))(const (42 : u8)) storage_dead(@7) storage_dead(@6) storage_live(f@8) diff --git a/charon/tests/ui/monomorphization/fndefs-casts.out b/charon/tests/ui/monomorphization/fndefs-casts.out index 25e99c709..d79d90c90 100644 --- a/charon/tests/ui/monomorphization/fndefs-casts.out +++ b/charon/tests/ui/monomorphization/fndefs-casts.out @@ -261,7 +261,7 @@ fn main() storage_live(@8) @8 := &a@4 @7 := &*(@8) - @5 := (move @6)(move (@7)) + @5 := (move (@6))(move (@7)) storage_dead(@7) storage_dead(@6) storage_dead(@8) @@ -275,7 +275,7 @@ fn main() storage_live(@13) @13 := &a@4 @12 := &*(@13) - @10 := (move @11)(move (@12)) + @10 := (move (@11))(move (@12)) storage_dead(@12) storage_dead(@11) storage_dead(@13) @@ -287,7 +287,7 @@ fn main() storage_live(@17) @17 := &b@9 @16 := &*(@17) - @14 := (move @15)(move (@16)) + @14 := (move (@15))(move (@16)) storage_dead(@16) storage_dead(@15) storage_dead(@17) @@ -299,7 +299,7 @@ fn main() storage_live(@21) @21 := &b@9 @20 := &*(@21) - @18 := (move @19)(move (@20)) + @18 := (move (@19))(move (@20)) storage_live(@28) storage_live(@29) @29 := const (x) @@ -316,7 +316,7 @@ fn main() @27 := move (@28) @25 := &*(@27) @24 := &*(@25) - @22 := (move @23)(move (@24)) + @22 := (move (@23))(move (@24)) storage_dead(@24) storage_dead(@23) storage_dead(@25) diff --git a/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out b/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out index 022c5bdc7..1e9525fa3 100644 --- a/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out +++ b/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out @@ -223,7 +223,7 @@ fn foo::<()>(@1: ()) @3 := copy (f@2) storage_live(@4) @4 := () - @0 := (move @3)(move (@4)) + @0 := (move (@3))(move (@4)) storage_dead(@4) storage_dead(@3) storage_dead(f@2) diff --git a/charon/tests/ui/simple/fn-ptr.out b/charon/tests/ui/simple/fn-ptr.out new file mode 100644 index 000000000..c126dff44 --- /dev/null +++ b/charon/tests/ui/simple/fn-ptr.out @@ -0,0 +1,46 @@ +# Final LLBC before serialization: + +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + +// Full name: test_crate::foo +fn foo() +{ + let @0: (); // return + + @0 := () + @0 := () + return +} + +// Full name: test_crate::main +fn main() +{ + let @0: (); // return + let f@1: fn(); // local + let @2: (); // anonymous local + let @3: fn(); // anonymous local + + @0 := () + storage_live(f@1) + f@1 := cast(const (foo)) + storage_live(@2) + storage_live(@3) + @3 := copy (f@1) + @2 := (move (@3))() + storage_dead(@3) + storage_dead(@2) + @0 := () + storage_dead(f@1) + return +} + + + diff --git a/charon/tests/ui/simple/fn-ptr.rs b/charon/tests/ui/simple/fn-ptr.rs new file mode 100644 index 000000000..69ce5af64 --- /dev/null +++ b/charon/tests/ui/simple/fn-ptr.rs @@ -0,0 +1,6 @@ +fn foo() {} + +fn main() { + let f: fn() = foo; + f(); +} diff --git a/charon/tests/ui/vtable-simple.out b/charon/tests/ui/vtable-simple.out index 1b326d95a..28c62c52d 100644 --- a/charon/tests/ui/vtable-simple.out +++ b/charon/tests/ui/vtable-simple.out @@ -205,7 +205,7 @@ where @6 := &two-phase-mut *(x@2) with_metadata(copy (x@2.metadata)) storage_live(@7) @7 := &*(arg@1) - @0 := (move (*(@6.metadata)).method_modify)(move (@6), move (@7)) + @0 := (copy ((*(@6.metadata)).method_modify))(move (@6), move (@7)) storage_dead(@7) storage_dead(@6) storage_dead(@5) diff --git a/charon/tests/ui/vtable_drop.out b/charon/tests/ui/vtable_drop.out index 3d8f38da2..3f56a0bbb 100644 --- a/charon/tests/ui/vtable_drop.out +++ b/charon/tests/ui/vtable_drop.out @@ -286,7 +286,7 @@ where @6 := &two-phase-mut *(x@2) with_metadata(copy (x@2.metadata)) storage_live(@7) @7 := &*(arg@1) - @0 := (move (*(@6.metadata)).method_modify)(move (@6), move (@7)) + @0 := (copy ((*(@6.metadata)).method_modify))(move (@6), move (@7)) storage_dead(@7) storage_dead(@6) drop[{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]] @5 diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out index e730fd2c0..b0a053366 100644 --- a/charon/tests/ui/vtables.out +++ b/charon/tests/ui/vtables.out @@ -596,7 +596,7 @@ where @6 := &two-phase-mut *(x@2) with_metadata(copy (x@2.metadata)) storage_live(@7) @7 := &*(arg@1) - @0 := (move (*(@6.metadata)).method_modify)(move (@6), move (@7)) + @0 := (copy ((*(@6.metadata)).method_modify))(move (@6), move (@7)) storage_dead(@7) storage_dead(@6) storage_dead(@5) @@ -1068,7 +1068,7 @@ fn use_lifetime_trait<'a, '_1>(@1: &'_1 ((dyn exists<_dyn> [@TraitClause0_1]: Li @4 := &*(x@1) with_metadata(copy (x@1.metadata)) storage_live(@5) @5 := &*(y@2) - @3 := (move (*(@4.metadata)).method_lifetime_method)(move (@4), move (@5)) + @3 := (copy ((*(@4.metadata)).method_lifetime_method))(move (@4), move (@5)) @0 := &*(@3) storage_dead(@5) storage_dead(@4) @@ -1118,7 +1118,7 @@ fn use_alias<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0_1]: Both32And64<_dy @8 := move (@12) @7 := &*(@8) @6 := &*(@7) - @2 := (move (*(@3.metadata)).method_both_operate)(move (@3), move (@4), move (@6)) + @2 := (copy ((*(@3.metadata)).method_both_operate))(move (@3), move (@4), move (@6)) storage_dead(@6) storage_dead(@4) storage_dead(@3) @@ -1263,7 +1263,7 @@ fn main() storage_live(@4) storage_live(@5) @5 := &*(x@1) with_metadata(copy (x@1.metadata)) - @4 := (move (*(@5.metadata)).method_check)(move (@5)) + @4 := (copy ((*(@5.metadata)).method_check))(move (@5)) if move (@4) { } else { storage_dead(@5) @@ -1320,7 +1320,7 @@ fn main() @24 := const (100 : i32) @23 := &mut @24 @22 := &*(@23) - @20 := (move (*(@21.metadata)).method_modify)(move (@21), move (@22)) + @20 := (copy ((*(@21.metadata)).method_modify))(move (@21), move (@22)) storage_live(@88) storage_live(@89) @89 := const (100 : i32) @@ -1395,7 +1395,7 @@ fn main() storage_live(@43) storage_live(@44) @44 := &*(z@38) with_metadata(copy (z@38.metadata)) - @43 := (move (*(@44.metadata)).method_dummy)(move (@44)) + @43 := (copy ((*(@44.metadata)).method_dummy))(move (@44)) storage_live(@92) storage_live(@93) @93 := const (42 : i32) @@ -1432,7 +1432,7 @@ fn main() @80 := move (@96) @53 := &*(@80) @52 := &*(@53) - @48 := (move (*(@49.metadata)).method_both_operate)(move (@49), move (@50), move (@52)) + @48 := (copy ((*(@49.metadata)).method_both_operate))(move (@49), move (@50), move (@52)) storage_live(@98) storage_live(@99) @99 := const (42 : i32)