Change FnOperand::Move -> Dynamic

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"

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

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 = {

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 =

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

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.150"
+version = "0.1.151"
 authors = [
     "Son Ho <[email protected]>",
     "Guillaume Boisseau <[email protected]>",

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)]

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)?;

charon/src/pretty/fmt_with_ctx.rs

@@ -428,7 +428,7 @@ impl<C: AstFormatter> FmtWithCtx<C> 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)),
         }
     }
 }

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(())
 }

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<Infallible> {
         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),
         }
     }
 

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 := ()

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)

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 ([email protected]))
-    @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 := ()

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)

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)

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)

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<foo, fn()>(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
+}
+
+
+

charon/tests/ui/simple/fn-ptr.rs

@@ -0,0 +1,6 @@
+fn foo() {}
+
+fn main() {
+    let f: fn() = foo;
+    f();
+}

charon/tests/ui/vtable-simple.out

@@ -205,7 +205,7 @@ where
     @6 := &two-phase-mut *(x@2) with_metadata(copy ([email protected]))
     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)

charon/tests/ui/vtable_drop.out

@@ -286,7 +286,7 @@ where
     @6 := &two-phase-mut *(x@2) with_metadata(copy ([email protected]))
     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<T>[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}<i32, Global>[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]] @5