Add some example asm files (mit-plv#2021)

From gcc / clang I want to be able to eventually handle the output of gcc/clang on our C code.
JasonGross · Mar 4, 2025 · 77571a8 · 77571a8
1 parent 8f205d4
commit 77571a8
Show file tree

Hide file tree

Showing 22 changed files with 23,705 additions and 0 deletions.
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O0.s b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O0.s
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O0.v b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O0.v
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O1.s b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O1.s
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O1.v b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O1.v
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O2.s b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O2.s
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O2.v b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O2.v
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O3.s b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O3.s
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O3.v b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_O3.v
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_Os.s b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_Os.s
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_Os.v b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_Os.v
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O0.s b/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O0.s
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O0.v b/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O0.v
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O1.s b/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O1.s
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O1.v b/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O1.v
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O2.s b/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O2.s
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O2.v b/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O2.v
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O3.s b/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O3.s
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O3.v b/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_O3.v
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_Os.s b/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_Os.s
diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_Os.v b/src/Assembly/Parse/Examples/fiat_25519_all_gcc_14_1_Os.v
diff --git a/src/Assembly/Parse/Examples/make-example.sh b/src/Assembly/Parse/Examples/make-example.sh
@@ -0,0 +1,15 @@
+#!/bin/sh
+
+cat << EOF
+From Coq Require Import String List.
+Import ListNotations.
+Local Open Scope string_scope.
+Local Open Scope list_scope.
+Example example : list string := [
+EOF
+
+while read -r line; do
+  echo "\"$line\";"
+done
+
+echo '""].'
diff --git a/src/Assembly/Parse/TestAsm.v b/src/Assembly/Parse/TestAsm.v
@@ -13,6 +13,16 @@ Require Crypto.Assembly.Parse.Examples.fiat_p256_square_optimised_seed103.
 Require Crypto.Assembly.Parse.Examples.fiat_p256_square_optimised_seed46.
 Require Crypto.Assembly.Parse.Examples.fiat_p256_square_optimised_seed6.
 Require Crypto.Assembly.Parse.Examples.boringssl_nasm_full_mul_p256.
+Require Crypto.Assembly.Parse.Examples.fiat_25519_all_gcc_14_1_O0.
+Require Crypto.Assembly.Parse.Examples.fiat_25519_all_gcc_14_1_O1.
+Require Crypto.Assembly.Parse.Examples.fiat_25519_all_gcc_14_1_O2.
+Require Crypto.Assembly.Parse.Examples.fiat_25519_all_gcc_14_1_O3.
+Require Crypto.Assembly.Parse.Examples.fiat_25519_all_gcc_14_1_Os.
+Require Crypto.Assembly.Parse.Examples.fiat_25519_all_clang_19_1_0_O0.
+Require Crypto.Assembly.Parse.Examples.fiat_25519_all_clang_19_1_0_O1.
+Require Crypto.Assembly.Parse.Examples.fiat_25519_all_clang_19_1_0_O2.
+Require Crypto.Assembly.Parse.Examples.fiat_25519_all_clang_19_1_0_O3.
+Require Crypto.Assembly.Parse.Examples.fiat_25519_all_clang_19_1_0_Os.
 Import ListNotations.
 Local Open Scope list_scope.
 Local Open Scope string_scope.