]> matita.cs.unibo.it Git - helm.git/commitdiff
- Added new output in standard C.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 13 Jan 2009 10:50:29 +0000 (10:50 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 13 Jan 2009 10:50:29 +0000 (10:50 +0000)
helm/software/matita/contribs/assembly/parser/parser.y
helm/software/matita/contribs/assembly/parser/test0.cm [new file with mode: 0644]
helm/software/matita/contribs/assembly/parser/test1.cm [new file with mode: 0644]

index 40d901ac789317c27c63081898bc6260749051c8..373f3b2fd85329245b4b2eb5ecece0587b780675 100755 (executable)
@@ -158,6 +158,7 @@ typedef struct _valueLeaf_
 /* ************************************************************************* */\r
 \r
 valueLeaf      root;                           /* radice dell'AST */\r
+valueLeaf      *typeRoot=NULL;         /* radice degli user type */\r
 \r
 int                    numErr=0;\r
 \r
@@ -187,6 +188,10 @@ valueLeaf  *treeId1Alloc(vEnum id,valueLeaf *param1,const YYLTYPE *locp);
 valueLeaf      *treeId2Alloc(vEnum id,valueLeaf *param1,valueLeaf *param2,const YYLTYPE *locp);\r
 valueLeaf      *treeId3Alloc(vEnum id,valueLeaf *param1,valueLeaf *param2,valueLeaf *param3,const YYLTYPE *locp);\r
 \r
+int                    eqUserType(valueLeaf *type1,valueLeaf *type2);\r
+int                    getUserType(valueLeaf *type,valueLeaf **res);\r
+void           createUserType(valueLeaf *type);\r
+\r
 void prettyPrint(valueLeaf *cur,int indent);\r
 \r
 /* ************************************************************************* */\r
@@ -289,7 +294,7 @@ _decl_lst_          :       Keyword_CONST _type_ Value_STRING DualOperator_ASG _init_choice_ S
                                        _type_ Value_STRING _init_ Separator_COLUMN _decl_lst_\r
                                                {\r
                                                $$=treeId3Alloc(E_DECL_VAR,$1,$2,$3,&@1);\r
-                                               $$->next=$5;\r
+                                               $$->next=$5;                                            \r
                                                }|\r
                                        _stm_lst_\r
                                                { $$=$1; };\r
@@ -308,6 +313,8 @@ _type_                      :       Keyword_ARRAY OpenBracket_SQUARE Value_INUM CloseBracket_SQUARE Keywo
                                                {\r
                                                $$=treeId1Alloc(E_TYPE_STRUCT,$3,&@1);\r
                                                $3->next=$5;\r
+\r
+                                               createUserType($$);\r
                                                }|\r
                                        Type_DWORD\r
                                                { $$=treeId0Alloc(E_TYPE_DWORD,&@1); }|\r
@@ -863,6 +870,107 @@ void usage(char *name)
        return;\r
 }\r
 \r
+/* *************************** gestione degli user type *********** */\r
+\r
+int eqUserType(valueLeaf *type1,valueLeaf *type2)\r
+{\r
+       valueLeaf       *tmp1,*tmp2;\r
+\r
+       if(type1->id!=type2->id)\r
+               { return(0); }\r
+\r
+       switch(type1->id)\r
+               {\r
+               case E_TYPE_DWORD:\r
+               case E_TYPE_WORD:\r
+               case E_TYPE_BYTE:\r
+                       return(1);\r
+\r
+               case E_TYPE_ARRAY:\r
+                       if(type1->param1->inumValue!=type2->param1->inumValue)\r
+                               { return(0); }\r
+\r
+                       return(eqUserType(type1->param2,type2->param2));\r
+\r
+               case E_TYPE_STRUCT:\r
+                       tmp1=type1->param1;\r
+                       tmp2=type2->param1;\r
+\r
+                       while(tmp1&&tmp2)\r
+                               {\r
+                               if(!eqUserType(tmp1,tmp2))\r
+                                       { return(0); }\r
+\r
+                               tmp1=tmp1->next;\r
+                               tmp2=tmp2->next;\r
+                               }\r
+\r
+                       return(!(tmp1||tmp2));\r
+\r
+               /* dummy */\r
+               default:\r
+                       return(0);\r
+               }\r
+}\r
+\r
+int getUserType(valueLeaf *type,valueLeaf **res)\r
+{\r
+       valueLeaf       *tmpRes=typeRoot;\r
+       valueLeaf       *lastRes;\r
+       int                     index=1;\r
+\r
+       while(tmpRes)\r
+               {\r
+               if(eqUserType(type,tmpRes))\r
+                       {\r
+                       if(res)\r
+                               { *res=tmpRes; }\r
+                       return(index);\r
+                       }\r
+\r
+               lastRes=tmpRes;\r
+               tmpRes=tmpRes->next;\r
+               index++;\r
+               }\r
+\r
+       if(res)\r
+               { *res=lastRes; }\r
+       return(0);\r
+}\r
+\r
+void createUserType(valueLeaf *type)\r
+{\r
+       if(!typeRoot)\r
+               {\r
+               if(!(typeRoot=(valueLeaf *) myMalloc(sizeof(valueLeaf))))\r
+                       {\r
+                       printf("[%s:%d] ParsError:OutOfMemory%c",__FILE__,__LINE__,SEP);\r
+                       exit(ERR_EXIT);\r
+                       }\r
+\r
+               memcpy(typeRoot,type,sizeof(valueLeaf));\r
+               typeRoot->next=NULL;\r
+               }\r
+       else\r
+               {\r
+               valueLeaf       *res;\r
+\r
+               if(!getUserType(type,&res))\r
+                       {\r
+                       if(!(res->next=(valueLeaf *) myMalloc(sizeof(valueLeaf))))\r
+                               {\r
+                               printf("[%s:%d] ParsError:OutOfMemory%c",__FILE__,__LINE__,SEP);\r
+                               exit(ERR_EXIT);\r
+                               }\r
+\r
+                       memcpy(res->next,type,sizeof(valueLeaf));\r
+                       res->next->next=NULL;\r
+                       }\r
+               }\r
+}\r
+\r
+/* *************************** prettyPrint ************************ */\r
+\r
 void prettyPrintString(char *str)\r
 {\r
        printf("([");\r
@@ -1421,6 +1529,255 @@ void prettyPrint(valueLeaf *cur,int indent)
                }\r
 }\r
 \r
+/* *************************** cPrint ***************************** */\r
+\r
+void cPrintIndent(int indent)\r
+{\r
+       int     index;\r
+\r
+       for(index=0;index<indent;index++)\r
+               { printf("\t"); }\r
+}\r
+\r
+void cPrintTypesAux(valueLeaf *type,int field)\r
+{\r
+       if(type->id==E_TYPE_STRUCT)\r
+               { printf("\tuser%d_t\tfield%d;\n\n",getUserType(type,NULL),field); }\r
+       else if(type->id==E_TYPE_ARRAY)\r
+               {\r
+               char            bufferDim[256];\r
+               valueLeaf       *tmp=type;\r
+\r
+               memset(bufferDim,0,256);\r
+\r
+               while(tmp->id==E_TYPE_ARRAY)\r
+                       {\r
+                       sprintf(&bufferDim[strlen(bufferDim)],"[%d]",tmp->param1->inumValue+1);\r
+                       tmp=tmp->param2;\r
+                       }\r
+\r
+               if(tmp->id==E_TYPE_STRUCT)\r
+                       { printf("\tuser%d_t\tfield%d%s;\n\n",getUserType(tmp,NULL),field,bufferDim); }\r
+               else if(tmp->id==E_TYPE_DWORD)\r
+                       { printf("\t_DWORD_\tfield%d%s;\n\n",field,bufferDim); }\r
+               else if(tmp->id==E_TYPE_WORD)\r
+                       { printf("\t_WORD_\tfield%d%s;\n\n",field,bufferDim); }\r
+               else\r
+                       { printf("\t_BYTE_\tfield%d%s;\n\n",field,bufferDim); }\r
+               }\r
+       else if(type->id==E_TYPE_DWORD)\r
+               { printf("\t_DWORD_\tfield%d;\n\n",field); }\r
+       else if(type->id==E_TYPE_WORD)\r
+               { printf("\t_WORD_\tfield%d;\n\n",field); }\r
+       else\r
+               { printf("\t_BYTE_\tfield%d;\n\n",field); }\r
+\r
+       if(type->next)\r
+               { cPrintTypesAux(type->next,field+1); }\r
+}\r
+\r
+void cPrintTypes(void)\r
+{\r
+       int                     index=1;\r
+       valueLeaf       *cur=typeRoot;\r
+\r
+       while(cur)\r
+               {\r
+               printf("typedef struct\n");\r
+               printf("{\n");\r
+               cPrintTypesAux(cur->param1,0);\r
+               printf("} user%d_t;\n\n",index);\r
+\r
+               cur=cur->next;\r
+               index++;\r
+               }\r
+}\r
+\r
+void cPrint(valueLeaf *cur,int indent)\r
+{\r
+       /* ** valori ** */\r
+       if(cur->id==E_VALUE_INUM)\r
+               { printf("%lu",cur->inumValue); }\r
+       else if(cur->id==E_VALUE_BYTE)\r
+               { printf("0x%02lX",(_DWORD_) cur->byteValue); }\r
+       else if(cur->id==E_VALUE_WORD)\r
+               { printf("0x%04lX",(_DWORD_) cur->wordValue); }\r
+       else if(cur->id==E_VALUE_DWORD)\r
+               { printf("0x%08lX",cur->dwordValue); }\r
+       else if((cur->id==E_VALUE_ARRAY)||(cur->id==E_VALUE_STRUCT))\r
+               {\r
+               valueLeaf       *tmp=cur->param1;\r
+\r
+               printf("{ ");\r
+               while(tmp)\r
+                       {\r
+                       cPrint(tmp,indent);\r
+                       tmp=tmp->next;\r
+                       if(tmp)\r
+                               { printf(", "); }\r
+                       }\r
+               printf(" }");\r
+               }\r
+\r
+       /* ** variabili ** */\r
+       else if((cur->id==E_VAR_ROOT)||(cur->id==E_VAR_STRUCT)||(cur->id==E_VAR_ARRAY))\r
+               {\r
+               valueLeaf       *tmp=cur;\r
+\r
+               while(tmp->id!=E_VAR_ROOT)\r
+                       {\r
+                       tmp->next->last=tmp;\r
+                       tmp=tmp->next;\r
+                       }\r
+\r
+               while(1)\r
+                       {\r
+                       if(tmp->id==E_VAR_ROOT)\r
+                               { printf("%s",tmp->param1->stringValue); }\r
+                       else if(tmp->id==E_VAR_STRUCT)\r
+                               { printf(".field%lu",tmp->param1->inumValue); }\r
+                       else if(tmp->id==E_VAR_ARRAY)\r
+                               { printf("["); cPrint(tmp->param1,indent); printf("]"); }\r
+\r
+                       if(tmp==cur)\r
+                               { break; }\r
+                       else\r
+                               { tmp=tmp->last; }\r
+                       }\r
+               }\r
+\r
+       /* ** espressioni ** */\r
+       else if(cur->id==E_EXPR_VAR)\r
+               { cPrint(cur->param1,indent); }\r
+       else if(cur->id==E_EXPR_NOT)\r
+               { printf("!("); cPrint(cur->param1,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_COM)\r
+               { printf("~("); cPrint(cur->param1,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_NEG)\r
+               { printf("-("); cPrint(cur->param1,indent); printf(")"); }\r
+       else if((cur->id==E_EXPR_W2B)||(cur->id==E_EXPR_DW2B))\r
+               { printf("((_BYTE_) ("); cPrint(cur->param1,indent); printf("))"); }\r
+       else if((cur->id==E_EXPR_B2W)||(cur->id==E_EXPR_DW2W))\r
+               { printf("((_WORD_) ("); cPrint(cur->param1,indent); printf("))"); }\r
+       else if((cur->id==E_EXPR_B2DW)||(cur->id==E_EXPR_W2DW))\r
+               { printf("((_DWORD_) ("); cPrint(cur->param1,indent); printf("))"); }\r
+       else if(cur->id==E_EXPR_ADD)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") + ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_SUB)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") - ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_MUL)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") * ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_DIV)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") / ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_SHL)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") << ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_SHR)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") >> ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_AND)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") & ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_OR)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") | ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_XOR)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") ^ ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_LT)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") < ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_LTE)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") <= ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_GT)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") > ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_GTE)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") >= ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_EQ)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") == ("); cPrint(cur->param2,indent); printf(")"); }\r
+       else if(cur->id==E_EXPR_NEQ)\r
+               { printf("("); cPrint(cur->param1,indent); printf(") != ("); cPrint(cur->param2,indent); printf(")"); }\r
+\r
+       /* ** statement ** */\r
+       else if(cur->id==E_STM_ASG)\r
+               {\r
+               cPrintIndent(indent); cPrint(cur->param1,indent); printf(" = "); cPrint(cur->param2,indent); printf(";\n\n");\r
+\r
+               if(cur->next)\r
+                       { cPrint(cur->next,indent); }\r
+               }\r
+       else if(cur->id==E_STM_WHILE)\r
+               {\r
+               cPrintIndent(indent); printf("while("); cPrint(cur->param1,indent); printf(")\n");\r
+               cPrintIndent(indent+1); printf("{\n");\r
+               cPrint(cur->param2,indent+1);\r
+               cPrintIndent(indent+1); printf("}\n\n");\r
+\r
+               if(cur->next)\r
+                       { cPrint(cur->next,indent); }\r
+               }\r
+       else if(cur->id==E_STM_IF)\r
+               {\r
+               valueLeaf       *tmp=cur->param1;\r
+\r
+               while(tmp)\r
+                       {\r
+                       cPrintIndent(indent); printf("%s(",(tmp==cur->param1) ? "if" : "else if"); cPrint(tmp->param1,indent); printf(")\n");\r
+                       cPrintIndent(indent+1); printf("{\n");\r
+                       cPrint(tmp->param2,indent+1);\r
+                       cPrintIndent(indent+1); printf("}\n");\r
+\r
+                       tmp=tmp->next;\r
+                       }\r
+\r
+               if(cur->param2)\r
+                       {\r
+                       cPrintIndent(indent); printf("else\n");\r
+                       cPrintIndent(indent+1); printf("{\n");\r
+                       cPrint(cur->param2,indent+1);\r
+                       cPrintIndent(indent+1); printf("}\n");\r
+                       }\r
+\r
+               printf("\n");\r
+\r
+               if(cur->next)\r
+                       { cPrint(cur->next,indent); }\r
+               }\r
+\r
+       /* ** dichiarazioni ** */\r
+       else if((cur->id==E_DECL_CONST)||(cur->id==E_DECL_VAR))\r
+               {\r
+               valueLeaf       *tmp=cur->param1;\r
+               char            bufferDim[256];\r
+\r
+               memset(bufferDim,0,256);\r
+\r
+               while(tmp->id==E_TYPE_ARRAY)\r
+                       {\r
+                       sprintf(&bufferDim[strlen(bufferDim)],"[%d]",tmp->param1->inumValue+1);\r
+                       tmp=tmp->param2;\r
+                       }\r
+\r
+               cPrintIndent(indent);\r
+               if(cur->id==E_DECL_CONST)\r
+                       { printf("const "); }\r
+\r
+               if(tmp->id==E_TYPE_STRUCT)\r
+                       { printf("user%d_t\t",getUserType(tmp,NULL)); }\r
+               else if(tmp->id==E_TYPE_DWORD)\r
+                       { printf("_DWORD_\t"); }\r
+               else if(tmp->id==E_TYPE_WORD)\r
+                       { printf("_WORD_\t"); }\r
+               else\r
+                       { printf("_BYTE_\t"); }\r
+\r
+               printf("%s%s",cur->param2->stringValue,bufferDim);\r
+\r
+               if(cur->param3)\r
+                       { printf(" = "); cPrint(cur->param3,indent); }\r
+               printf(";\n\n");\r
+\r
+               if(cur->next)\r
+                       { cPrint(cur->next,indent); }\r
+               }\r
+}\r
+\r
+/* *************************** main ******************************* */\r
+\r
 int main(int argc,char **argv)\r
 {\r
        int             ret;\r
@@ -1433,10 +1790,29 @@ int main(int argc,char **argv)
 \r
        if((!ret)&&(!numErr))\r
                {\r
+               printf("(* matita language *)\n\n");\r
                printf("definition parsingResult \\def\n");\r
                printf(" (PREAST_ROOT\n");\r
                prettyPrint(&root,2);\r
-               printf(" ).");\r
+               printf(" ).\n\n");\r
+\r
+               printf("(* C language\n\n");\r
+               printf("#ifndef\t__STDC__\n");\r
+               printf("typedef\tunsigned __int32\t_DWORD_;\n");\r
+               printf("typedef\tunsigned __int16\t_WORD_;\n");\r
+               printf("typedef\tunsigned __int8\t_BYTE_;\n");\r
+               printf("#else\n");\r
+               printf("typedef\t__uint32_t\t_DWORD_;\n");\r
+               printf("typedef\t__uint16_t\t_WORD_;\n");\r
+               printf("typedef\t__uint8_t\t_BYTE_;\n");\r
+               printf("#endif\n\n");\r
+               cPrintTypes();\r
+               printf("void main(void)\n");\r
+               printf("{\n");\r
+               cPrint(&root,1);\r
+               printf("\treturn;\n\n");\r
+               printf("}\n\n");\r
+               printf("*)");\r
                }\r
 \r
        return(ret);\r
diff --git a/helm/software/matita/contribs/assembly/parser/test0.cm b/helm/software/matita/contribs/assembly/parser/test0.cm
new file mode 100644 (file)
index 0000000..cd8183b
--- /dev/null
@@ -0,0 +1,19 @@
+{\r
+       const array[2] of struct { array[2] of byte; word; dword; } n1=[{[0x00,0x01],0x0000,0x00000000},{[0x02,0x03],0x0001,0x00000001}];\r
+\r
+       word n2=n1[0x00].1;\r
+\r
+       byte n3;\r
+\r
+       while(n2)\r
+               {\r
+               dword n1=n1[n2].2;\r
+\r
+               if(n1>0x1234ABCD)\r
+                       { n3=-!~(dw2b(w2dw(b2w(n3)))+0x01-0x02*0x03/0x04>>0x05<<0x06&0x07|0x08^0x09); }\r
+\r
+               n2=n2+0x0001;\r
+               }\r
+\r
+       n3=n1[0x01].0[0x00];\r
+}
\ No newline at end of file
diff --git a/helm/software/matita/contribs/assembly/parser/test1.cm b/helm/software/matita/contribs/assembly/parser/test1.cm
new file mode 100644 (file)
index 0000000..a53a879
--- /dev/null
@@ -0,0 +1,42 @@
+#define u1 struct { byte; word; }\r
+#define u2 struct { word; byte; }\r
+#define u3 struct { array[2] of u1; array[3] of u2; }\r
+#define u4 struct { array[3] of u1; array[2] of u2; }\r
+#define u5 struct { dword; u3; u4; array[5] of word; }\r
+\r
+{\r
+       u5 var5;\r
+       byte index=0x00;\r
+\r
+       while(index<0x02)\r
+               {\r
+               const array[4] of u1 const1=[{0x00,0x0000},{0x01,0x0001},{0x02,0x0002},{0x03,0x0003}];\r
+               const array[4] of u2 const2=[{0x0000,0x00},{0x0001,0x01},{0x0002,0x02},{0x0003,0x03}];\r
+\r
+               var5.1.0[index].0=const1[index].0+(index*0x03);\r
+               var5.1.0[index].1=const1[index].1*(b2w(index)-0x1234);\r
+               var5.2.1[index].0=const1[index].1&(b2w(index)/0xABCD);\r
+               var5.2.1[index].1=const1[index].0^(!index);\r
+\r
+               if(index!=0x00)\r
+                       {\r
+                       dword tmp=0x1234FEDC;\r
+\r
+                       var5.0=tmp;\r
+                       }\r
+               elsif(index==0x01)\r
+                       {\r
+                       array[7] of array[8] of array [9] of byte tmp;\r
+\r
+                       tmp[0x02][0x01][0x00]=index;\r
+                       }\r
+               else\r
+                       {\r
+                       array[10] of u5 tmp;\r
+\r
+                       tmp[0x00].0=var5.0;\r
+                       }\r
+\r
+               index=index+0x01;\r
+               }\r
+}\r