没有合适的资源?快使用搜索试试~ 我知道了~
可在www.sciencedirect.com在线获取理论计算机科学电子笔记288(2012)37-47www.elsevier.com/locate/entcsC程序静态分析的有效类型推断1帕斯卡尔·索廷2INRIA摘要C语言没有特定的布尔类型:布尔值用整数编码。 这是对于枚举类型也是如此,它可以自由地和静默地转换为整数或从整数转换。另另一方面,旨在推断每个程序点处变量的可能值的验证工具可以从以下信息中受益:某些(整数)变量仅用作布尔或枚举类型变量,或更一般地用作具有小域的有限类型变量。事实上,专门和有效的符号表示,如BDD可以用于表示这些变量的属性,而近似表示,如间隔和八边形更适合于更大的域整数和浮点变量。基于这种动机,本文提出了一种静态分析方法,用于推断C程序中变量的更精确类型,以有效地使用它们。分析了C99语言的一个子集,包括指针、结构和动态分配。关键词:静态分析,类型推断,C语言,布尔,有限类型。1引言C程序的验证。这项工作的最初动机是使用工具CONCUR IINTERPROC[6]推断C程序上的不变量。当想要将学术分析器与C语言连接时,有两个主要问题:(i) 分析器可能会遇到它不是设计来处理的C语言的特性。这在最好的情况下导致使用不精确的回退处理,在最坏的情况下导致无声的不合理分析。(ii) 分析器可能无法识别C表示中的设计特征。这导致对程序的处理不那么精确本文讨论属于第(ii)点的一个问题1这项工作得到了法国ANR项目ASOPT的支持2电子邮件:bertrand. inria.frpascal. inria.fr1571-0661 © 2012 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2012.10.00638B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)37int b,x;if(b)x++;boolb;intx;if(b)x++;Fig. 1. 布尔类型整型用整数变量编码的布尔值验证工具CONCUR IINTERPROC区分数值、布尔和有限枚举变量。 我们想把C程序作为这个分析器的输入,并利用它的类型系统。不幸的是,C类型系统太弱了例如图 1,b和x都被声明为int,但分析器将通过将b视为布尔值而将x视为数字来获得精度(然后将执行取决于b的真值的析取分析)。此外,即使b被声明为布尔枚举类型{false=0,true=1},这并不意味着它在其他地方没有被赋值为2。贡献我们提出了一个静态分析的C程序,专门在一个健全的方式,通用整数类型的一些变量和结构字段到布尔或推断枚举类型。此分析考虑了由过程调用和指针引发的别名属性。这种静态分析允许将初始弱类型的C程序转换为语义等价的强类型程序,可以通过诸如CONCURINTER-PROC[6]的验证工具更有效地分析。 在简短介绍了上下文和相关工作(第2节)之后,我们首先在一个只涉及过程和整数变量的简单上下文中描述我们的分析(第3节),然后将其扩展到指针,结构和动态分配(第4节),并在结论中讨论剩余的问题2一般背景和相关工作如前所述,我们的动机是将CONCUR IINTERPROC验证工具[6]及其扩展连接到指针PIINTERPROC[10]。这些工具可以将C程序的整数变量视为数值变量,通过使用例如八边形[ 8 ]表示它们的可能值,但它们可以更精确地处理(即, 在一个析取的方式)这些整数变量,实际上是作为布尔或枚举变量操作,使用BDD s。避免布尔变量和数值变量之间混淆的一个简单解决方案是使用C的强类型形式(例如。Cyclone [7]),并确保程序尊重声明的类型,但这并不适用于普通的C程序。加强分析程序的类型化问题 [3]在解释型语言(如JavaScript)的上下文中,使用弱类型和动态类型解决了这个问题。作者执行一个对数据流敏感的静态分析,收集给定点上变量的可能类型。类似地,出于编译目的,已经提出了许多技术来推断调用站点处的对象的可能类,以便优化动态调用解析B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)3739progprocdecl ::=(类型化变量的声明)类型::=intstm|lvexpr)过程调用|return x表示变 量 的值中文(简体)公司简介 ::= cst|左常量或左值|博博莱快递|公司简介|快递"?”expr ":“expr”条件表达式请输入boolexpr::=“!”公司简介|bool布尔表达式根据C99标准计算为0或1公司简介 ::=“−"expr|expr“德国 ::= 0,1,2,.吉尔布尔·比诺普 ::=“”我的&&天|“||“|“==”|“!=”|“”我的<天|......这是什么?比诺普·阿申特 ::=“+”|“--”|“”|“/“|“”我的&天|“|“|......这是什么?图二. 一般语法静态调用。与我们的分析相比,这些分析以一种对下行敏感的方式推断类型集,而我们正在为每个变量寻找一个唯一的对下行不敏感的类型。3具有过程调用和标量变量的我们首先在简单的程序环境中介绍我们的静态分析,一些只操作标量变量的过程(我们从标量中排除指针)。这允许在研究指针、强制转换和动态分配引起的其他问题之前,在一个简单的环境中讨论我们的方法。3.1所考虑的输入语言我们考虑C的一个简单子集,其文法3如图2所示。f、g表示过程名,x、y表示变量名。由于我们的分析是对数据流不敏感的,因此我们不详细介绍与控制相关的语句。简而言之,在这个子集中,所有变量都被声明为整数,没有指针,没有结构化类型,没有动态分配的数据。我们假设所有过程都返回一个值,并且变量通过它们的名称唯一标识我们不考虑显式枚举类型声明,这与SPLint [1]等工具不同,SPLint会抱怨从一个枚举类型到另一个枚举类型的转换。这是因为我们的分析并不是为了帮助程序员发现由于弱类型而导致的潜在问题3我们忽略了有关分隔符等的细节40B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)37x=expr∈xstmreturnexpr∈Cumstm(f)x= f(表达式1,..., exprn)typf(ty p1x1, . ,typnxn)∈proc(二)D(x)D(expr)D(f)D(expr)D(cst)={cst}D(布尔表达式)={ 0, 1}D(整数表达式)=ZD(x)D(f)i:D(xi)(三)D(exprexpr1图3.第三章。在标量程序中推断变量的可能值3.2推断变量在这个简单的设置中,我们的分析哲学并不是真的推断类型,而只是发现给定过程中任何变量的可能值的集合。这意味着我们关注的是一个与属性无关、对流程和上下文不敏感的静态分析,它计算一个函数D:过程变量→ P(Z)(1)哪里• P(Z)是整数子集的完备格,其最小上界算子与集合并重合• D(f)表示过程f的可能返回值,D(x)表示变量x的可能值。点序泛函集D=ProcVar→ P(Z)是一个完备格(任何D∈ D的余域是有限的)。这种推理分析在图3中形式化。它基于对过程中包含的赋值、过程调用和返回语句的检查。我们隐式地将函数D扩展到使用等式(1)的表达式。(三)、 注意,我们没有利用表达式的上下文:有子表达式“x+3“或“x?1:0“不允许推断C语言中x中包含的可能值的任何信息。这种分析与常数传播分析非常相似,在常数传播分析中,晶格处的常数λ被晶格P(Z)代替。我们在这个分析中执行的近似是考虑任何整数表达式的可能值的集合(如图1所定义)2)是所有整数值的集合例如,如果x可以取值1或3(即,D(x)={1,3}),我们的分析认为x +1可以取任何值(即,D(x +1)= Z),而不仅仅是集合{2,4}中的一个值。如果没有这种近似,我们的分析是不可计算的,因为格D不满足有限升链条件。另一种方法是不执行这种近似,而是使用一个加宽算子,当它们的基数大于给定的阈值时,用Z替换Z的有限子集。这种替代方案对应于常数传播分析的析取完成,配备了一个加宽算子,以确保收敛。4或至少非常昂贵,如果考虑到所有变量都是有限机器整数,B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)3741ZHKKnk给定一个特定的程序,分析中出现的P(Z)中最长的元素链长度为H,最多是程序中出现的数字常数的数量加上3(因为布尔运算符返回的因此,全分析最多收敛于H|Proc|+ |Var|步骤,其中|Proc|、|Var|分别表示程序和变量的数量。3.3键入分析的程序一旦通过前面的分析计算出函数D,我们必须将弱类型的C程序转换为C语言的强类型变体,其中运算符的类型如图所示4(a).该变换基于有限值D(x)={v1,.,v n}隐式定义了一个枚举类型,在公式中表示为typ D(x)。如果D(x)=Z,则按照惯例,类型D(x)=int。转换包括两个操作:(i) 添加枚举类型声明:• 对于每个不同的有限值D k={v1,..., v}的D,我们插入C类型声明“typedef enum {lk 1 = vk 1,...,lkn=vkn} tk“;• 我们隐式地添加预定义类型}bool• 每个变量声明这同样适用于过程的返回类型。(ii) 在整数和有限类型之间插入强制转换,以确保正确的类型。表达式和赋值的翻译如图4所示,其中我们对类型使用以下操作:t tJ=tt如果t=tJ否则,(四)图5(b)显示了在prog.图5(a)。注意,强制转换运算符castbool <$int和castint <$bool的定义并不完全遵循与普通枚举类型相同的模式,因为任何非零整数值都与布尔值true相关联。3.4讨论可靠性准则是新程序应具有与原程序相同的很容易看出,给定通过分析计算的函数D的性质以及函数typ和cast的定义,不会发生键入错误。但是,如果在初始化之前读取某些变量,则会出现问题看看右边的程序我们的推理分析将类型enum{l1=1}分配给x}中。 因此,作为一个布尔值,x总是为真,函数返回1。 C99标准规范int main()函数{ int x,y;y = x?1:0;x =1;return y;}42B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)37(Ⅲ)(a)(1)(1)(2)(Ⅲ)<$lv)=^lv,opb:t→te1op2e2=castt<$t'(e1)opbcastt<$t'(e2)if^1t′=typ(ei)β2:α×α→bol⎪⎨f:t1×. . . ×tn→t112!b:bool→bool−b:int →int&&b,||b:bool×bool→ booltypp(cst)=inttypp(x)=typD(x)typ(opb e)=t ifopb:t1→t+ b,b,<b,.:int×int →bool22bbty p(e1?be2:be3)=typ(e2)Htyp(e3)==,!为:α×α→bool类型(铸造(e))=t·?b·:b·:bool×α×α→α(a) C99运算符的强类型版本。α是用于多态算子的类型变量。(cst)=^cstBt2←t12(b) 键入表达式<$op1e)=^op1(castt1<$t'(<$e)如果t′=typ(e)(2)(Ⅱ),opb:t1×t2→tB1 2←t1Bt←t2′ ′ ′eop2e)=^castt''1(e))op2cast''2(e)ift=t1Ht2t′=typ(ei)(bb bi)1? e2:e3)=^castbool<$t'1(<$e1))? castt'←t'2(e2):castt'←,t'3(e3)如果t′=t′2Ht′3t′=typ(ei)<$lv=e)=^lv=cast<$t'(<$e))ift=typ(lv)t′=typ(e)(一)lv=f(e1, . ,en)=lv=castt'<$t(f(castt1<$t'1(e1, . ,casttn<$tn'(en))如果t′=typ(lv)t′i=typ(<$ei))castt←t(e)=ecastt←in t(e)=(e==v1)? l1:castint<$t(l)=(l==l1)?v1:kk k...kk k...(e==vnk −1)? lnk −1:lnk(l==lnk−1)?vnk−1:vnkk k k k k kint(e)=(e== 0)false:truecastint←bool(e)=是吗?一比零castt<$t'=castt <$int如果t/=t′,则cast t <$t <$t(d)强制转换运算符图四、生成程序的强类型版本另一方面,x的值在y被赋值时是未知的,这意味着它可以有任何值。为了在不使框架复杂化的情况下处理这个问题,我们选择强制所有变量在被读取之前进行初始化。 检查这个假设可以用大多数C编译器中实现的经典数据流分析来完成,并且可以通过将任何非参数声明“int x“替换为“int x=0“来在原始程序中执行它。第二个要点与我们开发能力的动机有关一些工具来更精确地分析有限状态变量。因为我们插入了从枚举类型到整数的转换,所以我们可能会在第一眼看到ben-将枚举类型分配给proc的一些原始整数变量的限制1222、(c)通过插入强制转换来转换表达式和赋值B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)3743克使用CONCUR IINTERPROC工具不会发生这种情况,这要归功于44B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)37------public int findDuplicate(intx){if(x==0)x=1;elsex=0;return x;}intmain(){inty = incrmod2(1);return y;(a)原始C程序typedef枚举k 0 =0,k1=1t;tincrmod 2(t x)typedef枚举k 0 =0,k1=1t; tincrmod 2(t x){if(cast intt(x)==0)x=casttint(1); elsex=casttint(0);return x;}tmain(){ty =incrmod2(casttint(1));return y;}(b)添加有限类型typedef枚举k 0 =0,k1=1t; tincrmod 2(t x){if((x==k0? 0:1)==0)x=(1==0?k0:k1);否则x=(0==0?returnx;return x;}intmain(){t y = incrmod 2(1==0?returny;return y;(c)膨胀铸件{if(x==k0)x=k1; else x=k0;return x;}intmain(){ty =incrmod2(k1);return y;}(d)计算常数图五、推断枚举类型并转换原始程序。它通过在条件表达式的分支中推送运算符和简化琐碎的测试来规范表达式例如,它重写表达式if((x==k0?0:1)==0)x=(1==0?k0:k1),如下所示:如果((x==k0? 0:1)==0)x=(1==0? k0:k1 )如果(x==k0?0==0:1==0)x=k1如果(x==k0)x=k14添加指针、结构和动态分配现在我们在语言中添加指针、结构化类型和动态分配我们扩展了图的文法2如下:typp|“typedef struct {“(类型定义)结构“}“texpr |pexpr|“&“x|“&“(x → n)中文(简体)|“”x stm::=. | ⟨ lv ⟩ = alloc(⟨typ⟩)(五)我们特别添加了从变量或结构的字段创建指针值的操作符(没有函数指针)。&n,m,. 表示结构字段的名称,假定是唯一的。我们只允许在左值中使用一个*运算符(包括隐式的 *of->)。类似于&&*pb;我们在本节中所做的重要假设是,显式)类型t1k和t2k′之间的转换,其中k节目在这方面做得很好。kjt1t2,并且,B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)3745{}}{}}int main()函数intx = 0; inty= 1;int*p =NULL;p=x;*p=2;p=y;*p=3;return*p;}(a) 原始程序typedef枚举l0=0,l1=1,l2=2,l3=3t;tmain(){t x =l0; ty =l1;returnNULL;p = x; *p =l2; p =y; *p =l3; return*p;}(b) 最终编程intn;t;int main()函数{tx; t* y;int *p,*q;y =alloc(t); p =(y->n); y =x;n =(n);*p =1;*q =2;*p = *p1;return *p;}(a) 原始程序typedef枚举l0=0,l1=1,l2=2e;typedef structe n;t;int main()函数{tx; t* y; e*p,*q;...*p =l1;*q =l2;*p =(*p==l0)?return*p;}(b) 最终编程图第六章使用标量指针的程序图7。结构程序4.1推理分析的目的在第3节中,我们的有限类型推断简化为对标量变量的可能值的分析。在这个新的设置中,我们的类型推断的目标是(i) 如前所述,检测被操作为布尔或枚举类型的标量变量,并推断相应的类型;(ii) 而且也适用于结构化类型的领域;同时考虑指针引起的键入和别名属性。我们的分析将为给定的字段名返回一个唯一的类型,这意味着我们放弃了在不同的上下文中捕获相同结构化类型的不同(布尔/整数)使用。考虑Fig.的程序第6(a)段。我们想推断p可能指向x,或者y.这允许推断D(x)={ 0, 2, 3}和D(y)={ 1, 2, 3}。现在,由于x和y可能被同一个指针p指向,它们应该具有相同的类型。因此,我们生成图的程序6(b).现在考虑图7(a)的程序。我们知道y是一个指向类型为t的结构的指针。我们不需要更多关于指向结构的指针的信息,因为给定类型的所有结构的字段n最终可能被专门化为唯一类型。换句话说,对应于字段n的所有位置都被汇总到一个名为.n的位置。我们仍然需要推断p和q可以指向类型t的对象的标量场.n,并从这个事实推断标量场可以包含集合D(.n)={ 0, 1, 2}中的值。这导致图1的程序7(b).总而言之,我们需要一种弱形式的指向分析,在这种分析中,我们只对指针变量、整数变量和结构域之间的指向关系感兴趣。{{46B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)37x = expr∈ xstmint n+x∈n declP(x)P(expr)returnexpr ∈ Cumstm(f)int+ f(. . )∈ProcP(f)P(expr)P(null)=0x= expr∈int n+x∈ n decly∈P(x):P(y)x= f(表达式1,..., exprn)typf(ty p1x1, . ,typnxn)∈procP(x)≠P(f)iftyp =int n+吉吉|typi = int i+:P(x i)P(expri)P(x)={x}(仅适用于var。 类型为int类型)P((x→n))=联系我们(仅适用于整型字段)P(exprpexpr1见图8。 指向分析(六)x = expr∈ xstmintx∈ {\displaystyle x}D(x)D(expr)returnexpr∈ Cumstm intf(. . )∈procD(f)D(expr)x= expr∈int n+x∈ n declf∈P(x):D(y)<$D(expr)x = f(expr1,.,exprn)typf(ty p1x1, . ,typnxn)∈procD(x)=D(f)如果typ=inttypi=int:D(xi)D(expri)D(cst)={cst}D(x)=y∈P(x)D(y)D(boolexpr)={ 0,1}D(intexpr)=ZD(exprexpr1第九章推断变量和字段的可能值(七)4.2分析的形式化我们仍然执行一种弱形式的数据流和上下文无关的指向分析,它推断出一个函数P:过程 Var 场→ P(变量 外地)它将过程返回值、变量和指针类型的字段映射到变量和字段。P(x)(resp. P(.n))将是一组变量和场的过度近似,x(resp.任何对象的field.n)都可以指向。该函数是图8的推理规则的最小解,其中,(6)将P扩展到类型为intk,k >0的表达式。然后,我们通过推断一个函数来推广3.2节的标值分析D:过程变量 场→ P(Z)它将整数变量和字段映射到可能的值。该函数是图9的推理规则的最小解,其中,(7)将D扩展到int类型的表达式。4.3键入分析的程序如4.1节所述,给变量赋值类型比纯标量的情况要复杂一些,因为同一指针吉吉|B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)3747KK应该是相同的类型。否则,是否需要强制转换可能取决于指针的值。因此,我们认为,• 如果x(或.n)最初声明为整数,则typ(x)= typ{D(y)|n(p){x,y}};• 如果 x(或 .n) 是 最初 宣布 作为 一 指针 intk,k>0, (x)=(typy∈Pk(x)D(y))<$,其中P表示P的第k个<$.模型的插入完全按照3.3节中的方法进行。观察我们所做的指针之间不需要强制转换:我们不能有“t* x; int* y;...; y=x4.4讨论在本节中,我们将第3节的命题扩展到更广泛的C子集。然而,这个建议是在一些假设下完成的(没有强制转换和指针算法),应该被视为值分析和指向分析如何相互作用的演示可以通过使用经典的研究充分的点到分析来放松这些假设。特别是Steensgardd的技术[11]似乎很适合,因为它是跨过程的,对数据流不敏感,并且接受等式5的语言。这种技术通过强制转换来推断C程序所操作的指向关系和有效结构除了处理结构和指针之外,还可以通过为整个数组提供唯一类型并假设没有发生超范围访问来将数组处理集成到指向分析中。请注意,在3.4节中提到的变量在被读取之前必须被初始化的条件,也应该满足动态分配的内存,但这要检查或执行起来更复杂5结论提出了一种在C程序中确定int类型变量集合中布尔变量和枚举变量集合的方法。这些信息对编译几乎没有用处,但可以通过将这些变量分配给适当的抽象域来提高程序验证的精度该过程将C语言的一个大子集(包括函数、结构、指针)作为输入,并执行简单的指向分析,然后执行值分析。这些分析的结果允许通过细化类型并在正确的位置插入显式强制转换来将程序转换为强类型的等价版本。请注意,如果使用的抽象域 分析器能够在它们操纵的变量逃避它们的能力时动态地切换它们操纵的变量的类型。但是,在文献中提出的抽象领域往往是非常专业化的(例如。计算点[2],数值阵列[4]),并考虑更一般的情况将增加其复杂性的负担。48B. Jeannet,P.Sotin/Electronic Notes in Theoretical Computer Science 288(2012)37我们的工作与C程序编译为中间语言或更简单的子集是互补的[9,5]。这些建议可以被看作是专门用于验证的前端,通过减少C和更简单的分析器输入语言之间的差距,从而回答了引言中的第(i)点一个 执行 具有 被 发达 对于CONCUR IINTERPROC[6], 具有c2newspeak[5]作为前端。分析器只处理标量类型,不需要分析的指向版本(第4节),但具有更丰富内存模型的分析器的进一步开发将从中受益引用[1] 埃文斯,D.和D. Larochelle,Improving security using extensible lightweight static analysis,IEEESoftware19(2002). 42比51[2] Goubault,E.,M. Martel和S. Putot,Asserting the precision of adjusting pointing computations:Asimpleabst ract interpreter,in:D. L. M'etayer,editor,ESOP,LectureNotesinComputerScience2305(2002), pp.209-212[3] Guha,A., C. Saftoiu和S. Krishnamurthi,Typing local control and state using crossflowanalysis,在:G. Barthe,editor,ESOP,Lecture Notes in Computer Science6602(2011),pp. 256-275。[4] Hal bwa chs,N. 和M. P'eron,Dis coveringpro perties a boutarays in simpleprog ram,in:R. Gupta和S. P. Amarasinghe,editors,PLDI(2008),pp.339-348.[5] 海曼斯角和O.Levillain,Newspeak,Doubleplussimple Minilang for Goodthinkful Static Analysis ofC,Technical report,EADS(2008).[6] Jeannet,B.,并发程序的关系过程间验证,见:软件工程和形式化方法,SEFM[7] 吉姆,T.,J. G. Morrisett,D.格罗斯曼,M. W. Hicks,J. Cheney和Y.王,旋风:一个安全的方言的C,在:C。S. Ellis,editor,USENIX Annual Technical Conference,General Track(2002),pp.275-288。[8] Mi n'e,A., Octagonabst ract domain,Higher-OrderandSymBolicComputation19(2006).[9] Necula、G. C.的方法,S. McPeak,S. P. Rahul和W. Weimer,CIL:Intermediate Language and Toolsfor Analysis and Transformation of C Programs , in : R. N. Horspool , editor , CC , LNCS2304(2002),pp. 213-228.[10] Sotin,P. and B. Jeannet,在存在指向堆栈,在:G. Barthe,editor,ESOP,Lecture Notes in Computer Science6602(2011),pp.459-479[11] Steensgaard,B., 通过对具有结构和联合的程序的类型推断进行的指向分析,在:T. Gyim'ot hy,编辑,CC,计算机科学讲义1060(1996),pp. 136-150
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- zigbee-cluster-library-specification
- JSBSim Reference Manual
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功