diff --git a/infer/src/llvm/examples/store.ll b/infer/src/llvm/examples/store.ll new file mode 100644 index 000000000..84f52b1c1 --- /dev/null +++ b/infer/src/llvm/examples/store.ll @@ -0,0 +1,5 @@ +; Function with store instruction +define i32 @main() { + store i32 0, i32* %i + ret i32 0 +} diff --git a/infer/src/llvm/lAst.ml b/infer/src/llvm/lAst.ml index b973656aa..de2d378ad 100644 --- a/infer/src/llvm/lAst.ml +++ b/infer/src/llvm/lAst.ml @@ -34,6 +34,7 @@ type instr = | Ret of (typ * operand) option | UncondBranch of variable | CondBranch of operand * variable * variable + | Store of operand * typ * variable type func_def = FuncDef of variable * typ option * (typ * string) list * instr list diff --git a/infer/src/llvm/lLexer.mll b/infer/src/llvm/lLexer.mll index 4e33f0768..088bc3eef 100644 --- a/infer/src/llvm/lLexer.mll +++ b/infer/src/llvm/lLexer.mll @@ -121,7 +121,7 @@ rule token = parse (* memory access and addressing operations *) (*| "alloca" { ALLOCA }*) (*| "load" { LOAD }*) - (*| "store" { STORE }*) + | "store" { STORE } (*| "fence" { FENCE }*) (*| "cmpxchg" { CMPXCHG }*) (*| "atomicrmw" { ATOMICRMW }*) diff --git a/infer/src/llvm/lParser.mly b/infer/src/llvm/lParser.mly index 7e3b113b9..75caa6f76 100644 --- a/infer/src/llvm/lParser.mly +++ b/infer/src/llvm/lParser.mly @@ -96,7 +96,7 @@ (* memory access and addressing operations *) (*%token ALLOCA*) (*%token LOAD*) -(*%token STORE*) +%token STORE (*%token FENCE*) (*%token CMPXCHG*) (*%token ATOMICRMW*) @@ -165,7 +165,7 @@ vector_typ: element_typ: | width=INT { Tint width } | floating_typ { Tfloat } - | tp=ptr_typ { tp } + | tp=ptr_typ { Tptr tp } floating_typ: | HALF { () } @@ -176,7 +176,7 @@ floating_typ: | PPC_FP128 { () } ptr_typ: - | tp=typ STAR { Tptr tp } + | tp=typ STAR { tp } block: | LBRACE instrs=list(instr) RBRACE { instrs } @@ -184,6 +184,8 @@ block: instr: | term=terminator { term } | variable EQUALS binop { Ret None } (* TODO *) + | STORE val_tp=typ value=operand COMMA ptr_tp=ptr_typ var=variable { Store (value, val_tp, var) } + (* don't yet know why val_tp and ptr_tp would be different *) terminator: | RET tp=typ op=operand { Ret (Some (tp, op)) } diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index a115a4b29..64eefa72a 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -37,6 +37,8 @@ let trans_instr (cfg : Cfg.cfg) (pdesc : Cfg.Procdesc.t) : LAst.instr -> Sil.ins | Ret (Some (tp, exp)) -> let ret_var = Sil.get_ret_pvar (Cfg.Procdesc.get_proc_name pdesc) in [Sil.Set (Sil.Lvar ret_var, trans_typ tp, trans_operand exp, Sil.dummy_location)] + | Store (op, tp, var) -> + [Sil.Set (trans_variable var, trans_typ tp, trans_operand op, Sil.dummy_location)] | _ -> raise (Unimplemented "Need to translate instruction to SIL.") (* Update CFG and call graph with new function definition *) @@ -76,7 +78,7 @@ let trans_func_def (cfg : Cfg.cfg) (cg: Cg.t) : LAst.func_def -> unit = function let exit_kind = Cfg.Node.Exit_node procdesc in let exit_node = Cfg.Node.create cfg Sil.dummy_location exit_kind [] procdesc [] in let nodekind_of_instr : LAst.instr -> Cfg.Node.nodekind = function - | Ret _ -> Cfg.Node.Stmt_node "method_body" + | Ret _ | Store _ -> Cfg.Node.Stmt_node "method_body" | _ -> raise (Unimplemented "Need to get node type for instruction.") in let node_of_instr (cfg : Cfg.cfg) (procdesc : Cfg.Procdesc.t) (instr : LAst.instr) : Cfg.Node.t = Cfg.Node.create cfg Sil.dummy_location (nodekind_of_instr instr) (trans_instr cfg procdesc instr) procdesc [] in