Commit ab788203 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

cleaning

parent e7fa1950
......@@ -834,7 +834,7 @@ ARCHDIRS=$arch
EXECUTE=kvx-cluster --syscall=libstd_scalls.so --
CFLAGS= -D __KVX_COS__
SIMU=kvx-cluster --
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.v\\
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v\\
Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\
ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\
......
#include "init.h"
unsigned long long int checksum () {
unsigned long long int seed = 0ULL;
hash(&seed, var_36);
hash(&seed, var_37);
hash(&seed, var_38);
hash(&seed, var_39);
hash(&seed, var_40);
hash(&seed, var_41);
hash(&seed, var_42);
hash(&seed, var_43);
hash(&seed, var_44);
hash(&seed, var_45);
hash(&seed, var_46);
hash(&seed, var_47);
hash(&seed, var_48);
hash(&seed, var_49);
hash(&seed, var_50);
hash(&seed, var_51);
hash(&seed, var_52);
hash(&seed, var_53);
hash(&seed, var_54);
hash(&seed, var_55);
hash(&seed, var_56);
hash(&seed, var_57);
hash(&seed, var_58);
hash(&seed, var_59);
hash(&seed, var_60);
hash(&seed, var_61);
hash(&seed, var_62);
hash(&seed, var_63);
hash(&seed, var_64);
hash(&seed, var_65);
hash(&seed, var_70);
hash(&seed, var_78);
hash(&seed, var_82);
hash(&seed, var_90);
hash(&seed, var_94);
hash(&seed, var_100);
hash(&seed, var_106);
hash(&seed, var_123);
hash(&seed, var_129);
hash(&seed, var_143);
hash(&seed, var_152);
hash(&seed, var_156);
hash(&seed, var_162);
hash(&seed, var_178);
hash(&seed, var_217);
hash(&seed, var_234);
hash(&seed, var_240);
hash(&seed, var_241);
hash(&seed, var_260);
hash(&seed, var_268);
hash(&seed, var_284);
hash(&seed, var_297);
hash(&seed, var_314);
hash(&seed, var_358);
hash(&seed, var_359);
hash(&seed, var_367);
hash(&seed, var_392);
hash(&seed, var_468);
hash(&seed, var_500);
hash(&seed, var_514);
hash(&seed, var_522);
hash(&seed, var_543);
hash(&seed, var_544);
hash(&seed, var_547);
hash(&seed, var_549);
hash(&seed, var_558);
hash(&seed, var_591);
hash(&seed, struct_obj_5.member_1_0);
hash(&seed, struct_obj_5.member_1_1);
hash(&seed, struct_obj_5.member_1_2);
hash(&seed, struct_obj_5.member_1_3);
hash(&seed, struct_obj_6.member_5_0);
hash(&seed, struct_obj_6.member_5_1);
hash(&seed, struct_obj_6.member_5_2);
hash(&seed, struct_obj_6.member_5_3);
hash(&seed, struct_obj_7.member_1_0);
hash(&seed, struct_obj_7.member_1_1);
hash(&seed, struct_obj_7.member_1_2);
hash(&seed, struct_obj_7.member_1_3);
hash(&seed, struct_obj_8.member_4_0);
hash(&seed, struct_obj_8.member_4_1.member_3_0);
hash(&seed, struct_obj_8.member_4_1.member_3_1.member_1_0);
hash(&seed, struct_obj_8.member_4_1.member_3_1.member_1_1);
hash(&seed, struct_obj_8.member_4_1.member_3_1.member_1_2);
hash(&seed, struct_obj_8.member_4_1.member_3_1.member_1_3);
hash(&seed, struct_obj_8.member_4_2);
hash(&seed, struct_obj_8.member_4_3);
hash(&seed, struct_obj_8.member_4_4);
hash(&seed, struct_obj_8.member_4_5);
hash(&seed, struct_obj_8.member_4_6);
hash(&seed, struct_obj_8.member_4_7);
hash(&seed, struct_obj_8.member_4_8);
hash(&seed, struct_obj_8.member_4_9.member_1_0);
hash(&seed, struct_obj_8.member_4_9.member_1_1);
hash(&seed, struct_obj_8.member_4_9.member_1_2);
hash(&seed, struct_obj_8.member_4_9.member_1_3);
hash(&seed, struct_obj_9.member_2_0);
hash(&seed, struct_obj_9.member_2_1.member_1_0);
hash(&seed, struct_obj_9.member_2_1.member_1_1);
hash(&seed, struct_obj_9.member_2_1.member_1_2);
hash(&seed, struct_obj_9.member_2_1.member_1_3);
hash(&seed, struct_obj_9.member_2_2);
hash(&seed, struct_obj_9.member_2_3.member_1_0);
hash(&seed, struct_obj_9.member_2_3.member_1_1);
hash(&seed, struct_obj_9.member_2_3.member_1_2);
hash(&seed, struct_obj_9.member_2_3.member_1_3);
hash(&seed, struct_obj_9.member_2_4);
hash(&seed, struct_obj_9.member_2_5);
hash(&seed, struct_obj_9.member_2_6);
hash(&seed, struct_obj_9.member_2_7);
hash(&seed, struct_obj_10.member_1_0);
hash(&seed, struct_obj_10.member_1_1);
hash(&seed, struct_obj_10.member_1_2);
hash(&seed, struct_obj_10.member_1_3);
return seed;
}
\ No newline at end of file
#include <stdio.h>
#include "init.h"
extern void init ();
extern void foo ();
extern unsigned long long int checksum ();
int main () {
init ();
foo ();
printf("%llu\n", checksum ()); return 0;
}
\ No newline at end of file
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
void hash(unsigned long long int *seed, unsigned long long int const v) {
*seed ^= v + 0x9e3779b9 + ((*seed)<<6) + ((*seed)>>2);
}
#include "init.h"
const unsigned short var_1 = 64966;
const unsigned short var_2 = 17784;
signed char var_3 = 58;
const unsigned short var_4 = 3656;
unsigned short var_5 = 17583;
const unsigned short var_6 = 40663;
const signed char var_7 = 42;
unsigned short var_8 = 14662;
unsigned short var_9 = 13482;
unsigned short var_10 = 21751;
const short var_11 = 9782;
const unsigned short var_12 = 29985;
short var_13 = -23903;
const signed char var_14 = 26;
const unsigned short var_15 = 38613;
unsigned short var_16 = 7910;
short var_17 = 32667;
signed char var_18 = 77;
signed char var_19 = 69;
unsigned short var_20 = 49524;
const signed char var_21 = -59;
const signed char var_22 = 114;
const unsigned short var_23 = 43999;
short var_24 = -4596;
signed char var_25 = 127;
const unsigned short var_26 = 14598;
const short var_27 = 15321;
short var_28 = 13394;
const unsigned short var_29 = 51752;
const unsigned short var_30 = 42705;
const short var_31 = -23514;
unsigned short var_32 = 46800;
const unsigned short var_33 = 40302;
const signed char var_34 = -74;
unsigned short var_35 = 14428;
short var_36 = 27385;
signed char var_37 = 116;
signed char var_38 = 47;
unsigned short var_39 = 28164;
signed char var_40 = 68;
unsigned short var_41 = 48535;
signed char var_42 = -56;
unsigned short var_43 = 63272;
unsigned short var_44 = 53605;
signed char var_45 = -76;
unsigned short var_46 = 37656;
signed char var_47 = -2;
unsigned short var_48 = 20934;
signed char var_49 = -21;
unsigned short var_50 = 46979;
short var_51 = -11787;
short var_52 = 9874;
short var_53 = 13740;
short var_54 = -24909;
signed char var_55 = -12;
unsigned short var_56 = 20186;
signed char var_57 = -80;
signed char var_58 = 48;
unsigned short var_59 = 59812;
short var_60 = 21585;
signed char var_61 = -16;
unsigned short var_62 = 49246;
short var_63 = 21666;
signed char var_64 = -18;
short var_65 = -12846;
signed char var_70 = 63;
short var_78 = -3444;
unsigned short var_82 = 58294;
short var_90 = -25718;
unsigned short var_94 = 54118;
short var_100 = 16012;
short var_106 = 6394;
unsigned short var_123 = 42864;
short var_129 = 18229;
signed char var_143 = 92;
short var_152 = -25759;
signed char var_156 = -88;
signed char var_162 = 86;
short var_178 = -15567;
signed char var_217 = 37;
short var_234 = 29976;
signed char var_240 = 29;
unsigned short var_241 = 39297;
signed char var_260 = -30;
signed char var_268 = 13;
short var_284 = -4345;
unsigned short var_297 = 16067;
signed char var_314 = -126;
unsigned short var_358 = 48899;
short var_359 = 5585;
signed char var_367 = 57;
unsigned short var_392 = 6146;
signed char var_468 = -7;
signed char var_500 = 28;
short var_514 = -27356;
signed char var_522 = 67;
signed char var_543 = -115;
unsigned short var_544 = 38397;
signed char var_547 = 105;
signed char var_549 = 62;
short var_558 = -1976;
signed char var_591 = 78;
struct_5 struct_obj_1;
struct_5 struct_obj_2;
struct_5 struct_obj_3;
struct_2 struct_obj_4;
struct_1 struct_obj_5;
struct_5 struct_obj_6;
struct_1 struct_obj_7;
struct_4 struct_obj_8;
struct_2 struct_obj_9;
struct_1 struct_obj_10;
void init () {
struct_obj_1.member_5_0 = (short) (-13981);
struct_obj_1.member_5_1 = (unsigned short) (32569);
struct_obj_1.member_5_2 = (unsigned short) (55905);
struct_obj_1.member_5_3 = (short) (740);
struct_obj_2.member_5_0 = (short) (-16520);
struct_obj_2.member_5_1 = (unsigned short) (25768);
struct_obj_2.member_5_2 = (unsigned short) (41445);
struct_obj_2.member_5_3 = (short) (25458);
struct_obj_3.member_5_0 = (short) (-27814);
struct_obj_3.member_5_1 = (unsigned short) (32840);
struct_obj_3.member_5_2 = (unsigned short) (59825);
struct_obj_3.member_5_3 = (short) (-26656);
struct_obj_4.member_2_0 = (short) (7610);
struct_obj_4.member_2_1.member_1_0 = (signed char) (86);
struct_obj_4.member_2_1.member_1_1 = (short) (-29951);
struct_obj_4.member_2_1.member_1_2 = (signed char) (-57);
struct_obj_4.member_2_1.member_1_3 = (short) (-1514);
struct_obj_4.member_2_2 = (unsigned short) (30795);
struct_obj_4.member_2_3.member_1_0 = (signed char) (17);
struct_obj_4.member_2_3.member_1_1 = (short) (-21792);
struct_obj_4.member_2_3.member_1_2 = (signed char) (-78);
struct_obj_4.member_2_3.member_1_3 = (short) (-19417);
struct_obj_4.member_2_4 = (short) (-19205);
struct_obj_4.member_2_5 = (unsigned short) (10096);
struct_obj_4.member_2_6 = (unsigned short) (56048);
struct_obj_4.member_2_7 = (short) (-9525);
struct_obj_5.member_1_0 = (signed char) (-105);
struct_obj_5.member_1_1 = (short) (28953);
struct_obj_5.member_1_2 = (signed char) (-80);
struct_obj_5.member_1_3 = (short) (-20984);
struct_obj_6.member_5_0 = (short) (30730);
struct_obj_6.member_5_1 = (unsigned short) (44652);
struct_obj_6.member_5_2 = (unsigned short) (45968);
struct_obj_6.member_5_3 = (short) (12419);
struct_obj_7.member_1_0 = (signed char) (-74);
struct_obj_7.member_1_1 = (short) (-6639);
struct_obj_7.member_1_2 = (signed char) (-119);
struct_obj_7.member_1_3 = (short) (13879);
struct_obj_8.member_4_0 = (unsigned short) (17346);
struct_obj_8.member_4_1.member_3_0 = (short) (657);
struct_obj_8.member_4_1.member_3_1.member_1_0 = (signed char) (-103);
struct_obj_8.member_4_1.member_3_1.member_1_1 = (short) (25291);
struct_obj_8.member_4_1.member_3_1.member_1_2 = (signed char) (-76);
struct_obj_8.member_4_1.member_3_1.member_1_3 = (short) (-25024);
struct_obj_8.member_4_2 = (signed char) (42);
struct_obj_8.member_4_3 = (unsigned short) (57223);
struct_obj_8.member_4_4 = (signed char) (58);
struct_obj_8.member_4_5 = (short) (-1330);
struct_obj_8.member_4_6 = (short) (-13828);
struct_obj_8.member_4_7 = (unsigned short) (26678);
struct_obj_8.member_4_8 = (unsigned short) (52711);
struct_obj_8.member_4_9.member_1_0 = (signed char) (6);
struct_obj_8.member_4_9.member_1_1 = (short) (13897);
struct_obj_8.member_4_9.member_1_2 = (signed char) (-94);
struct_obj_8.member_4_9.member_1_3 = (short) (-30110);
struct_obj_9.member_2_0 = (short) (-24156);
struct_obj_9.member_2_1.member_1_0 = (signed char) (40);
struct_obj_9.member_2_1.member_1_1 = (short) (31967);
struct_obj_9.member_2_1.member_1_2 = (signed char) (-36);
struct_obj_9.member_2_1.member_1_3 = (short) (21679);
struct_obj_9.member_2_2 = (unsigned short) (40629);
struct_obj_9.member_2_3.member_1_0 = (signed char) (116);
struct_obj_9.member_2_3.member_1_1 = (short) (-741);
struct_obj_9.member_2_3.member_1_2 = (signed char) (101);
struct_obj_9.member_2_3.member_1_3 = (short) (24485);
struct_obj_9.member_2_4 = (short) (13544);
struct_obj_9.member_2_5 = (unsigned short) (26978);
struct_obj_9.member_2_6 = (unsigned short) (9057);
struct_obj_9.member_2_7 = (short) (21085);
struct_obj_10.member_1_0 = (signed char) (94);
struct_obj_10.member_1_1 = (short) (28577);
struct_obj_10.member_1_2 = (signed char) (-56);
struct_obj_10.member_1_3 = (short) (-21782);
}
\ No newline at end of file
void hash(unsigned long long int *seed, unsigned long long int const v);
extern const unsigned short var_1;
extern const unsigned short var_2;
extern signed char var_3;
extern const unsigned short var_4;
extern unsigned short var_5;
extern const unsigned short var_6;
extern const signed char var_7;
extern unsigned short var_8;
extern unsigned short var_9;
extern unsigned short var_10;
extern const short var_11;
extern const unsigned short var_12;
extern short var_13;
extern const signed char var_14;
extern const unsigned short var_15;
extern unsigned short var_16;
extern short var_17;
extern signed char var_18;
extern signed char var_19;
extern unsigned short var_20;
extern const signed char var_21;
extern const signed char var_22;
extern const unsigned short var_23;
extern short var_24;
extern signed char var_25;
extern const unsigned short var_26;
extern const short var_27;
extern short var_28;
extern const unsigned short var_29;
extern const unsigned short var_30;
extern const short var_31;
extern unsigned short var_32;
extern const unsigned short var_33;
extern const signed char var_34;
extern unsigned short var_35;
extern short var_36;
extern signed char var_37;
extern signed char var_38;
extern unsigned short var_39;
extern signed char var_40;
extern unsigned short var_41;
extern signed char var_42;
extern unsigned short var_43;
extern unsigned short var_44;
extern signed char var_45;
extern unsigned short var_46;
extern signed char var_47;
extern unsigned short var_48;
extern signed char var_49;
extern unsigned short var_50;
extern short var_51;
extern short var_52;
extern short var_53;
extern short var_54;
extern signed char var_55;
extern unsigned short var_56;
extern signed char var_57;
extern signed char var_58;
extern unsigned short var_59;
extern short var_60;
extern signed char var_61;
extern unsigned short var_62;
extern short var_63;
extern signed char var_64;
extern short var_65;
extern signed char var_70;
extern short var_78;
extern unsigned short var_82;
extern short var_90;
extern unsigned short var_94;
extern short var_100;
extern short var_106;
extern unsigned short var_123;
extern short var_129;
extern signed char var_143;
extern short var_152;
extern signed char var_156;
extern signed char var_162;
extern short var_178;
extern signed char var_217;
extern short var_234;
extern signed char var_240;
extern unsigned short var_241;
extern signed char var_260;
extern signed char var_268;
extern short var_284;
extern unsigned short var_297;
extern signed char var_314;
extern unsigned short var_358;
extern short var_359;
extern signed char var_367;
extern unsigned short var_392;
extern signed char var_468;
extern signed char var_500;
extern short var_514;
extern signed char var_522;
extern signed char var_543;
extern unsigned short var_544;
extern signed char var_547;
extern signed char var_549;
extern short var_558;
extern signed char var_591;
typedef struct {
signed char member_1_0;
short member_1_1;
signed char member_1_2;
short member_1_3;
} struct_1;
typedef struct {
short member_2_0;
struct_1 member_2_1;
unsigned short member_2_2;
struct_1 member_2_3;
short member_2_4;
unsigned short member_2_5;
unsigned short member_2_6;
short member_2_7;
} struct_2;
typedef struct {
short member_3_0;
struct_1 member_3_1;
} struct_3;
typedef struct {
unsigned short member_4_0;
struct_3 member_4_1;
signed char member_4_2;
unsigned short member_4_3;
signed char member_4_4;
short member_4_5;
short member_4_6;
unsigned short member_4_7;
unsigned short member_4_8;
struct_1 member_4_9;
} struct_4;
typedef struct {
short member_5_0;
unsigned short member_5_1;
unsigned short member_5_2;
short member_5_3;
} struct_5;
typedef struct {
signed char member_6_0;
unsigned short member_6_1;
short member_6_2;
struct_3 member_6_3;
struct_3 member_6_4;
signed char member_6_5;
short member_6_6;
} struct_6;
extern struct_5 struct_obj_1;
extern struct_5 struct_obj_2;
extern struct_5 struct_obj_3;
extern struct_2 struct_obj_4;
extern struct_1 struct_obj_5;
extern struct_5 struct_obj_6;
extern struct_1 struct_obj_7;
extern struct_4 struct_obj_8;
extern struct_2 struct_obj_9;
extern struct_1 struct_obj_10;
Require Import Coqlib Maps AST Integers Values Memory Events Globalenvs Smallstep.
Require Import Op Machregs Locations Stacklayout Conventions.
Require Import Mach Machblock OptionMonad.
(** Registers and States *)
Inductive preg: Type :=
| PC: preg (* program counter *)
| RA: preg (* return-address *)
| SP: preg (* stack-pointer *)
| preg_of: mreg -> preg.
Coercion preg_of: mreg >-> preg.
Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
Proof.
decide equality.
apply mreg_eq.
Defined.
Module PregEq.
Definition t := preg.
Definition eq := preg_eq.
End PregEq.
Module Pregmap := EMap(PregEq).
Definition regset := Pregmap.t val.
Module AsmNotations.
(* Declare Scope asm. *)
Notation "a # b" := (a b) (at level 1, only parsing) : asm.
Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
Open Scope asm.
End AsmNotations.
Import AsmNotations.
Definition to_Machrs (rs: regset): Mach.regset :=
fun (r:mreg) => rs r.
Coercion to_Machrs: regset >-> Mach.regset.
Definition set_from_Machrs (mrs: Mach.regset) (rs: regset): regset :=
fun (r:preg) =>