Added EVM test js script; Added debugging print

maruibin · maruibin · commit 2d9cc88e8526 · 2020-05-16T22:20:52.000-04:00
diff --git a/package-lock.json b/package-lock.json
diff --git a/src/example_contract/simpleStorage.sc b/src/example_contract/simpleStorage.sc
@@ -14,7 +14,7 @@ constructor c (){
 
 method set(x: int) {
 	guard{
-		x > 0 ;
+		/-x > 0 ;-/
 	}
 	storage{
     	storedData |-> x;
diff --git a/src/example_contract/test-simpleStorage.js b/src/example_contract/test-simpleStorage.js
@@ -0,0 +1,53 @@
+#!/usr/bin/env node
+
+// const net = require('net');
+// const solc = require('solc');
+const fs = require('fs');
+const ethers = require("ethers");
+
+if (process.argv.length != 3) {
+    console.log("invalid args");
+    process.exit(1);
+}
+
+const endpoint = "http://localhost:8545";
+const provider = new ethers.providers.JsonRpcProvider(endpoint);
+
+// const abi = [
+//   "constructor()",
+//   "function initialize () public returns (uint)",
+//   "function totalSupply() view returns (uint)",
+//   "function balanceOf(uint) view returns (uint)",
+//   "function transfer(uint, int) returns (bool)"
+// ];
+
+const abi = [
+ {"type":"function",
+   "name":"set",
+   "inputs":[{"name":"x", "type":"uint256"}],
+   "outputs":[{"name":"", "type":"uint256"}],
+   "payable":"true",
+   "constant":false,
+   "stateMutability":"view"}];
+
+const bytecode = fs.readFileSync(process.argv[2]).toString().replace(/\n|\t|\r| /g, "");
+const signer = provider.getSigner(0);
+const creator = signer.getAddress();
+
+async function deploy() {
+  console.log("sending creation transaction...")
+  let factory = new ethers.ContractFactory(abi, bytecode, signer);
+  let contract = await factory.deploy();
+  await contract.deployed();
+  console.log("contract address: " + contract.address);
+  console.log("transaction hash: " + contract.deployTransaction.hash);
+  let deployedBytecode = await provider.getCode(contract.address);
+  // console.log("deployed bytecode: " + deployedBytecode);
+
+  let setv = 240; // arbitrary uint
+  console.log("calling set...");
+  setval = await contract.set(setv);
+  console.log("value set as: " + setval);
+}
+
+deploy();
diff --git a/src/translateMinic.ml b/src/translateMinic.ml
@@ -66,7 +66,8 @@ let struct_name_to_ident2 = ident_generator "" "struct"
 let struct_field_name_to_ident2 = ident_generator "" "field"
 let backend_ident_of_globvar  = ident_generator "var_" "var2"
 let backend_ident_of_funcname = ident_generator "ident_" "function"
-let backend_ident_of_tempvar =  ident_generator "temp_" "var"
+(* let backend_ident_of_tempvar =  ident_generator "temp_" "var" *)
+let backend_ident_of_tempvar =  positive_of_int 11
 
 let rec gen_ctype =
   let open Ctypes in 
@@ -128,7 +129,8 @@ let rec gen_rexpr e =
   let open Language in
   match e with
   | (t, SId(Sglobal,l)) -> Evar (backend_ident_of_globvar l, gen_ctype t)
-  | (t, SId(Slocal,l)) -> Etempvar (backend_ident_of_tempvar l, gen_ctype t)
+  (* | (t, SId(Slocal,l)) -> Etempvar (backend_ident_of_tempvar l, gen_ctype t) *)
+  | (t, SId(Slocal,l)) -> Etempvar (backend_ident_of_tempvar, gen_ctype t)
   | se -> raise (Failure ("Not implemented: " ^ string_of_sexpr se))
 
 let rec gen_lexpr e =
@@ -142,7 +144,8 @@ let rec gen_lexpr e =
                         |true -> Econst_int256 (Int256.one, Tint (I256, Unsigned))
                         |false -> Econst_int256 (Int256.zero, Tint (I256, Unsigned)) )
   | (t, SId(Sglobal,l)) -> Evar (backend_ident_of_globvar l, gen_ctype t)
-  | (t, SId(Slocal,l)) -> Etempvar (backend_ident_of_tempvar l, gen_ctype t)
+  (* | (t, SId(Slocal,l)) -> Etempvar (backend_ident_of_tempvar l, gen_ctype t) *)
+  | (t, SId(Slocal,l)) -> Etempvar (backend_ident_of_tempvar, gen_ctype t)
   | (t1, SBinop ((t2, se1), op, (t3, se2))) -> Ebinop (gen_binop op, gen_lexpr (t2, se1), gen_lexpr (t3, se2), gen_ctype t1)	
   | (t, SComparsion ((t1, se1), op, (t2, se2))) -> Ebinop (gen_binop op, gen_lexpr (t1, se1), gen_lexpr (t2, se2), gen_ctype t)	
   | (t, SMapexpr((t1, se1), selist)) -> 
@@ -182,7 +185,8 @@ let gen_params sparams =
   let open Datatypes in
   let open Globalenvs.Genv in
   let cvt = function
-    | Var(Id str, typ) -> Some (Coq_pair(backend_ident_of_tempvar str, gen_ctype typ))
+    (* | Var(Id str, typ) -> Some (Coq_pair(backend_ident_of_tempvar str, gen_ctype typ)) *)
+    | Var(Id str, typ) -> Some (Coq_pair(backend_ident_of_tempvar, gen_ctype typ))
     | _ -> None
   in
   coqlist_of_list (filter_map cvt sparams)
@@ -247,13 +251,21 @@ let gen_methoddef m =
   { 
     fn_return = ret_type m.sreturns;
     fn_params = gen_params m.sparams; (* (ident, coq_type) prod list; *)
-    fn_temps  = Coq_nil; (* coqlist_of_list (gen_tempenv ((dest,mt.aMethodReturnType.aTypeCtype) :: gen_cmd_locals m.aMethodBody dest))*)
-    fn_body =  (if has_return then
+    (* fn_temps  = Coq_nil; coqlist_of_list (gen_tempenv ((dest,mt.aMethodReturnType.aTypeCtype) :: gen_cmd_locals m.aMethodBody dest)) *)
+    fn_temps  = coqlist_of_list [Coq_pair(positive_of_int 10, gen_ctype (Void "void"))];
+    fn_body =  gen_storage_cmd m.sstorage_body
+    (* (if has_return then
       Ssequence(Ssequence(gen_guard_cmd m.sguard_body, gen_storage_cmd m.sstorage_body), gen_return_cmd m.sreturns)
 		else 
-      Ssequence(gen_guard_cmd m.sguard_body, gen_storage_cmd m.sstorage_body))
+      Ssequence(gen_guard_cmd m.sguard_body, gen_storage_cmd m.sstorage_body)) *)
   }
 
+  (* { fn_return = Tvoid;
+  fn_params = (11,TInt (SIZE,SIGNEDNESS))::nil;
+  fn_temps =  (10,Tvoid)::nil;
+  fn_body = Sassign(Evar(550,TInt (SIZE,SIGNEDNESS)),Etempvar(11,TInt (SIZE,SIGNEDNESS)))
+  } *)
+
 (* let gen_methoddef objname m =
   let open Datatypes in
   let mt = m.aMethodType in
@@ -273,15 +285,74 @@ let gen_methoddef m =
       body)
   } *)
 
+(* Print MiniC expressions/statements, for debugging purposes. *)
 
 
+let rec string_of_ctype = 
+  let open Ctypes in
+  function
+  | Tvoid -> "Tvoid"
+  | Tint (_,_) -> "TInt (SIZE,SIGNEDNESS)"
+  | Tpointer _ -> "Tpointer"
+  | Tarray (t,z) -> ("Tarray ("^string_of_ctype t^","^string_of_int(int_of_z z)^")")
+  | Thashmap (t1,t2) -> ("Thashmap("^string_of_ctype t1^","^string_of_ctype t2^")")
+  | Tfunction (ts,t) -> "Tfunction (TYPES,TYPE)"
+  | Tstruct (id,flds) -> "Tstring (IDENT, FIELDS)"
+  | Tunion  (id,flds) -> "Tunion (IDENT, FIELDS)"
+  | Tcomp_ptr id -> "Tcomp_ptr ID"
+		    
+let rec string_of_expr = function
+  | Econst_int (z, t) -> ("Econst_int (" ^ string_of_int (int_of_z z) ^ ","^string_of_ctype t^")")
+  | Econst_int256 (z, t) -> ("Econst_int (" ^ string_of_int (int_of_z z) ^ ","^string_of_ctype t^")")
+  | Evar (id,t) -> ("Evar("^string_of_int (int_of_positive id)^","^string_of_ctype t^")")
+  | Etempvar (id,t) -> ("Etempvar("^string_of_int (int_of_positive id)^","^string_of_ctype t^")")
+  | Ederef (e,t) -> ("Ederef(" ^ string_of_expr e ^","^ string_of_ctype t ^")")
+  | Eunop (op,e,t) -> ("Eunop(OP,"^string_of_expr e^","^string_of_ctype t ^")")
+  | Ebinop (op,e1,e2,t) -> ("Ebinop(OP,"^string_of_expr e1^","^string_of_expr e2^","^string_of_ctype t ^")")
+  | Efield (e, ident, t) ->("Efield("^string_of_expr e^","^string_of_int (int_of_positive ident)^","^string_of_ctype t^")")
+  | Earrayderef (e1,e2,t) -> ("Earrayderef("^string_of_expr e1 ^","^string_of_expr e2^","^string_of_ctype t^")")
+  | Ehashderef (e1,e2,t) -> ("Ehashderef("^string_of_expr e1 ^","^string_of_expr e2^","^string_of_ctype t^")")
+  | Ecall0 (bt,t) -> "Ecall0(BUILTIN,TYPE)"
+  | Ecall1 (bt,e,t) -> "Ecall0(BUILTIN,EXPR,TYPE)"
+
+let rec string_of_statement = function
+  | Sskip -> "Sskip"
+  | Sassign (e1,e2) -> ("Sassign("^string_of_expr e1 ^","^ string_of_expr e2 ^")")
+  | Sset (id,e) -> ("Sset("^string_of_int(int_of_positive id)^","^string_of_expr e^")")
+  | Scall (None, lab, exprs) -> "Scall(None, LABEL, ARGS)"
+  | Scall (Some id, lab, expr) -> "Scall(Some ID, LABEL, ARGS)"
+  | Ssequence (s1,s2) -> ("Ssequence("^string_of_statement s1 ^","^ string_of_statement s2^")")
+  | Sifthenelse (e,s1,s2) -> ("Sifthenelse("^string_of_expr e^","^string_of_statement s1^","^string_of_statement s2 ^")")
+  | Sloop s -> "(Sloop "^string_of_statement s^")"
+  | Sbreak -> "Sbreak"
+  | Sreturn None -> "Sreturn None"
+  | Sreturn (Some e) -> ("Sreturn Some("^string_of_expr e^")")		      
+  | Stransfer (e1,e2) -> "Stransfer ("^string_of_expr e1 ^","^ string_of_expr e2 ^")"
+  | Scallmethod (e1,ids,z,e,es) -> "Scallmethod TODO"
+  | Slog e -> "Slog " ^ string_of_expr e
+  | Srevert -> "Srevert"
+
+let rec string_of_params = 
+  let open Datatypes in
+  function
+  | Coq_cons (Coq_pair(id, t) , params) -> "("^string_of_int (int_of_positive id) ^","^string_of_ctype t ^")::"^ string_of_params params
+  | Coq_nil -> "nil"
+		 
+let string_of_methoddef md =
+   "{ fn_return = " ^ string_of_ctype md.fn_return ^ ";\n"
+  ^"  fn_params = " ^ string_of_params md.fn_params ^";\n"
+  ^"  fn_temps =  " ^ string_of_params md.fn_temps ^";\n"
+  ^"  fn_body = " ^ string_of_statement md.fn_body ^"\n"
+  ^"}"
+   
+
 (** gen_object_methods : 
     (Int.int, coq_fun) prod list **)
 let gen_object_methods gen_methodname gen_method o =
   let open Datatypes in
   coqlist_of_list
     (List.map
-      (fun m -> Coq_pair (gen_methodname m, gen_method m))
+      (fun m -> print_endline(string_of_methoddef (gen_method m));Coq_pair (gen_methodname m, gen_method m)) (* for debugging purpose *)
       o.smethods) 
 
 (** gen_object_fields :
@@ -340,38 +411,3 @@ type genv = {
     genv_constructor : coq_function option 
   }
 **)
-
-(* 
-(* Print MiniC expressions/statements, for debugging purposes. *)
-let rec string_of_ctype = 
-  let open Ctypes in
-  function
-  | Tvoid -> "Tvoid"
-  | Tint (_,_) -> "TInt (SIZE,SIGNEDNESS)"
-  | Tpointer _ -> "Tpointer"
-  | Tarray (t,z) -> ("Tarray ("^string_of_ctype t^","^string_of_int(int_of_z z)^")")
-  | Thashmap (t1,t2) -> ("Thashmap("^string_of_ctype t1^","^string_of_ctype t2^")")
-  | Tfunction (ts,t) -> "Tfunction (TYPES,TYPE)"
-  | Tstruct (id,flds) -> "Tstring (IDENT, FIELDS)"
-  | Tunion  (id,flds) -> "Tunion (IDENT, FIELDS)"
-  | Tcomp_ptr id -> "Tcomp_ptr ID"
-
-let rec string_of_expr = function
-  | Econst_int (z, t) -> ("Econst_int (" ^ string_of_int (int_of_z z) ^ ","^string_of_ctype t^")")
-  | Econst_int256 (z, t) -> ("Econst_int (" ^ string_of_int (int_of_z z) ^ ","^string_of_ctype t^")")
-  | Evar (id,t) -> ("Evar("^string_of_int (int_of_positive id)^","^string_of_ctype t^")")
-  | Etempvar (id,t) -> ("Etempvar("^string_of_int (int_of_positive id)^","^string_of_ctype t^")")
-  | Ederef (e,t) -> ("Ederef(" ^ string_of_expr e ^","^ string_of_ctype t ^")")
-  | Eunop (op,e,t) -> ("Eunop(OP,"^string_of_expr e^","^string_of_ctype t ^")")
-  | Ebinop (op,e1,e2,t) -> ("Ebinop(OP,"^string_of_expr e1^","^string_of_expr e2^","^string_of_ctype t ^")")
-  | Efield (e, ident, t) ->("Efield("^string_of_expr e^","^string_of_int (int_of_positive ident)^","^string_of_ctype t^")")
-  | Earrayderef (e1,e2,t) -> ("Earrayderef("^string_of_expr e1 ^","^string_of_expr e2^","^string_of_ctype t^")")
-  | Ehashderef (e1,e2,t) -> ("Ehashderef("^string_of_expr e1 ^","^string_of_expr e2^","^string_of_ctype t^")")
-  | Ecall0 (bt,t) -> "Ecall0(BUILTIN,TYPE)"
-  | Ecall1 (bt,e,t) -> "Ecall0(BUILTIN,EXPR,TYPE)"
-
-let rec string_of_params = 
-  let open Datatypes in
-  function
-  | Coq_cons (Coq_pair(id, t) , params) -> "("^string_of_int (int_of_positive id) ^","^string_of_ctype t ^")::"^ string_of_params params
-  | Coq_nil -> "nil" *)

Original file line number	Diff line number	Diff line change
`@@ -14,7 +14,7 @@ constructor c (){`
`14`	`14`
`15`	`15`	`method set(x: int) {`
`16`	`16`	`guard{`
`17`		`- x > 0 ;`
	`17`	`+ /-x > 0 ;-/`
`18`	`18`	`}`
`19`	`19`	`storage{`
`20`	`20`	`storedData \|-> x;`