Merge pull request #374 from formal-land/guillaume-claret@add-axiom-for-assembly-blocks

Add axiom for assembly blocks

Author: clarus

CoqOfRust/CoqOfRust.v

@@ -115,6 +115,9 @@ Definition mut_ref : Set -> Set := ref.
 
 Parameter eqb : forall {A : Set}, A -> A -> bool.
 
+(** We replace assembly blocks by a value of type unit. *)
+Parameter InlineAssembly : unit.
+
 (** The functions on [Z] should eventually be replaced by functions on the
     corresponding integer types. *)
 Global Instance Method_Z_abs `{State.Trait} : Notation.Dot "abs" := {

CoqOfRust/blacklist.txt

@@ -122,21 +122,11 @@ examples/traits/supertraits.v
 examples/traits/traits.v
 examples/unsafe_operations/calling_unsafe_functions.v
 examples/unsafe_operations/inline_assembly_clobbered_registers.v
-examples/unsafe_operations/inline_assembly_explicit_register_operands.v
-examples/unsafe_operations/inline_assembly_inlateout_case_implemented.v
-examples/unsafe_operations/inline_assembly_inlateout_case_non_used.v
 examples/unsafe_operations/inline_assembly_inlateout_mul.v
 examples/unsafe_operations/inline_assembly_inout.v
-examples/unsafe_operations/inline_assembly_inputs_and_outputs_another_example_without_mov.v
 examples/unsafe_operations/inline_assembly_inputs_and_outputs_another_example.v
 examples/unsafe_operations/inline_assembly_inputs_and_outputs.v
-examples/unsafe_operations/inline_assembly_labels.v
-examples/unsafe_operations/inline_assembly_memory_address_operands.v
-examples/unsafe_operations/inline_assembly_options.v
-examples/unsafe_operations/inline_assembly_register_template_modifiers.v
-examples/unsafe_operations/inline_assembly_scratch_register.v
 examples/unsafe_operations/inline_assembly_symbol_operands_and_abi_clobbers.v
-examples/unsafe_operations/inline_assembly.v
 examples/unsafe_operations/raw_pointers.v
 examples/variable_bindings/declare_first.v
 examples_axiomatized/custom_types/enums_testcase_linked_list.v

coq_translation/default/examples/unsafe_operations/inline_assembly.v

@@ -3,5 +3,5 @@ Require Import CoqOfRust.CoqOfRust.
 
 (* #[allow(dead_code)] - function was ignored by the compiler *)
 Definition main `{H' : State.Trait} : M (H := H') unit :=
-  let _ := InlineAsm in
+  let _ := InlineAssembly in
   Pure tt.

coq_translation/default/examples/unsafe_operations/inline_assembly_clobbered_registers.v

@@ -5,7 +5,7 @@ Require Import CoqOfRust.CoqOfRust.
 Definition main `{H' : State.Trait} : M (H := H') unit :=
   let* name_buf := repeat 0 in
   let _ :=
-    let _ := InlineAsm in
+    let _ := InlineAssembly in
     tt in
   let* name :=
     let* α0 := core.str.converts.from_utf8 (addr_of name_buf) in

coq_translation/default/examples/unsafe_operations/inline_assembly_explicit_register_operands.v

@@ -4,5 +4,5 @@ Require Import CoqOfRust.CoqOfRust.
 (* #[allow(dead_code)] - function was ignored by the compiler *)
 Definition main `{H' : State.Trait} : M (H := H') unit :=
   let cmd := 209 in
-  let _ := InlineAsm in
+  let _ := InlineAssembly in
   Pure tt.

coq_translation/default/examples/unsafe_operations/inline_assembly_inlateout_case_implemented.v

@@ -6,7 +6,7 @@ Definition main `{H' : State.Trait} : M (H := H') unit :=
   let a : u64 := 4 in
   let b : u64 := 4 in
   let _ :=
-    let _ := InlineAsm in
+    let _ := InlineAssembly in
     tt in
   let* _ :=
     match (addr_of a, addr_of 8) with

coq_translation/default/examples/unsafe_operations/inline_assembly_inlateout_case_non_used.v

@@ -7,7 +7,7 @@ Definition main `{H' : State.Trait} : M (H := H') unit :=
   let b : u64 := 4 in
   let c : u64 := 4 in
   let _ :=
-    let _ := InlineAsm in
+    let _ := InlineAssembly in
     tt in
   let* _ :=
     match (addr_of a, addr_of 12) with

coq_translation/default/examples/unsafe_operations/inline_assembly_inlateout_mul.v

@@ -8,7 +8,7 @@ Definition mul `{H' : State.Trait} (a : u64) (b : u64) : M (H := H') u128 :=
   let lo : u64 := tt in
   let hi : u64 := tt in
   let _ :=
-    let _ := InlineAsm in
+    let _ := InlineAssembly in
     tt in
   let* α0 := (cast hi u128).["shl"] 64 in
   α0.["add"] (cast lo u128).

coq_translation/default/examples/unsafe_operations/inline_assembly_inout.v

@@ -6,7 +6,7 @@ Definition main `{H' : State.Trait} : M (H := H') unit :=
   let x : u64 := 3 in
   let y : u64 := tt in
   let _ :=
-    let _ := InlineAsm in
+    let _ := InlineAssembly in
     tt in
   let* _ :=
     match (addr_of y, addr_of 8) with

coq_translation/default/examples/unsafe_operations/inline_assembly_inputs_and_outputs.v

@@ -5,7 +5,7 @@ Require Import CoqOfRust.CoqOfRust.
 Definition main `{H' : State.Trait} : M (H := H') unit :=
   let x : u64 := tt in
   let _ :=
-    let _ := InlineAsm in
+    let _ := InlineAssembly in
     tt in
   let* _ :=
     match (addr_of x, addr_of 5) with